Pages that link to "Item:Q5740657"
From MaRDI portal
The following pages link to An experimental library of formalized Mathematics based on the univalent foundations (Q5740657):
Displaying 24 items.
- Univalent foundations as structuralist foundations (Q1708879) (← links)
- Combinatorial topology and constructive mathematics (Q1788338) (← links)
- The simplicial model of univalent foundations (after Voevodsky) (Q2031691) (← links)
- From signatures to monads in \textsf{UniMath} (Q2319990) (← links)
- Type theory and formalisation of mathematics (Q2399357) (← links)
- C-system of a module over a \(Jf\)-relative monad (Q2689172) (← links)
- Some Wellfounded Trees in UniMath (Q2819193) (← links)
- Proof Assistants for Natural Language Semantics (Q2963996) (← links)
- Vladimir Aleksandrovich Voevodsky (Q4558118) (← links)
- Heterogeneous Substitution Systems Revisited (Q4580223) (← links)
- Categorical structures for type theory in univalent foundations (Q4683858) (← links)
- An introduction to univalent foundations for mathematicians (Q4684362) (← links)
- Lawvere theories and C-systems (Q4959711) (← links)
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types (Q5016211) (← links)
- (Q5028425) (← links)
- (Q5031679) (← links)
- Cubical methods in homotopy type theory and univalent foundations (Q5055493) (← links)
- Constructive sheaf models of type theory (Q5084309) (← links)
- Injective types in univalent mathematics (Q5156770) (← links)
- Homotopy type-theoretic interpretations of constructive set theories (Q5156772) (← links)
- Univalent Foundations of Mathematics and Paraconsistency (Q5241529) (← links)
- On Small Types in Univalent Foundations (Q6135756) (← links)
- Towards a constructive simplicial model of Univalent Foundations (Q6176777) (← links)
- Kripke-Joyal forcing for type theory and uniform fibrations (Q6586829) (← links)