Canonicity and homotopy canonicity for cubical type theory (Q5028486): Difference between revisions

@@ label / en / label / en @@
+Canonicity and homotopy canonicity for cubical type theory
@@ Property / arXiv classification @@
+math.LO
@@ Property / arXiv classification: math.LO / rank @@
+Normal rank
@@ Property / arXiv classification @@
+cs.LO
@@ Property / arXiv classification: cs.LO / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.06572
@@ Property / arXiv ID: 1902.06572 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4944846
@@ Property / cites work: Q4944846 / 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 @@
+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 @@
+Canonicity and normalization for dependent type theory
+Normal rank
@@ Property / cites work @@
+Internal type theory
@@ Property / cites work: Internal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Polynomial functors and polynomial monads
@@ Property / cites work: Polynomial functors and polynomial monads / rank @@
+Normal rank
@@ Property / cites work @@
+The Frobenius condition, right properness, and uniform fibrations
+Normal rank
@@ Property / cites work @@
+Q5580926
@@ Property / cites work: Q5580926 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4225149
@@ Property / cites work: Q4225149 / rank @@
+Normal rank
@@ Property / cites work @@
+Canonicity for cubical type theory
@@ Property / cites work: Canonicity for cubical type theory / rank @@
+Normal rank
@@ Property / cites work @@
+A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
+Normal rank
@@ Property / cites work @@
+The simplicial model of univalent foundations (after Voevodsky)
+Normal rank
@@ Property / cites work @@
+A cubical approach to straightening
@@ Property / cites work: A cubical approach to straightening / rank @@
+Normal rank
@@ Property / cites work @@
+Q4993352
@@ Property / cites work: Q4993352 / rank @@
+Normal rank
@@ Property / cites work @@
+Semantics of higher inductive types
@@ Property / cites work: Semantics of higher inductive types / rank @@
+Normal rank
@@ Property / cites work @@
+Q5278410
@@ Property / cites work: Q5278410 / rank @@
+Normal rank
@@ Property / cites work @@
+Partial Horn logic and Cartesian categories
@@ Property / cites work: Partial Horn logic and Cartesian categories / rank @@
+Normal rank
@@ Property / cites work @@
+A type theory for synthetic $\infty$-categories
@@ Property / cites work: A type theory for synthetic $\infty$-categories / rank @@
+Normal rank
@@ Property / cites work @@
+Univalence for inverse diagrams and homotopy canonicity
+Normal rank
@@ Property / cites work @@
+Q5286647
@@ Property / cites work: Q5286647 / rank @@
+Normal rank
@@ Property / cites work @@
+An algebraic weak factorisation system on 01-substitution sets: a constructive proof
+Normal rank
@@ Property / cites work @@
+Intensional interpretations of functionals of finite type I
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank