Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mathstodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance for maths people. We have LaTeX rendering in the web interface!

Administered by:

Server stats:

2.8K
active users

mathstodon.xyz: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

#hottest

0 posts0 participants0 posts today
Public
Dan Christensen

This week the seminar presents:

Mitchell Riley

Tiny types and cubical type theory

The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 17. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See uwo.ca/math/faculty/kapulkin/s for the Zoom link and a list of all upcoming talks.

All are welcome!

@carloangiuli @emilyriehl

Abstract:

I will present an extension of Martin-Löf Type Theory that contains a tiny object; a type for which there is an "amazing" right adjoint to the formation of function types as well as the expected left adjoint. A primary aim of the theory is to be simple enough to be used both by hand and in a (hypothetical) proof assistant. I will sketch a normalisation algorithm and discuss a few potential applications, in particular, to implementations of Cubical Type Theory.

www.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
Public
Dan Christensen

This week the seminar presents:

Jonathan Weinberger

Directed univalence and the Yoneda embedding for synthetic ∞-categories

The talk is at 11:30am EST (16:30 UTC) on Thursday, March 6. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See uwo.ca/math/faculty/kapulkin/s for the Zoom link, the abstract, and a list of all upcoming talks.

All are welcome!

@carloangiuli @emilyriehl

Abstract:

In this talk, I'll present recent results in synthetic ∞-category theory in an extension of homotopy type theory. An ∞-category is analogous to a 1-category, but with composition defined only up to homotopy. To reason about them in HoTT, Riehl and Shulman proposed simplicial HoTT, an extension by a directed interval, generating the shapes that model arrows and their composition.

To account for fundamental constructions like the opposite category or the maximal subgroupoid, we add further type formers as modalities using Gratzer-Kavvos-Nuyts-Birkedal's framework of multimodal dependent type theory (MTT).

I'll present the construction of the universe 𝒮 of small ∞-groupoids in that setting which we can show to be an ∞-category satisfying directed univalence. As an application, we can define various ∞-categories of interest in higher algebra such as ∞-monoids and ∞-groups. Furthermore, I'll show the construction of the fully functorial Yoneda embedding w.r.t. 𝒮 as well as the Yoneda lemma (which is hard to establish in set-theoretic foundations). [truncated due to space considerations]

The material is joint work with Daniel Gratzer und Ulrik Buchholtz (arxiv.org/abs/2407.09146, arxiv.org/abs/2501.13229).

www.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
Public *
Martin Escardo

Today was one of these days I left home at 7am and got back home from work at 8pm.

Luckily the commute is nice by bike in the canal, and short too, only <20 minutes (4 miles) each way.

Also at least I wasn't doing bureaucracy, but teaching preparation, followed by teaching, followed by a teaching meeting with staff and TA's, followed by more teaching preparation for tomorrow.

I love teaching, but I really need to find time to prepare my Thursday talk, preferably not on Thursday, and preferably not in the evening.

Public *
Dan Christensen

This week the seminar presents:

Martín Hötzel Escardó

Injective types

The talk is at 11:30am EST (16:30 UTC) on Thursday, February 20. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See uwo.ca/math/faculty/kapulkin/s for the Zoom link, the abstract, and a list of all upcoming talks.

All are welcome!

@carloangiuli @emilyriehl @MartinEscardo

Abstract:

In previous work, we established results about injective types in HoTT/UF, including characterizations, closure properties, and examples. In recent current work, in collaboration with Tom de Jong, we have developed more examples and counter-examples, as well as a better understanding of the landscape. In this talk I will present these old and new ideas.

www.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
Public
Dan Christensen

This week the seminar presents:

Mario Carneiro

Lean4Lean: Towards a Verified Typechecker for Lean, in Lean

The talk is at 11:30am EST (16:30 UTC) on Thursday, February 6. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See uwo.ca/math/faculty/kapulkin/s for the Zoom link and a list of all upcoming talks.

All are welcome!

Abstract:

This talk will present Lean4Lean, a project to construct a verified checker for the Lean theorem prover in the style of MetaCoq. It consists of a new “external verifier” for Lean, written in Lean. It is the first complete verifier for Lean 4 other than the reference implementation in C++ used by Lean itself, and the new verifier is competitive with the original, running between 20% and 50% slower and usable to verify all of Lean’s mathlib library, forming an additional step in Lean’s aim to self-host the full elaborator and compiler. The second part of the project concerns the type theory itself, and establishing its properties (in spite of several known negative results about the behavior of the type system), with the ultimate goal of being able to show that the verifier is correct to a specification of the type theory, and that the type theory is consistent relative to ZFC with countably many inaccessible cardinals. This work is still ongoing but we plan to use this project to help justify any future changes to the kernel and type theory and ensure unsoundness does not sneak in through either the abstract theory or implementation bugs.

@carloangiuli @emilyriehl

www.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
Public
Lane

I thought that it might be interesting to diary some thoughts tangential to my research from time to time here.

I picked up Homotopy Type Theory (#hott) and #categorytheory more or less from scratch, albeit with the help of many wonderful guides and tutors from online seminars (#HoTTest Summer School crew and Topos Institute, I'm looking at you). Therefore I've been more or less undisturbed in forming my intuition on these subjects, often drawn to philosophical considerations and themes. 🧵

Public
Dan Christensen

This week the seminar presents:

Paige North

Coinductive control of inductive data types

The talk is at 11:30am EST (16:30 UTC) on Thursday, December 5. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See uwo.ca/math/faculty/kapulkin/s for the Zoom link, the abstract, and a list of all upcoming talks.

All are welcome!

@carloangiuli @emilyriehl

www.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
Public
Dan Christensen

This week the seminar presents:

Niels van der Weide

The internal languages of univalent categories

The talk is at 11:30am EST (16:30 UTC) on Thursday, November 21. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See uwo.ca/math/faculty/kapulkin/s for the Zoom link, the abstract, and a list of all upcoming talks.

All are welcome!

@carloangiuli @emilyriehl

www.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
Public
beSpacific

#Climate: #2024 promises to be a record year, above the 1.5oC #warming mark. The year 2024 will almost certainly be the #hottest year on record and the first with an average temperature increase in the world of 1.5 degrees Celsius over the pre-industrial period according to data from European Copernicus service published after the second warmest month of October. #ClimateCrisis #globalheating #poverty #catastrophy #drilling #fossilfuels #economy #government #politics tiredearth.com/fr/news/climat-

Public
Dan Christensen

This week the seminar presents:

Tashi Walde

An axiomatization of synthetic category theory

The talk is at 11:30am EST (16:30 UTC) on Thursday, November 7. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See uwo.ca/math/faculty/kapulkin/s for the Zoom link, the abstract, and a list of all upcoming talks.

(Note that we are no longer on daylight time, so the local time may have changed for you.)

All are welcome!

@carloangiuli @emilyriehl

www.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
SearchLive feeds
About