On generalized algebraic theories and categories with families (Q5084311): Difference between revisions

@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Q3937387
@@ Property / cites work: Q3937387 / rank @@
+Normal rank
@@ Property / cites work @@
+Type theory in type theory using quotient inductive types
+Normal rank
@@ Property / cites work @@
+Impredicative Encodings of (Higher) Inductive Types
+Normal rank
@@ Property / cites work @@
+Q5762080
@@ Property / cites work: Q5762080 / rank @@
+Normal rank
@@ Property / cites work @@
+Generalized algebraic theories and contextual categories
+Normal rank
@@ Property / cites work @@
+Q5277836
@@ Property / cites work: Q5277836 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4596801
@@ Property / cites work: Q4596801 / rank @@
+Normal rank
@@ Property / cites work @@
+Categories with Families: Unityped, Simply Typed, and Dependently Typed
+Normal rank
@@ Property / cites work @@
+The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
+Normal rank
@@ Property / cites work @@
+The biequivalence of locally cartesian closed categories and Martin-Löf type theories
+Normal rank
@@ Property / cites work @@
+Revisiting the categorical interpretation of dependent type theory
+Normal rank
@@ Property / cites work @@
+Internal type theory
@@ Property / cites work: Internal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive-Inductive Definitions
@@ Property / cites work: Inductive-Inductive Definitions / rank @@
+Normal rank
@@ Property / cites work @@
+Q5731806
@@ Property / cites work: Q5731806 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4474857
@@ Property / cites work: Q4474857 / rank @@
+Normal rank
@@ Property / cites work @@
+Conservativity of equality reflection over intensional type theory
+Normal rank
@@ Property / cites work @@
+Q4225149
@@ Property / cites work: Q4225149 / rank @@
+Normal rank
@@ Property / cites work @@
+Extensional Constructs in Intensional Type Theory
@@ Property / cites work: Extensional Constructs in Intensional Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Large and Infinitary Quotient Inductive-Inductive Types
+Normal rank
@@ Property / cites work @@
+Q3688389
@@ Property / cites work: Q3688389 / 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 @@
+Q3216629
@@ Property / cites work: Q3216629 / rank @@
+Normal rank
@@ Property / cites work @@
+On functors expressible in the polymorphic typed lambda calculus
+Normal rank
@@ Property / cites work @@
+Q5286647
@@ Property / cites work: Q5286647 / rank @@
+Normal rank
@@ Property / cites work @@
+Subsystems and regular quotients of C-systems
@@ Property / cites work: Subsystems and regular quotients of C-systems / rank @@
+Normal rank