43 lines
1.1 KiB
Plaintext
43 lines
1.1 KiB
Plaintext
module Equality
|
|
|
|
-- 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
|