An experimental library of formalized mathematics based on the univalent foundations
From MaRDI portal
Publication:5740657
Recommendations
Cites work
Cited in
(33)- Univalent Foundations and the UniMath Library
- An introduction to univalent foundations for mathematicians
- Kripke-Joyal forcing for type theory and uniform fibrations
- Univalent foundations of mathematics
- Categorical structures for type theory in univalent foundations
- Lawvere theories and C-systems
- Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. I: Theory of sets
- Type theory and formalisation of mathematics
- Proof assistants for natural language semantics
- Formal Representation of Mathematics in a Dependently Typed Set Theory
- From signatures to monads in \textsf{UniMath}
- Higher Structures in Homotopy Type Theory
- Univalent foundations of mathematics and paraconsistency
- Some Wellfounded Trees in UniMath
- Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers
- scientific article; zbMATH DE number 7474655 (Why is no real title available?)
- Liquid tensor experiment
- A univalent formalization of the \(p\)-adic numbers
- Internal parametricity for cubical type theory
- C-system of a module over a \(Jf\)-relative monad
- Homotopy type-theoretic interpretations of constructive set theories
- Cubical methods in homotopy type theory and univalent foundations
- Univalent foundations as structuralist foundations
- On Small Types in Univalent Foundations
- Vladimir Aleksandrovich Voevodsky
- Maintaining a library of formal mathematics
- Heterogeneous substitution systems revisited
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- Constructive sheaf models of type theory
- The simplicial model of univalent foundations (after Voevodsky)
- Combinatorial topology and constructive mathematics
- Towards a constructive simplicial model of Univalent Foundations
- Injective types in univalent mathematics
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)
