@GottaLaff
José A. AlonsoReadings shared May 5, 2026. https://jaalonso.github.io/vestigium/posts/2026/05/05-readings_shared_05-25-26 #AI4Math #Agda #FunctionalProgramming #Haskell #HoTT #ITP #IsabelleHOL #LeanProver #Lisp #LogicProgramming #Math #Programming #Prolog #Python #Scheme
Delooping generated groups in homotopy type theory. ~ Camil Champin, Samuel Mimram, Emile Oleon. https://arxiv.org/abs/2405.03264v1 #Agda #ITP #HoTT
Delooping generated groups in homotopy type theory
Homotopy type theory is a logical setting based on Martin-Löf type theory in which one can perform geometric constructions and proofs in a synthetic way. Namely, types can be interpreted as spaces (up to continuous deformation) and proofs as homotopy invariant constructions. In this context, the loop spaces of types with a distinguished element (more precisely, pointed connected groupoids), provide a natural representation of groups, what we call here internal groups. The construction which internalizes a given group is called delooping, because it is a formal inverse to the loop space operator. As we recall in the article, this delooping operation has a concrete definition for any group G given by the type of G-torsors. Those are particular sets together with an action of G, which means that they come equipped with an endomorphism for every element of G. We show that, when a generating set is known for the group, we can construct a smaller representation of the type of G-torsors, using the fact that we only need automorphisms for the elements of the generating set. We thus obtain a concise definition of (internal) groups in homotopy type theory, which can be useful to define deloopings without resorting to higher inductive types, or to perform computations on those. We also investigate an abstract construction for the Cayley group of a generated group. Most of the developments performed in the article have been formalized using the cubical version of the Agda proof assistant.
Dan ChristensenThis 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.]
lneI'm feeling more confident in the perspective that the reason we're faced with the problem of an infinite coherence tower in #hott is due to the fact that a given notion of composition is biased up to some chosen isomorphism, where even definitional equality (i.e. at idn) is a choice. Even if it is an operational notion of composition, to choose necessarily leads to the loss of information. We may instead proceed by characterizing the relationship of a choice to the total space of composites.
It turns out a neat definition of (wild?) category(?) in #hott obtains by supposing a notion of ternary composition based on generalizing from the following equivalence in cubical type theory:
`PathP A x y ≃ (∀ w → w ≡ x → ∀ z → y ≡ z → PathP A w z)`
Only in the general (categorical) case, we formulate this as an embedding, so we have a map s.t.:
`Hom x y ↪ (∀ w → Hom w x → ∀ z → Hom y z → Hom w z)`
derived from the map, some contractibility conditions, and an interchange axiom.
Tom de JongThis 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)
ayhon#HoTT #CubicalAgda
I'm trying to wrap my head around how `hcomp` works. In particular, does it have any definitional equalities? Would `hcomp {φ = i1} u u0` be definitionally equal to `u i1 1=1` for instance? I don't see a reference to any such reductions in the documentation.
I'm trying to wrap my head around how `hcomp` works. In particular, does it have any definitional equalities? Would `hcomp {φ = i1} u u0` be definitionally equal to `u i1 1=1` for instance? I don't see a reference to any such reductions in the documentation.