Mercurial > hg > Members > kono > Proof > category
changeset 846:4013cbfdd15e
idR
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 03 Apr 2020 16:03:46 +0900 |
| parents | 0c81ded4a734 |
| children | f2729064016d |
| files | CCCGraph1.agda |
| diffstat | 1 files changed, 14 insertions(+), 31 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph1.agda Thu Apr 02 20:55:29 2020 +0900 +++ b/CCCGraph1.agda Fri Apr 03 16:03:46 2020 +0900 @@ -36,6 +36,7 @@ id a ・ g = g ○ a ・ g = ○ _ < f , g > ・ h = < f ・ h , g ・ h > + f ・ id b = f iv f (id _) ・ h = iv f h iv π < g , g₁ > ・ h = g ・ h iv π' < g , g₁ > ・ h = g₁ ・ h @@ -57,7 +58,7 @@ eval ( iv f (iv f₁ g) ) = iv f ( iv f₁ (eval g)) _==_ : {a b : Objs } → ( x y : Arrows a b ) → Set (c₁ ⊔ c₂) - _==_ {a} {b} x y = eval x ≡ eval y + _==_ {a} {b} x y = (x ・ id _ ) ≡ ( y ・ id _ ) PL : Category (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂) PL = record { @@ -79,45 +80,27 @@ 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 x (○ a)} = refl - identityR≡ {a} {b} {iv π < f , f₁ >} = {!!} - identityR≡ {a} {b} {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₁} ) - iv x (iv f f₁) ・ id a - ≡⟨ {!!} ⟩ - iv x ((iv f f₁) ・ id a) - ≡⟨ cong (λ k → iv x k) identityR≡ ⟩ - iv x (iv f f₁) - ∎ where open ≡-Reasoning + identityR≡ {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR≡ identityR≡ + identityR≡ {a} {b} {iv x y} = 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 {_} {_} {f} ) ( identityR {_} {_} {f₁} ) - identityR {a} {.(atom _)} {iv (arrow x) f₁} = {!!} - identityR {a} {b} {iv π f₁} = {!!} - identityR {a} {b} {iv π' f₁} = {!!} - identityR {a} {b} {iv ε f₁} = {!!} - identityR {a} {.(_ <= _)} {iv (f *) f₁} = ? + identityR {a} {b} {f} = cong ( λ k → k ・ id a ) ( identityR≡ {_} {_} {f} ) 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 ) - + associative {a} (iv x f) g h = begin + (iv x f ・ (g ・ h)) ・ id a + ≡⟨ {!!} ⟩ + iv x ((f ・ (g ・ h)) ・ id a) + ≡⟨ cong ( λ k → iv x k ) ( associative f g h ) ⟩ + iv x (((f ・ g) ・ h) ・ id a) + ≡⟨ {!!} ⟩ + ((iv x f ・ g) ・ h) ・ id a + ∎ where open ≡-Reasoning o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} → f == g → h == i → (h ・ f) == (i ・ g) o-resp-≈ f=g h=i = {!!}