147 citations · 398 across the 15 of their papers we have counts for
4 papers · 1 filter
Homotopy-initial algebras in type theory
Steve Awodey, Nicola Gambino, Kristina Sojakova
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion…
Inductive types in homotopy type theory
Steve Awodey, Nicola Gambino, Kristina Sojakova
Homotopy type theory is an interpretation of Martin-Löf's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebrai…
The identity type weak factorisation system
Nicola Gambino, Richard Garner
We show that the classifying category C(T) of a dependent type theory T with axioms for identity types admits a non-trivial weak factorisation system. We provide an explicit charac…
Lawvere-Tierney sheaves in algebraic set theory
Steve Awodey, Nicola Gambino, Peter L. Lumsdaine +1
We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that we c…