An experimental library of formalized mathematics based on the univalent foundations
From MaRDI portal
Publication:5740657
DOI10.1017/S0960129514000577zbMATH Open1361.68192OpenAlexW2132795002MaRDI QIDQ5740657FDOQ5740657
Authors: 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
Recommendations
Cites Work
Cited In (33)
- From signatures to monads in \textsf{UniMath}
- On Small Types in Univalent Foundations
- A univalent formalization of the \(p\)-adic numbers
- Maintaining a library of formal mathematics
- Formal Representation of Mathematics in a Dependently Typed Set Theory
- Lawvere theories and C-systems
- Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. I: Theory of sets
- Kripke-Joyal forcing for type theory and uniform fibrations
- Univalent foundations of mathematics and paraconsistency
- Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers
- Proof assistants for natural language semantics
- The simplicial model of univalent foundations (after Voevodsky)
- Liquid tensor experiment
- Univalent Foundations and the UniMath Library
- Some Wellfounded Trees in UniMath
- C-system of a module over a \(Jf\)-relative monad
- Combinatorial topology and constructive mathematics
- Higher Structures in Homotopy Type Theory
- Cubical methods in homotopy type theory and univalent foundations
- Type theory and formalisation of mathematics
- Title not available (Why is that?)
- Towards a constructive simplicial model of Univalent Foundations
- Injective types in univalent mathematics
- Univalent foundations of mathematics
- Categorical structures for type theory in univalent foundations
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- Vladimir Aleksandrovich Voevodsky
- Internal parametricity for cubical type theory
- Constructive sheaf models of type theory
- Heterogeneous substitution systems revisited
- An introduction to univalent foundations for mathematicians
- Homotopy type-theoretic interpretations of constructive set theories
- Univalent foundations as structuralist foundations
Uses Software
This page was built for publication: An experimental library of formalized mathematics based on the univalent foundations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5740657)
