March 19: Astra Kolomatskaia, Displayed Type Theory, intervals, and analytic higher categorical structures
Angiuli, Carlo
Astra Kolomatskaia
Displayed Type Theory, intervals, and analytic higher categorical structures
PLEASE NOTE: the talk is on Thursday, March 19 at 11:30 AM EDT (UTC-4) / *15:30* UTC. This will be an unusual time for those of you located in Europe, because the US and Canada are already on summer time.
As usual, 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 our past and upcoming talks. All are welcome!
Carlo
(on behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen, Tom de Jong, and Emily Riehl)
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.
In this talk, I would like to explicitly set aside novelty claims, and focus on sticking points that are important in the sense of being necessary for building communication bridges.
The threads I would like to address are: the history of coherence theorems in constructions of models for dependent and univalent type theories, the emergence of constructive models of univalence and subsequent emergence of cubical type theories, and the initially parallel history of type theories with internalised parametricity and of modal type theories, all of which lead to a current landscape in which these threads merge by way of carcinization [convergent evolution] into interval-based cubical type theories situated in the framework of Orton and Pitts, which allows for modular conversion of diagram models on cube categories into constructive models of univalence by way of slotting in a notion of fibrancy subject to well-understood axioms.
There are several grounds on which dTT does not currently seem to slot into the Orton and Pitts framework or admit an interval-based treatment. The foremost point is that dTT reifies in syntax properties of the direct category of unary semi-cubes [no symmetries or degeneracies]. The lack of degeneracies in the index category brings about considerations of modal guarding that are subtly different from the modal considerations already present in the Orton and Pitts picture [this extends even to the full framework of multi-modal type theories as in the work of Nuyts and Devriese on transpension], and ties closely to the current understanding of interval based theories. Further, I feel that there are aspects of dTT that are unintelligible without careful delineation of the current usage of the phrase "internal model" within the literature.
The tail end of this talk will discuss the prospect of formalising higher category theory in dTT. This approach may be meaningfully described as an analytic counterpart to existing synthetic theories. I will formally introduce a Narya construction of Kan complexes from May 2024 in joint work with Kevin Carlson and Reed Mullanix, and discuss ongoing work with Reed in developing a shape/cofibration layer for dTT that seems necessary for further progress.
Displayed Type Theory is joint work with Mike Shulman
The construction of Kan complexes in Narya is joint work with Kevin Carlson and Reed Mullanix
The shape/cofibration theory for dTT is in-progress joint work with Reed Mullanix