--- a/a02/agda/equality.agda	Sat Mar 14 19:42:27 2020 +0900
+++ b/a02/agda/equality.agda	Sun Dec 27 13:26:44 2020 +0900
@@ -19,8 +19,8 @@
 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 {!!} {!!} {!!}
+-- 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 {!!}