April 2: Szumi Xie, The groupoid-syntax of type theory is a set
Angiuli, Carlo
Szumi Xie
The groupoid-syntax of type theory is a set
The talk will be on Thursday, April 2 at 11:30 AM EDT (UTC-4) / 15:30 UTC, which should once again be the "usual" time for Europeans now that we are all on summer time. Also 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:
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).