Model structure on the universe of all types in interval type theory (Q5022925): Difference between revisions

@@ Property / describes a project that uses @@
+cart-cube
@@ Property / describes a project that uses: cart-cube / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Quotient inductive-inductive types
@@ Property / cites work: Quotient inductive-inductive types / rank @@
+Normal rank
@@ Property / cites work @@
+Q5278407
@@ Property / cites work: Q5278407 / rank @@
+Normal rank
@@ Property / cites work @@
+Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
+Normal rank
@@ Property / cites work @@
+Q2968413
@@ Property / cites work: Q2968413 / rank @@
+Normal rank
@@ Property / cites work @@
+The univalence axiom in cubical sets
@@ Property / cites work: The univalence axiom in cubical sets / rank @@
+Normal rank
@@ Property / cites work @@
+Q5277833
@@ Property / cites work: Q5277833 / rank @@
+Normal rank
@@ Property / cites work @@
+Cubical Type Theory: a constructive interpretation of the univalence axiom
+Normal rank
@@ Property / cites work @@
+On Higher Inductive Types in Cubical Type Theory
@@ Property / cites work: On Higher Inductive Types in Cubical Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+The identity type weak factorisation system
@@ Property / cites work: The identity type weak factorisation system / rank @@
+Normal rank
@@ Property / cites work @@
+The Frobenius condition, right properness, and uniform fibrations
+Normal rank
@@ Property / cites work @@
+Q4790109
@@ Property / cites work: Q4790109 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4225149
@@ Property / cites work: Q4225149 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5428640
@@ Property / cites work: Q5428640 / rank @@
+Normal rank
@@ Property / cites work @@
+The simplicial model of univalent foundations (after Voevodsky)
+Normal rank
@@ Property / cites work @@
+Q4993352
@@ Property / cites work: Q4993352 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4611379
@@ Property / cites work: Q4611379 / rank @@
+Normal rank
@@ Property / cites work @@
+An algebraic weak factorisation system on 01-substitution sets: a constructive proof
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1017/s0960129520000213
+Normal rank
@@ Property / OpenAlex ID @@
+W3119304695
@@ Property / OpenAlex ID: W3119304695 / rank @@
+Normal rank