From e3fd260f313dce3fd2769aad27705b69b57b90d7 Mon Sep 17 00:00:00 2001
From: Sergei Winitzki <winitzki@gmail.com>
Date: Fri, 22 Nov 2024 20:57:44 +0100
Subject: [PATCH] wip

---
 tutorial/LeibnizEquality.dhall | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/tutorial/LeibnizEquality.dhall b/tutorial/LeibnizEquality.dhall
index 4c302f0d..c7d9c190 100644
--- a/tutorial/LeibnizEquality.dhall
+++ b/tutorial/LeibnizEquality.dhall
@@ -105,11 +105,21 @@ let toAssertType =
             = x Equals_a refl_a
 
         in  result
-
+{-  -- This does not type-check because Dhall does not use equality evidence for type-checking.
+-- The error is: the result must have type ResT x y eq, but it has type ResT x x refl.
+-}
+let eliminatorJ
+  : ∀(A : Type) → ∀(ResT : ∀(x : A) → ∀(y : A) → LeibnizEqual A x y → Type) → ∀(f : ∀(x : A) → ResT x x (refl A x)) → ∀(x : A) → ∀(y : A) → ∀(eq : LeibnizEqual A x y) → ResT x y eq
+  = λ(A : Type) → λ(ResT : ∀(x : A) → ∀(y : A) → LeibnizEqual A x y → Type) → λ(f : ∀(x : A) → ResT x x (refl A x)) → λ(x : A) → λ(y : A) → λ(eq : LeibnizEqual A x y) →
+    let fx : ResT x x (refl A x) = f x
+    let result1 : ResT x y (refl A x) = eq (λ(a : A) → ResT x a (refl A x)) fx
+    in result1
+{- -}
 in  { LeibnizEqual
     , reflexivity = refl
     , symmetry
     , transitivity
     , extensional_equality
     , toAssertType
+    -- , eliminatorJ
     }