From the 1 of 4 linked papers with an AI index.
4 papers
Free constructions for comprehension categories
Francesco Dagnino, Jacopo Emmenegger, Andrea Giusto
The paper investigates comprehension categories used to model type dependency, introduces a subclass called Lawvere‑Ehrhard comprehension categories, and provides constructions of…
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.
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…
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.…