module equality where


data _==_ {A : Set } : A → A → Set where
   refl :  {x : A} → x == x

ex1 : {A : Set} {x : A } → x == x
ex1  = ?

ex2 : {A : Set} {x y : A } → x == y → y == x
ex2 = ?

ex3 : {A : Set} {x y z : A } → x == y → y == z → x == z
ex3 = {!!}

ex4 : {A B : Set} {x y : A } { f : A → B } →   x == y → f x == f y
ex4 = {!!}

subst : {A : Set } → { x y : A } → ( f : A → Set ) → x == y → f x → f y
subst {A} {x} {y} f refl fx = fx

-- ex5 :   {A : Set} {x y z : A } →  x == y → y == z → x == z
-- ex5 {A} {x} {y} {z} x==y y==z = subst (λ refl  → {!!} ) x==y {!!}