Q5091148 (Q5091148): Difference between revisions

@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Impredicative Encodings of (Higher) Inductive Types
+Normal rank
@@ Property / cites work @@
+Propositions as [Types]
@@ Property / cites work: Propositions as [Types] / rank @@
+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 @@
+Modal dependent type theory and dependent right adjoints
+Normal rank
@@ Property / cites work @@
+Varieties of Cubical Sets
@@ Property / cites work: Varieties of Cubical Sets / 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 calculus of constructions
@@ Property / cites work: The calculus of constructions / rank @@
+Normal rank
@@ Property / cites work @@
+Internal type theory
@@ Property / cites work: Internal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+A homotopy-theoretic model of function extensionality in the effective topos
+Normal rank
@@ Property / cites work @@
+The Frobenius condition, right properness, and uniform fibrations
+Normal rank
@@ Property / cites work @@
+Understanding the small object argument
@@ Property / cites work: Understanding the small object argument / rank @@
+Normal rank
@@ Property / cites work @@
+Q3994895
@@ Property / cites work: Q3994895 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4247303
@@ Property / cites work: Q4247303 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3671978
@@ Property / cites work: Q3671978 / rank @@
+Normal rank
@@ Property / cites work @@
+A small complete category
@@ Property / cites work: A small complete category / rank @@
+Normal rank
@@ Property / cites work @@
+Comprehension categories and the semantics of type dependency
+Normal rank
@@ Property / cites work @@
+Categorical logic and type theory
@@ Property / cites work: Categorical logic and type theory / rank @@
+Normal rank
@@ Property / cites work @@
+The homotopy theory of type theories
@@ Property / cites work: The homotopy theory of type theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q4993352
@@ Property / cites work: Q4993352 / rank @@
+Normal rank
@@ Property / cites work @@
+Constructive natural deduction and its ‘ω-set’ interpretation
+Normal rank
@@ Property / cites work @@
+Q5278410
@@ Property / cites work: Q5278410 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4611379
@@ Property / cites work: Q4611379 / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank
@@ Property / cites work @@
+An algebraic weak factorisation system on 01-substitution sets: a constructive proof
+Normal rank
@@ Property / cites work @@
+Realizability. An introduction to its categorical side
+Normal rank