Two-level type theory and applications (Q6149950): Difference between revisions

@@ Property / cites work @@
+A Higher Structure Identity Principle
@@ Property / cites work: A Higher Structure Identity Principle / 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 @@
+Partiality, Revisited
@@ Property / cites work: Partiality, Revisited / rank @@
+Normal rank
@@ Property / cites work @@
+Type theory in type theory using quotient inductive types
+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 @@
+Homotopy invariant algebraic structures on topological spaces
+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 @@
+Internal type theory
@@ Property / cites work: Internal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Quasi-unital \(\infty\)-categories
@@ Property / cites work: Quasi-unital \(\infty\)-categories / rank @@
+Normal rank
@@ Property / cites work @@
+Q4225149
@@ Property / cites work: Q4225149 / rank @@
+Normal rank
@@ Property / cites work @@
+Quasi-categories and Kan complexes
@@ Property / cites work: Quasi-categories and Kan complexes / rank @@
+Normal rank
@@ Property / cites work @@
+Q5216301
@@ Property / cites work: Q5216301 / rank @@
+Normal rank
@@ Property / cites work @@
+The General Universal Property of the Propositional Truncation
+Normal rank
@@ Property / cites work @@
+Q4993352
@@ Property / cites work: Q4993352 / rank @@
+Normal rank
@@ Property / cites work @@
+A minimalist two-level foundation for constructive mathematics
+Normal rank
@@ Property / cites work @@
+Q4611379
@@ Property / cites work: Q4611379 / rank @@
+Normal rank
@@ Property / cites work @@
+A model for the homotopy theory of homotopy theory
+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 @@
+The theory and practice of Reedy categories
@@ Property / cites work: The theory and practice of Reedy categories / rank @@
+Normal rank
@@ Property / cites work @@
+The univalence axiom for elegant Reedy presheaves
@@ Property / cites work: The univalence axiom for elegant Reedy presheaves / rank @@
+Normal rank
@@ Property / cites work @@
+Univalence for inverse diagrams and homotopy canonicity
+Normal rank
@@ Property / cites work @@
+Brouwer's fixed-point theorem in real-cohesive homotopy type theory
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank