Mercurial > hg > Members > kono > Proof > category
changeset 844:3b8c1ca0d737
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 02 Apr 2020 20:42:18 +0900 |
| parents | a73acfdef643 |
| children | 0c81ded4a734 |
| files | CCCGraph1.agda |
| diffstat | 1 files changed, 14 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph1.agda Thu Apr 02 13:43:43 2020 +0900 +++ b/CCCGraph1.agda Thu Apr 02 20:42:18 2020 +0900 @@ -21,7 +21,6 @@ data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i arrow : {a b : vertex G} → (edge G) a b → Arrow (atom a) (atom b) - ○ : (a : Objs ) → Arrow a ⊤ π : {a b : Objs } → Arrow ( a ∧ b ) a π' : {a b : Objs } → Arrow ( a ∧ b ) b ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a @@ -29,18 +28,20 @@ data Arrows : (b c : Objs ) → Set ( c₁ ⊔ c₂ ) where id : ( a : Objs ) → Arrows a a --- case i + ○ : ( a : Objs ) → Arrows a ⊤ --- case i <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b) --- case iii iv : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c -- cas iv _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c id a ・ g = g + ○ a ・ g = ○ _ < f , g > ・ h = < f ・ h , g ・ h > iv f (id _) ・ h = iv f h - iv (○ a) g ・ h = iv (○ _) (id _) 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 f (iv f₁ g) ・ h = iv f ( (iv f₁ g) ・ h ) _==_ : {a b : Objs } → ( x y : Arrows a b ) → Set (c₁ ⊔ c₂) @@ -63,15 +64,23 @@ } where identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) == f identityL {_} {_} {id a} = refl + identityL {_} {_} {○ a} = refl identityL {a} {b} {< f , f₁ >} = refl identityL {_} {_} {iv f f₁} = refl + identyR-iv : {a b c d : Objs} (x : Arrow c d ) (f : Arrow b c) (f₁ : Arrows a b ) → iv x (iv f f₁) ・ id a ≡ iv x ((iv f f₁) ・ id a) + identyR-iv (arrow x) f f₁ = refl + identyR-iv π f f₁ = refl + identyR-iv π' f f₁ = refl + identyR-iv ε f f₁ = refl + identyR-iv (x *) f f₁ = refl identityR≡ : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f identityR≡ {a} {.a} {id a} = refl + identityR≡ {a} {⊥} {○ a} = refl identityR≡ {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) (identityR≡ {a} {_} {f} ) (identityR≡ {a} {_} {f₁} ) identityR≡ {a} {b} {iv x (id a)} = refl - identityR≡ {a} {b} {iv π < f , f₁ >} = {!!} + identityR≡ {a} {b} {iv x (○ a)} = refl + identityR≡ {a} {b} {iv π < f , f₁ >} = ? identityR≡ {a} {b} {iv π' < f , f₁ >} = {!!} - identityR≡ {a} {⊤} {iv (○ .(_ ∧ _)) < f , f₁ >} = {!!} identityR≡ {a} {b} {iv ε < f , f₁ >} = cong ( λ k → iv ε k ) ( identityR≡ {_} {_} {< f , f₁ >} ) identityR≡ {a} {_} {iv (x *) < f , f₁ >} = cong ( λ k → iv (x *) k ) ( identityR≡ {_} {_} {< f , f₁ >} ) identityR≡ {a} {b} {iv {a} {c} {d} x (iv {a} {d} {c1} f f₁)} = begin -- cong ( λ k → iv x k ・ id a ) {!!} -- ( identityR {_} {_} {iv f f₁} ) @@ -86,6 +95,7 @@ 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 = 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 (iv x f) g h = {!!} -- cong ( λ k → iv x k ) ( associative f g h )