February 5: Benedikt Ahrens, A Type Theory for Comprehension Categories
Angiuli, Carlo
Benedikt Ahrens
A Type Theory for Comprehension Categories
The talk will be this Thursday, February 5 at 11:30 AM EST (UTC-5) = 16:30 UTC, and will be 60 minutes followed by up to 30 minutes for questions. (Abstract below.) You can find the Zoom link and all our past and upcoming talks at our new-ish website:
https://hottest-seminar.github.io
See you then!
Carlo
(on behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen, Chris Kapulkin, and Emily Riehl)
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.