--- a/a02/agda/equality.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/a02/agda/equality.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -1,26 +1,26 @@
 module equality where
 
 
-data _==_ {A : Set } : A → A → Set where
-   refl :  {x : A} → x == x
+data _≡_ {A : Set } : A → A → Set where
+   refl :  {x : A} → x ≡ x
 
-ex1 : {A : Set} {x : A } → x == x
+ex1 : {A : Set} {x : A } → x ≡ x
 ex1  = ?
 
-ex2 : {A : Set} {x y : A } → x == y → y == x
+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 : {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 : {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 : 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 {!!}
+-- 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 {!!}