|
138
|
1 module equality where
|
|
|
2
|
|
|
3
|
|
406
|
4 data _≡_ {A : Set } : A → A → Set where
|
|
|
5 refl : {x : A} → x ≡ x
|
|
138
|
6
|
|
406
|
7 ex1 : {A : Set} {x : A } → x ≡ x
|
|
330
|
8 ex1 = ?
|
|
138
|
9
|
|
406
|
10 ex2 : {A : Set} {x y : A } → x ≡ y → y ≡ x
|
|
330
|
11 ex2 = ?
|
|
138
|
12
|
|
406
|
13 ex3 : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z
|
|
138
|
14 ex3 = {!!}
|
|
|
15
|
|
406
|
16 ex4 : {A B : Set} {x y : A } { f : A → B } → x ≡ y → f x ≡ f y
|
|
138
|
17 ex4 = {!!}
|
|
|
18
|
|
406
|
19 subst : {A : Set } → { x y : A } → ( f : A → Set ) → x ≡ y → f x → f y
|
|
139
|
20 subst {A} {x} {y} f refl fx = fx
|
|
|
21
|
|
406
|
22 -- ex5 : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z
|
|
|
23 -- ex5 {A} {x} {y} {z} x≡y y≡z = subst (λ refl → {!!} ) x≡y {!!}
|
|
138
|
24
|
|
|
25
|
|
139
|
26
|
