Mercurial > hg > Members > kono > Proof > category
changeset 872:bfe0215593b9
decidablity of < f , g > is required
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 09 Apr 2020 07:54:18 +0900 |
| parents | 4d50d51e9410 |
| children | 0b5fb015009c |
| files | CCCGraph1.agda |
| diffstat | 1 files changed, 10 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph1.agda Wed Apr 08 17:49:57 2020 +0900 +++ b/CCCGraph1.agda Thu Apr 09 07:54:18 2020 +0900 @@ -68,17 +68,17 @@ refl-<r> refl = refl _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c - id a ・ g = eval g + id a ・ g = g ○ a ・ g = ○ _ < f , g > ・ h = < f ・ h , g ・ h > - iv f (id _) ・ h = eval ( iv f h ) + iv f (id _) ・ h = iv f h iv π < g , g₁ > ・ h = g ・ h iv π' < g , g₁ > ・ h = g₁ ・ h iv ε < g , g₁ > ・ h = iv ε < g ・ h , g₁ ・ h > iv (f *) < g , g₁ > ・ h = iv (f *) < g ・ h , g₁ ・ h > iv f ( (○ a)) ・ g = iv f ( ○ _ ) - iv x y ・ id a = eval (iv x y) - iv f (iv f₁ g) ・ h with eval (iv f₁ g ・ h ) + iv x y ・ id a = iv x y + iv f (iv f₁ g) ・ h with iv f₁ g ・ h (iv f (iv f₁ g) ・ h) | id a = iv f (id a) (iv f (iv f₁ g) ・ h) | ○ a = iv f (○ a) (iv π (iv f₁ g) ・ h) | < t , t₁ > = t @@ -100,7 +100,7 @@ identityR {_} {_} {iv π' < g , g₁ >} = identityR {_} {_} {g₁} identityR {_} {_} {iv ε < f , f₁ >} = cong₂ (λ j k → iv ε < j , k > ) (identityR {_} {_} {f} ) (identityR {_} {_} {f₁}) identityR {_} {_} {iv (x *) < f , f₁ >} = cong₂ (λ j k → iv (x *) < j , k > ) (identityR {_} {_} {f} ) (identityR {_} {_} {f₁}) - identityR {_} {_} {iv f (iv g h)} = {!!} + identityR {_} {_} {iv f (iv g h)} = refl open import Data.Empty open import Relation.Nullary @@ -162,7 +162,7 @@ -- lemma = std-iv f f₁ t {!!} assoc-iv : {a b c d : Objs} (x : Arrow c d) (f : Arrows b c) (g : Arrows a b ) → eval (iv x (f ・ g)) ≡ eval (iv x f ・ g) - assoc-iv x (id a) g = {!!} + assoc-iv x (id a) g = refl assoc-iv x (○ a) g = refl assoc-iv π < f , f₁ > g = refl assoc-iv π' < f , f₁ > g = refl @@ -197,10 +197,10 @@ identityL {_} {_} {id a} = refl identityL {_} {_} {○ a} = refl identityL {a} {b} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) (identityL {_} {_} {f}) (identityL {_} {_} {f₁}) - identityL {_} {_} {iv f f₁} = {!!} + identityL {_} {_} {iv f f₁} = refl associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) → (f ・ (g ・ h)) == ((f ・ g) ・ h) - associative (id a) g h = {!!} + associative (id a) g h = refl associative (○ a) g h = refl associative (< f , f1 > ) g h = cong₂ ( λ j k → < j , k > ) (associative f g h) (associative f1 g h) associative {a} (iv π < f , f1 > ) g h = associative f g h @@ -209,11 +209,11 @@ associative {a} (iv (x *) < f , f1 > ) g h = cong ( λ k → iv (x *) k ) ( associative < f , f1 > g h ) associative {a} (iv x (id _)) g h = begin eval (iv x (id _) ・ (g ・ h)) - ≡⟨ {!!} ⟩ + ≡⟨⟩ eval (iv x (g ・ h)) ≡⟨ assoc-iv x g h ⟩ eval (iv x g ・ h) - ≡⟨ {!!} ⟩ + ≡⟨⟩ eval ((iv x (id _) ・ g) ・ h) ∎ where open ≡-Reasoning associative {a} (iv x (○ _)) g h = refl