categorical semantics 1comprehension categories 1fibrations 1free constructions 1lawvere-ehrhard 1type theory 1
From the 1 of 4 linked papers with an AI index.
Showing math.CTShow all
3 papers · 1 filter
math.CT2025
Toward the effective 2-topos
Steve Awodey, Jacopo Emmenegger
A candidate for the effective 2-topos is proposed and shown to include the effective 1-topos as its subcategory of 0-types.
math.CT2025
Algebraic Presentations of Type Dependency
Benedikt Ahrens, Jacopo Emmenegger, Paige Randall North +1
C-systems were defined by Cartmell as the algebraic structures that correspond exactly to generalised algebraic theories. B-systems were defined by Voevodsky in his quest to formul…
math.CT2024
A 2-categorical analysis of context comprehension
Greta Coraglia, Jacopo Emmenegger
We consider the equivalence between the two main categorical models for the type-theoretical operation of context comprehension, namely P. Dybjer's categories with families and B.…