#hott — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #hott, aggregated by home.social.
-
Delooping generated groups in homotopy type theory. ~ Camil Champin, Samuel Mimram, Emile Oleon. https://arxiv.org/abs/2405.03264v1 #Agda #ITP #HoTT
-
This week the #HoTTEST seminar presents:
Freek Geerligs
Synthetic Stone duality
The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 16. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
In this talk, we will give an overview of Synthetic Stone duality (https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.3). We will then discuss some related work in progress.
Synthetic Stone duality is an extension of homotopy type theory with four axioms. These axioms are strong enough to decide Bishop's omniscience principles. We introduce a (synthetic) topology on any type, such that all functions are continuous. We are interested in Stone spaces and compact Hausdorff spaces, where the topology behaves as one would expect. In particular, we can define the (topological) interval and show that all functions are continuous in the epsilon-delta sense.
Currently, we are working on a paper with a method for calculating cohomology with countably presented coefficients for compact Hausdorff spaces. We are also interested in a correspondence between homotopical concepts defined using traditional topology (using paths from the topological interval) and homotopy type theory (using identity types).
This talk will contain joint work with Reid Barton, Felix Cherubini, Thierry Coquand, and Hugo Moeneclaey.
-
This week the #HoTTEST seminar presents:
Szumi Xie
The groupoid-syntax of type theory is a set
The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 2. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks. (This should be back to the "usual" time for Europeans who are now on summer time.)
All are welcome!
Abstract:
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of homotopy type theory, one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, I will introduce the notion of groupoid categories with families (GCwFs), which truncates types at the groupoid level and incorporates coherence equations.
I will demonstrate that the initial GCwF for a type theory with some type formers is set-truncated, using a technique called α-normalization. This allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models.
I will also present a generalization of GCwFs and discuss its relation to comprehension categories.
This talk is based on joint work with Thorsten Altenkirch and Ambrus Kaposi (https://doi.org/10.4230/LIPIcs.CSL.2026.40).
-
This week the #HoTTEST seminar presents:
Astra Kolomatskaia
Displayed Type Theory, intervals, and analytic higher categorical structures
The talk is at 11:30am EDT (15:30 UTC) on Thursday, March 19. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks. (Note that we recently started daylight time in North America, so the local time may have changed for you.)
All are welcome!
Abstract:
I have historically encountered a number of difficulties in communicating my work to others. The process of preparing this talk has thus involved engaging with throughlines in the type theory literature and has helped me identify places in which building bridges was necessary.
My joint work with Mike Shulman introduced Displayed Type Theory [dTT], which syntactically admits a construction of semi-simplicial types in a way that then semantically admits interpretation into arbitrary Grothendieck (∞,1)-topoi. This result is not novel as stated: First, it is not a syntactic construction in Book HoTT. Second, syntactic constructions of SSTs were a foremost consideration in the development of 2LTT, and Elif Üsküplü's analysis shows that the inner layer of 2LTT, when enriched with an axiom of cofibrant exo-nats, is general with respect to Grothendieck (∞,1)-topos semantics. [...]
[Full abstract too long for even two toots, so follow the link to the seminar page to see it all.]
-
This week the #HoTTEST seminar presents:
Ayberk Tosun (@ayberkt)
Constructive and predicative locale theory in univalent foundations
The talk is at 11:30am EST (16:30 UTC) on Thursday, March 5. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract in the next post (because of the character limit)
-
This week the #HoTTEST seminar presents:
Bastiaan Cnossen
Synthetic category theory in CaTT
The talk is at 11:30am EST (16:30 UTC) on Thursday, February 19. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
Up to now, most approaches to a synthetic theory of categories are based on Martin-Löf type theory (e.g. directed/simplicial type theory). In this talk, I discuss some first explorations for using the type theory CaTT as a basis for synthetic category theory.
The type theory CaTT, developed by Finster and Mimram, captures the internal language of a weak ω-category: a categorical structure with n-morphisms for every n with operations satisfying the weakest possible form of coherence laws. Unlike HoTT, CaTT may be interpreted directly within any (∞,1)-category, without need for intricate strictification results. In particular, CaTT has a model given by the (∞,1)-category Cat of small (∞,1)-categories.
The long-term goal of our project is to enhance CaTT with additional rules capturing the internal language of Cat. In this talk I will focus on a first step: after explaining the basics of CaTT, I will formulate additional rules in CaTT that force its models to be (∞,1)-categories with products, pullbacks and/or internal homs. I will further explain how we hope to extend this in the future. Everything is joint with Ivan Kobe.
-
The 2026 website for the annual autumn school Proof and Computation is now up at https://www.mathematik.uni-muenchen.de/~schwicht/pc26.php
I'm excited to give a short course introducing homotopy type theory / univalent foundations, and look forward to participating in this very enjoyable school once more!
-
I forgot to announce this week's #HoTTEST seminar ahead of time, but the talk is now live on YouTube, so you can watch it there: https://youtu.be/dCOZGKbSQSo
Talk info:
Benedikt Ahrens
A type theory for comprehension categories
Abstract:
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories.
We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with Π-, Σ-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations.
This talk is based on joint work with Niyousha Najmaei, Niels van der Weide, and Paige Randall North published in doi:10.1145/3776725.
-
This week the #HoTTEST seminar presents:
Matteo Spadetto
Different descriptions of the semantics of computation axioms
The talk is at 11:30am EST (16:30 UTC) on Thursday, December 4. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
We discuss three ways of formulating the semantics of type theory (syntactic, (higher) categorical, and homotopy theoretic) and the relationships between them, focusing on concrete examples provided by axiomatic type constructors.
#HoTT @carloangiuli @emilyriehl -
Emily Riehl: How I became seduced by Univalent Foundations
[tbh I think shes only disclosing her theoretical motivations her; I recall she was posting questions about Linux distros a few years ago, and if we're honest being a nerd is the actual reason 99% of people get into HoTT]
https://www.youtube.com/watch?v=XIYoI5j5Flo&t=486s -
I enjoyed listening to this lecture, or at least the first half by Emily Riehl. About computer proof and mathematics. And scary vibe proofs and why they are nonsense
-
Readings shared November 7, 2025. https://jaalonso.github.io/vestigium/posts/2025/11/08-readings_shared_11-07-25 #AI #Agda #AlphaEvolve #FormalVerification #FunctionalProgramming #Haskell #HoTT #ITP #LLM #LeanProver #Math #Rocq
-
Polynomial universes in Homotopy Type Theory. ~ C.B. Aberlé, David I. Spivak. https://arxiv.org/abs/2409.19176 #ITP #Agda #HoTT
-
This week the #HoTTEST seminar presents:
Stefania Damato
The Groupoid CwF of Containers
The talk is at 11:30am EST (16:30 UTC) on Thursday, November 6. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract: The original definition of a category with families (CwF) gives rise to some coherence issues when working intensionally. For example, the set model and the presheaf model technically do not fit this definition because their collections of types form groupoids and not h-sets. Altenkirch and Kaposi have previously introduced a CwF of containers which suffers from similar coherence issues in the intensional setting. In this talk, I will present ongoing work on fixing these issues for the container case by defining a groupoid CwF (GCwF) of containers. A GCwF allows us to have types forming groupoids, while requiring us to prove some extra coherences.
-
@lobsters above post is about #hott #homotopytypetheory
-
This week the #HoTTEST seminar presents:
Axel Ljungström
A formalisation of the Serre finiteness theorem
The talk is at 11:30am EDT (15:30 UTC) on Thursday, October 23. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
The central claim of the Serre finiteness theorem is that homotopy groups of spheres are finitely presented. Remarkably, this theorem can be proved constructively in HoTT. A particular consequence of this is that we get a completely synthetic proof of Brown's result that we, at least in theory, can compute (in the computer scientist's sense of the word) any homotopy group of any sphere! The HoTT proof of the Serre finiteness theorem, which is due to Barton and Campion, quickly inspired the launching of a rather extensive formalisation project, with the end-goal of verifying Barton and Campion's proof in Cubical Agda. About a month ago, this formalisation was finally completed.
In this talk, I'll give a rough outline of the Barton and Campion's proof. In my presentation, I will try to follow the timeline of the formalisation project and emphasise whenever the formalisation actually ended up leading to simplifications of the original pen-and-paper proof. I will also take the opportunity to mention some recent work on CW complexes which turned out to play an important role in both the formalisation and the pen-and-paper proof of the theorem.
This is joint work with Reid Barton, Owen Milner, Anders Mörtberg and Loïc Pujet.
-
This week the #HoTTEST seminar presents:
Greg Langmead
Discrete differential geometry in homotopy type theory
The talk starts in five minutes: 11:30am EDT (15:30 UTC) on Thursday, October 9. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See our new website https://hottest-seminar.github.io/for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
Type families on higher inductive types such as pushouts can capture homotopical properties of differential geometric constructions including connections, curvature, and vector fields. We define a class of pushouts based on simplicial complexes, then define principal bundles, connections, and curvature on these. We provide an example of a tangent bundle but do not prove when these must exist. We define vector fields, and the index of a vector field. Our main result is a theorem relating total curvature and total index, a key step to proving the Gauss-Bonnet theorem and the Poincaré-Hopf theorem, but without an existing definition of Euler characteristic to compare them to. We draw inspiration in part from the young field of discrete differential geometry, and in part from the original classical proofs, which often make use of triangulations and other discrete arguments.
-
The #HoTTEST seminar begins its fall season with the following talk:
Jon Sterling
Is it time for a new proof assistant?
The talk is at 11:30am EDT (15:30 UTC) on Thursday, September 25. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See our new website https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
It could be time to build a non-experimental proof assistant for homotopy type theory and univalent foundations. I’ll give my thoughts on what that would entail, and where we are able to contribute in the era of Pax Leanica, focusing on algebraic hierarchies, carefully designed user experience, and a proposed return to foundational orthodoxy.
-
The Fall 2025 HoTTEST lineup
The HoTTEST organizers are pleased to announce the Fall 2025 lineup for the Homotopy Type Theory Electronic Seminar Talks (HoTTEST). The speakers are:
Sep 25: Jon Sterling
Oct 9: Greg Langmead
Oct 23: Axel Ljungstrom
Nov 6: Stefania Damato
Nov 20: Benedikt Ahrens
Dec 4: Matteo SpadettoThe seminar will meet on alternating Thursdays at 11:30 Eastern Time. For the first three meetings of the seminar this means Eastern Daylight Time (11:30 EDT = 15:30 UTC), while for the final three meetings this means Eastern Standard Time (11:30 EST = 16:30 UTC).
For updates and instructions how to attend, please see our brand new website:
https://hottest-seminar.github.io/
Titles and abstracts will be announced shortly before each talk on the hott-electronic-seminar-talks list. Please join if you'd like to receive those announcements:
https://groups.google.com/g/hott-electronic-seminar-talks
For the organizers: Carlo Angiuli, Dan Christensen, Chris Kapulkin, Emily Riehl.
#HoTT @carloangiuli @emilyriehl -
I enjoyed talking about my expository paper (https://doi.org/10.4230/LIPIcs.TYPES.2024.1) at this wonderful CIRM event this morning.
https://conferences.cirm-math.fr/3377.htmlThanks to Jacopo Emmenegger for the photo!
-
Ordinal exponentiation in homotopy type theory. ~ Tom de Jong et als. https://arxiv.org/abs/2501.14542 #ITP #Agda #HoTT #Math
-
PhD position with Benno van den Berg on the semantics of Homotopy Type Theory (esp. effective Kan fibrations) at the ILLC in Amsterdam!
https://www.illc.uva.nl/NewsandEvents/News/Positions/newsitem/15777/PhD-Position-in-the-Semantics-of-Homotopy-Type-TheoryApplication deadline: 27 September.
-
TYPES talk done! Time to enjoy the rest of the conference 😄 I talked about injective types in univalent mathematics which is joint work with @MartinEscardo. You can find my slides here https://tdejong.com/talks/TYPES-2025.pdf.
-
This week the #HoTTEST 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 https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html for the Zoom link and a list of all upcoming talks.
All are welcome!
#HoTT @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.
-
This week the #HoTTEST 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 https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html for the Zoom link, the abstract, and a list of all upcoming talks.
All are welcome!
#HoTT @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 (https://arxiv.org/abs/2407.09146, https://arxiv.org/abs/2501.13229).
-
RE: https://math.andrej.com/2009/12/28/constructive-gem-irrational-to-the-power-of-irrational-that-is-rational/ @andrejbauer
If you can classically prove that a computable number is irrational, there is a constructive proof of the same fact! The same thing applies to proofs that a number is transcendental.
To be more specific, if you prove it in PA, it can also be proven in HA, if you can prove it in ZFC, it can also be proven in IZF, etc... (Probably works with classical #HoTT to HoTT, but that seems a pain to prove.)
Proof: Let p be a program that computes a real number r. (To be specific, for every rational ε>0, p(ε) is rational number such that |p(ε) - r| ≤ ε.) Assume there is a classical proof of "the real number computed by p is irrational". Then there is also a classical proof that "For all rational numbers q, there exists a rational number ε>0 such that |p(ε) - q| > ε". By the Friedman translation, there is a constructive proof of the same sentence (see https://mathoverflow.net/questions/460815/#comment1195059_460815). From there, we can create a constructive proof of "the real number computed by p is apart from every rational number". A similar argument works for proving a number transcendental.
∎ -
"Concerning computer assisted proofs, it seems to me the main obstacle is user friendliness; if you want this to become a part of the culture of mathematics, that when you submit a paper it includes a computer verification that the paper is correct -- I think this is very unlikely to become a part of the culture of mathematics, but if you want it to -- then, what you need is proof assistants that mathematicians are willing to use, so that it doesn't take 100 times as long to provide that certificate as it does to produce a paper the usual way."
- Jacob Lurie -
Index of selected threads on #hott #constructive #math
* 2022/10/31. Proofs by contradiction.
https://mathstodon.xyz/@MartinEscardo/109264034964990196* 2022/11/12. Synthetic topology of data types and classical spaces.
https://mathstodon.xyz/@MartinEscardo/109332986014534390* 2022/11/14. Notions of space.
https://mathstodon.xyz/@MartinEscardo/109343930842850773* 2022/11/16. Trichotomy of ordinals.
https://mathstodon.xyz/@MartinEscardo/109355604029879269* 2022/11/22. Birthday present by Tom de Jong.
https://mathstodon.xyz/@MartinEscardo/109388875794058555* 2022/11/23. Concrete example illustrating that constructive mathematics is more general than classical mathematics.
https://mathstodon.xyz/@MartinEscardo/109395006766077334* 2022/12/01. Combinatorial game theory.
https://mathstodon.xyz/@MartinEscardo/109440314312765877* 2022/12/08. Universe polymorphic type systems.
https://mathstodon.xyz/@MartinEscardo/109480057029596732* 2022/12/08. Why cubical type theory, and why cubical Agda?
https://mathstodon.xyz/@MartinEscardo/109480455436886869* 2022/12/20. The axiom of choice in HoTT/UF.
https://mathstodon.xyz/@MartinEscardo/109546988519874380* 2022/12/22. A common generalization of the univalence axiom and the K axiom.
https://mathstodon.xyz/@MartinEscardo/109558670025171863* 2023/02/03. Defining large numbers without using induction.
https://mathstodon.xyz/@MartinEscardo/109802885041067972* 2023/02/10. Several kinds of categories in HoTT/UF.
https://mathstodon.xyz/@MartinEscardo/109842791175514936* 2023/03/03. Universes in type theory as mathematical objects interesting in their own right.
https://mathstodon.xyz/@MartinEscardo/109961534132268566* 2023/03/22. Playing rationally against irrational players.
https://mathstodon.xyz/@MartinEscardo/110068977445045121* 2023/04/11. What are universes for in HoTT/UF?
https://mathstodon.xyz/@MartinEscardo/110181596099423100* 2023/06/02. Ayberk's predicative version of the patch locale of a Stone locale.
https://mathstodon.xyz/@MartinEscardo/110476555405397697* 2023/06/07. Github project TypeTopology.
https://mathstodon.xyz/@MartinEscardo/110504563233350460* 2023/06/15. Constructive notions of disjunction.
https://mathstodon.xyz/@MartinEscardo/110549967500023998* 2023/07/09. Trichotomy of the reals constructively.
https://mathstodon.xyz/@MartinEscardo/1106850749211032371/
-
TTRPG things that I'm into:
#ttrpg #dnd #adnd #odnd #osr #notthecreepyosr #classic #traveller #swordswizardry #battletech #mechwarrior
#chainmail #dba #hott #chaoswars #miniatures #painting #modeling #wargames #wargaming
-
My motto: (this is where I lamely realize I don't have a unique motto, I tend to adopt others').
#aspergers #parent #grandparent #veteran #usaf
#ttrpg #dnd #adnd #odnd #osr #traveller #swordswizardry #battletech #mechwarrior
#chainmail #dba #hott #chaoswars #miniatures #painting #modeling #wargames #wargaming
#camping #hunting #bowhunting #fishing #hiking
#marksmanship #shooting #reloading
(Edited over time... this might change!)
