An experimental library of formalized Mathematics based on the univalent foundations

DOI10.1017/S0960129514000577zbMath1361.68192OpenAlexW2132795002MaRDI QIDQ5740657

Vladimir Voevodsky

Publication date: 27 July 2016

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129514000577

Mathematics Subject Classification ID

Categorical logic, topoi (03G30)

Related Items (25)

Categorical structures for type theory in univalent foundations ⋮ Cubical methods in homotopy type theory and univalent foundations ⋮ Vladimir Aleksandrovich Voevodsky ⋮ Type theory and formalisation of mathematics ⋮ Constructive sheaf models of type theory ⋮ Higher Structures in Homotopy Type Theory ⋮ Univalent Foundations and the UniMath Library ⋮ On Small Types in Univalent Foundations ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ C-system of a module over a \(Jf\)-relative monad ⋮ Proof Assistants for Natural Language Semantics ⋮ Univalent foundations as structuralist foundations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Injective types in univalent mathematics ⋮ Homotopy type-theoretic interpretations of constructive set theories ⋮ An introduction to univalent foundations for mathematicians ⋮ Combinatorial topology and constructive mathematics ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ Lawvere theories and C-systems ⋮ Some Wellfounded Trees in UniMath ⋮ From signatures to monads in \textsf{UniMath} ⋮ Heterogeneous Substitution Systems Revisited ⋮ Univalent Foundations of Mathematics and Paraconsistency ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types

Uses Software

• Coq

Cites Work

• The calculus of constructions
• Unnamed Item

This page was built for publication: An experimental library of formalized Mathematics based on the univalent foundations