Leibniz equality is isomorphic to Martin-Löf identity, parametrically (Q5120232): Difference between revisions

@@ Property / cites work @@
+A relationally parametric model of dependent type theory
+Normal rank
@@ Property / cites work @@
+A presheaf model of parametric type theory
@@ Property / cites work: A presheaf model of parametric type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Parametricity and dependent types
@@ Property / cites work: Parametricity and dependent types / rank @@
+Normal rank
@@ Property / cites work @@
+Proofs for free
@@ Property / cites work: Proofs for free / rank @@
+Normal rank
@@ Property / cites work @@
+Pattern matching without K
@@ Property / cites work: Pattern matching without K / rank @@
+Normal rank
@@ Property / cites work @@
+Unifiers as equivalences: proof-relevant unification of dependently typed data
+Normal rank
@@ Property / cites work @@
+Cubical Type Theory: a constructive interpretation of the univalence axiom
+Normal rank
@@ Property / cites work @@
+Categorical data types in parametric polymorphism
@@ Property / cites work: Categorical data types in parametric polymorphism / rank @@
+Normal rank
@@ Property / cites work @@
+Q4247303
@@ Property / cites work: Q4247303 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4099613
@@ Property / cites work: Q4099613 / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank
@@ Property / cites work @@
+The Girard-Reynolds isomorphism (second edition)
@@ Property / cites work: The Girard-Reynolds isomorphism (second edition) / rank @@
+Normal rank