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).

#HoTT @carloangiuli @emilyriehl @de_Jong_Tom

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.]

#HoTT @carloangiuli @emilyriehl @de_Jong_Tom

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.

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)

#HoTT @carloangiuli @emilyriehl @jdchristensen

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.

#HoTT @carloangiuli @emilyriehl

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!

#logic #typetheory #HoTT

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.

#HoTT @carloangiuli @emilyriehl

Urs Schreiber:
> It took the editors at "Quantum Topology" 111 weeks to conclude they are "not interested" in our arxiv.org/abs/2309.07245 .

http://ncatlab.org/schreiber/show/Model+Structure+on+K-Linear+Infinity-Local+Systems

The Twitter post:
https://x.com/UrsSchreiber/status/2011394201674711188

#Math #MathematicalPhysics #HoTT #CategoryTheory