4 papers
Predicative Aspects of Order Theory in Univalent Foundations
Tom de Jong, Martín Hötzel Escardó
We investigate predicative aspects of order theory in constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's pr…
A Note on Generalized Algebraic Theories and Categories with Families
Marc Bezem, Thierry Coquand, Peter Dybjer +1
We give a new syntax independent definition of the notion of a generalized algebraic theory as an initial object in a category of categories with families (cwfs) with extra structu…
Injective types in univalent mathematics
Martín Hötzel Escardó
We investigate the injective types and the algebraically injective types in univalent mathematics, both in the absence and in the presence of propositional resizing. Injectivity is…
A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom
Martín Hötzel Escardó
In introductions to the subject for a general audience of mathematicians or logicians, the univalence axiom is typically explained by handwaving. This gives rise to several misconc…