An experimental library of formalized mathematics based on the univalent foundations
From MaRDI portal
Publication:5740657
Recommendations
Cites work
Cited in
(33)- From signatures to monads in \textsf{UniMath}
- On Small Types in Univalent Foundations
- Maintaining a library of formal mathematics
- A univalent formalization of the \(p\)-adic numbers
- 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
- scientific article; zbMATH DE number 7474655 (Why is no real title available?)
- Univalent foundations of mathematics
- Injective types in univalent mathematics
- Categorical structures for type theory in univalent foundations
- Towards a constructive simplicial model of 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
- Univalent foundations as structuralist foundations
- Homotopy type-theoretic interpretations of constructive set theories
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)
