module Equality1

-- Leibniz equality
Eq : {A : U} -> A -> A -> U
Eq = \ x y => (P : A -> U) -> P x -> P y

refl : {A : U} {x : A} -> Eq x x
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

sym : {A : U} {x y : A} -> Eq x y -> Eq y x
sym = \ Exy => Exy (\ z => Eq z x) refl

id : {A} -> A -> A
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} ->
--     (x y : A) ->
--     (p : Eq x y) ->
--     {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
