Showing 2019Show all
2 papers · 1 filter
cs.LO2019
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…
math.CT2019
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…