11 citations · 15 across the 3 of their papers we have counts for
6 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…
Domain Theory in Constructive and Predicative Univalent Foundations
Tom de Jong, Martín Hötzel Escardó
We develop domain theory in constructive univalent foundations without Voevodsky's resizing axioms. In previous work in this direction, we constructed the Scott model of PCF and pr…
Introduction to Univalent Foundations of Mathematics with Agda
Martín Hötzel Escardó
We introduce Voevodsky's univalent foundations and univalent mathematics, and explain how to develop them with the computer system Agda, which is based on Martin-Löf type theory. A…
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…