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 {!!}