Naive cubical type theory (Q5055495): Difference between revisions

@@ Property / describes a project that uses @@
+GitHub
@@ Property / describes a project that uses: GitHub / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+cart-cube
@@ Property / describes a project that uses: cart-cube / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+cubicaltt
@@ Property / describes a project that uses: cubicaltt / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2985011261
@@ Property / OpenAlex ID: W2985011261 / rank @@
+Normal rank
@@ Property / cites work @@
+Naïve Type Theory
@@ Property / cites work: Naïve Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Syntax and models of Cartesian cubical type theory
+Normal rank
@@ Property / cites work @@
+A cubical model of homotopy type theory
@@ Property / cites work: A cubical model of homotopy type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopy theoretic models of identity types
@@ Property / cites work: Homotopy theoretic models of identity types / rank @@
+Normal rank
@@ Property / cites work @@
+Q2968413
@@ Property / cites work: Q2968413 / rank @@
+Normal rank
@@ Property / cites work @@
+Cubical Type Theory: a constructive interpretation of the univalence axiom
+Normal rank
@@ Property / cites work @@
+Q4823137
@@ Property / cites work: Q4823137 / rank @@
+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 @@
+Q4773706
@@ Property / cites work: Q4773706 / rank @@
+Normal rank
@@ Property / cites work @@
+UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY
@@ Property / cites work: UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY / rank @@
+Normal rank
@@ Property / cites work @@
+Weak omega-categories from intensional type theory
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank
@@ Property / cites work @@
+Cubical Agda: A dependently typed programming language with univalence and higher inductive types
+Normal rank