5 citations · 11 across the 11 of their papers we have counts for
13 papers
Free constructions for comprehension categories
Francesco Dagnino, Jacopo Emmenegger, Andrea Giusto
Jacobs comprehension categories subsume a large class of categorical models of type dependency, supporting also the description of morphisms between types. We study the relationshi…
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.…
Categorical models of subtyping
Greta Coraglia, Jacopo Emmenegger
Most categorical models for dependent types have traditionally been heavily set based: contexts form a category, and for each we have a set of types in said context -- and for each…
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…
The solutions to single-variable polynomials, implemented and verified in Lean
Nicholas Dyson, Benedikt Ahrens, Jacopo Emmenegger
In this work, we describe our experience in learning the use of a computer proof assistant - specifically, Lean - from scratch, through proving formulae for the solutions of polyno…
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…
W-types in setoids
Jacopo Emmenegger
We present a construction of W-types in the setoid model of extensional Martin-Löf type theory using dependent W-types in the underlying intensional theory. More precisely, we prov…
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…
Exact completion and constructive theories of sets
Jacopo Emmenegger, Erik Palmgren
In the present paper we use the theory of exact completions to study categorical properties of small setoids in Martin-Löf type theory and, more generally, of models of the Constru…
A category-theoretic version of the identity type weak factorization system
Jacopo Emmenegger
Gambino and Garner proved that the syntactic category of a dependent type theory with identity types can be endowed with a weak factorization system structure, called identity type…