5 citations · 11 across the 11 of their papers we have counts for
7 papers · 1 filter
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.
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.…
A comonad for Grothendieck fibrations
Jacopo Emmenegger, Luca Mesiti, Giuseppe Rosolini +1
We prove that cloven Grothendieck fibrations over a fixed base $\ct{B}$ are the pseudo-coalgebras for a lax idempotent 2-comonad on $\ct{Cat}/\ct{B}$. We show this via an original…
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 characterisation of elementary fibrations
Jacopo Emmenegger, Fabio Pasquali, Giuseppe Rosolini
Grothendieck fibrations provide a unifying algebraic framework that underlies the treatment of various form of logics, such as first order logic, higher order logics and dependent…
The Fullness Axiom and exact completion of homotopy categories
Jacopo Emmenegger
We use a category-theoretic formulation of Aczel's Fullness Axiom from Constructive Set Theory to derive the local cartesian closure of an exact completion. As an application, we p…
On the local cartesian closure of exact completions
Jacopo Emmenegger
This paper presents a necessary and sufficient condition on a category with weak finite limits for its exact completion to be (locally) cartesian closed. A paper by Carboni and Ros…