Mercurial > hg > Members > kono > Proof > automaton
view a02/agda/equality.agda @ 139:3be1afb87f82
add utm
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 14 Mar 2020 17:34:54 +0900 |
parents | 7a0634a7c25a |
children | b3f05cd08d24 |
line wrap: on
line source
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 {!!} {!!} {!!}