notes

newt/eq.newt

@@ -1,7 +1,6 @@
 module Equality
 
 -- Leibniz equality
-
 Eq : {A : U} -> A -> A -> U
 Eq = \ {A} x y => (P : A -> U) -> P x -> P y
 
@@ -11,6 +10,8 @@ refl = \ P Px => Px
 trans : {A : U} {x y z : A} -> Eq x y -> Eq y z -> Eq x z
 trans = \ Exy Eyz => Eyz (\ w => Eq x w) Exy
 
+-- This version has a universe issue, see Abel et al for
+-- a better one
 sym : {A : U} {x y : A} -> Eq x y -> Eq y x
 sym = \ Exy => Exy (\ z => Eq z x) refl
 
@@ -20,10 +21,24 @@ id = \ x => x
 coerce : {A B : U} -> Eq A B -> A -> B
 coerce = \ EqAB a => EqAB id a
 
+-- pi-forall's formulation
 -- J : {A : U} ->
---     {C : (x y : A) -> Eq x y -> U} ->
---     (c : (x : _) -> C x x refl) ->
 --     (x y : A) ->
 --     (p : Eq x y) ->
---     C x y p
--- J = \ c x y eq => eq (\ z => C x z _) (c x)
+--     {C : (z : A) -> Eq z y -> U} ->
+--     (b : C y refl) ->
+--     C x p
+-- -- doesn't really work because we have refl and some Eq y y
+-- J = \ x y eq {C} b => eq (\z => (q : Eq z y) -> C z q) (\ _ => b)
+
+-- I don't think this is going to happen, maybe with funext?
+-- anyway, could be useful case to improve error messages.
+-- (add names)
+
+J : {A : U} ->
+    {C : (x y : A) -> Eq x y -> U} ->
+    (c : (x : _) -> C x x refl) ->
+    (x y : A) ->
+    (p : Eq x y) ->
+    C x y p
+J = \ c x y eq => eq (\ z => (q : Eq x z) -> C x z q) (\ _ => c x) eq