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

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