A general formulation of simultaneous inductive-recursive definitions in type theory (Q4508246): Difference between revisions

@@ Property / Wikidata QID @@
+Q59540955
@@ Property / Wikidata QID: Q59540955 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5573965
@@ Property / cites work: Q5573965 / rank @@
+Normal rank
@@ Property / cites work @@
+Inaccessibility in constructive set theory and type theory
+Normal rank
@@ Property / cites work @@
+A TYPE-FREE THEORY OF HALF-MONOTONE INDUCTIVE DEFINITIONS
+Normal rank
@@ Property / cites work @@
+Inductive families
@@ Property / cites work: Inductive families / rank @@
+Normal rank
@@ Property / cites work @@
+Normalization and the Yoneda embedding
@@ Property / cites work: Normalization and the Yoneda embedding / rank @@
+Normal rank
@@ Property / cites work @@
+Intuitionistic model constructions and normalization proofs
+Normal rank
@@ Property / cites work @@
+Propositional functions and families of types
@@ Property / cites work: Propositional functions and families of types / rank @@
+Normal rank
@@ Property / cites work @@
+The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
+Normal rank