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