Mercurial > hg > Members > kono > Proof > category
changeset 852:425eda25ff8c
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 04 Apr 2020 17:51:01 +0900 |
| parents | f4f5ce90d3af |
| children | efdb09dc9972 |
| files | CCCGraph1.agda |
| diffstat | 1 files changed, 28 insertions(+), 97 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph1.agda Sat Apr 04 13:40:35 2020 +0900 +++ b/CCCGraph1.agda Sat Apr 04 17:51:01 2020 +0900 @@ -32,19 +32,6 @@ <_,_> : {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 - < f , g > ・ h = < f ・ h , g ・ 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 = iv x y - iv f (iv f₁ g) ・ h = iv f ( (iv f₁ g) ・ h ) - ○ a ・ g = ○ _ - eval : {a b : Objs } (f : Arrows a b ) → Arrows a b eval (id a) = id a eval (○ a) = ○ a @@ -53,78 +40,36 @@ eval (iv π' < f , g > ) = eval g eval (iv f g) = iv f (eval g) + _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c + id a ・ g = eval g + < f , g > ・ h = < f ・ h , g ・ h > + iv f (id _) ・ h = iv f (eval 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 = iv x (eval y) + iv f (iv f₁ g) ・ h = iv f ( iv f₁ g ・ h ) + ○ a ・ g = ○ _ + _==_ : {a b : Objs } → ( x y : Arrows a b ) → Set (c₁ ⊔ c₂) _==_ {a} {b} x y = eval x ≡ eval y - 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≡ identityR≡ - identityR≡ {a} {b} {iv x (id a)} = refl - identityR≡ {a} {b} {iv x (○ a)} = refl - identityR≡ {a} {_} {iv π < f , g >} = begin - iv π < f , g > ・ id a - ≡⟨⟩ - f ・ id a - ≡⟨ identityR≡ ⟩ - f - ≡⟨ {!!} ⟩ - iv π < f , g > - ∎ where open ≡-Reasoning - identityR≡ {a} {b} {iv π' < f , g >} = {!!} - identityR≡ {a} {b} {iv ε < f , g >} = cong₂ ( λ j k → iv ε < j , k > ) identityR≡ identityR≡ - identityR≡ {a} {_} {iv (x *) < f , g >} = cong₂ ( λ j k → iv (x *) < j , k > ) identityR≡ identityR≡ - identityR≡ {a} {b} {iv x (iv f y)} = refl identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) == f - identityR {a} {b} {f} = {!!} -- cong ( λ k → k ・ id a ) ( identityR≡ {_} {_} {f} ) - - ≡←== : {A B : Objs} {f g : Arrows A B} → f == g → f ≡ g - ≡←== eq = subst₂ (λ j k → j ≡ k ) identityR≡ identityR≡ {!!} + 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} {b} {iv f (id a)} = refl + identityR {a} {b} {iv f (○ a)} = refl + identityR {a} {b} {iv π < g , g₁ >} = {!!} + identityR {a} {b} {iv π' < g , g₁ >} = {!!} + identityR {a} {b} {iv ε < f , f₁ >} = cong₂ (λ j k → iv ε < j , k > ) (identityR {_} {_} {f} ) (identityR {_} {_} {f₁}) + identityR {a} {_} {iv (x *) < f , f₁ >} = cong₂ (λ j k → iv (x *) < j , k > ) (identityR {_} {_} {f} ) (identityR {_} {_} {f₁}) + identityR {a} {b} {iv f (iv g h)} = {!!} ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g - ==←≡ eq = {!!} -- cong (λ k → k ・ id _) eq - - assoc-iv : {a b c d : Objs} (x : Arrow c d ) (f : Arrows b c ) ( g : Arrows a b ) → iv x f ・ g ≡ iv x ( f ・ g ) - assoc-iv x f (id _) = begin - iv x f ・ id _ - ≡⟨ identityR≡ ⟩ - iv x f - ≡⟨ sym (cong (λ k → iv x k ) identityR≡) ⟩ - iv x (f ・ id _) - ∎ where open ≡-Reasoning - assoc-iv x (id a) g = refl - assoc-iv x (○ a) g = refl - assoc-iv π < f , f₁ > g = begin - iv π < f , f₁ > ・ g - ≡⟨⟩ - f ・ g - ≡⟨ sym identityR≡ ⟩ - (f ・ g) ・ id _ - ≡⟨⟩ - iv π < f ・ g , f₁ ・ g > ・ id _ - ≡⟨ identityR≡ ⟩ - iv π < f ・ g , f₁ ・ g > - ≡⟨⟩ - iv π (< f , f₁ > ・ g) - ∎ where open ≡-Reasoning - assoc-iv π' < f , f₁ > g = begin - iv π' < f , f₁ > ・ g - ≡⟨⟩ - f₁ ・ g - ≡⟨ sym identityR≡ ⟩ - (f₁ ・ g) ・ id _ - ≡⟨⟩ - iv π' < f ・ g , f₁ ・ g > ・ id _ - ≡⟨ identityR≡ ⟩ - iv π' < f ・ g , f₁ ・ g > - ≡⟨⟩ - iv π' (< f , f₁ > ・ g) - ∎ where open ≡-Reasoning - assoc-iv ε < f , f₁ > g = refl - assoc-iv (x *) < f , f₁ > g = refl - assoc-iv x (iv f f₁) (○ a) = refl - assoc-iv x (iv f f₁) < g , g₁ > = refl - assoc-iv x (iv f f₁) (iv f₂ g) = refl + ==←≡ eq = cong (λ k → eval k ) eq PL : Category (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂) PL = record { @@ -144,28 +89,14 @@ 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 + identityL {a} {b} {< f , f₁ >} = {!!} + identityL {_} {_} {iv f 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 (id a) g h = {!!} 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 x f) g h = {!!} - -- begin - -- (iv x f ・ (g ・ h)) ・ id a - -- ≡⟨ cong ( λ k → k ・ id a) (assoc-iv x f ( g ・ h )) ⟩ - -- iv x (f ・ (g ・ h)) ・ id a - -- ≡⟨ cong ( λ k → iv x k ・ id a) (≡←== (associative f g h ) ) ⟩ - -- {!!} - -- ≡⟨ {!!} ⟩ - -- iv x ((f ・ g ) ・ h) ・ id a - -- ≡⟨ sym (cong ( λ k → k ・ id a) (assoc-iv x (f ・ g ) h)) ⟩ - -- ( iv x (f ・ g ) ・ h) ・ id a - -- ≡⟨ sym (cong ( λ k → (k ・ h ) ・ id a) (assoc-iv x f g)) ⟩ - -- ((iv x f ・ g) ・ h) ・ id a - -- ∎ where open ≡-Reasoning - -- {!!} ( cong ( λ k → iv x k ) ( ≡←== (associative f g h ) ) ) + associative {a} (iv x f) g h = {!!} -- cong ( λ k → iv x k ) (associative f g h) 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 = {!!}