Mercurial > hg > Members > kono > Proof > category
changeset 867:e47045bfc37a
≡ is no good because of non regularized terms
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 07 Apr 2020 18:01:29 +0900 |
| parents | 2ff6242aed06 |
| children | 35b2412a68e4 |
| files | CCCGraph1.agda |
| diffstat | 1 files changed, 25 insertions(+), 46 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph1.agda Tue Apr 07 15:58:43 2020 +0900 +++ b/CCCGraph1.agda Tue Apr 07 18:01:29 2020 +0900 @@ -68,32 +68,35 @@ refl-<r> refl = refl _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c - id a ・ g = g + id a ・ g = eval g ○ a ・ g = ○ _ < f , g > ・ h = < f ・ h , g ・ h > - iv f (id _) ・ h = iv f h + iv f (id _) ・ h = eval ( 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 ) + iv x y ・ id a = eval (iv x y) + iv f (iv f₁ g) ・ h with eval (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 + (iv π' (iv f₁ g) ・ h) | < t , t₁ > = t₁ + (iv f (iv f₁ g) ・ h) | < t , t₁ > = iv f < t , t₁ > + (iv f (iv f₁ g) ・ h) | iv f₂ t = iv f ( iv f₂ t ) - _==_ : {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 B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f identityR {a} {.a} {id a} = refl identityR {a} {⊤} {○ a} = refl identityR {_} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) (identityR {_} {_} {f} ) (identityR {_} {_} {f₁}) identityR {_} {_} {iv f (id a)} = refl identityR {_} {_} {iv f (○ a)} = refl - identityR {_} {_} {iv π < g , g₁ >} = identityR {_} {_} {g} - identityR {_} {_} {iv π' < g , g₁ >} = identityR {_} {_} {g₁} + identityR {_} {_} {iv π < g , g₁ >} = {!!} -- identityR {_} {_} {g} + 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)} = refl + identityR {_} {_} {iv f (iv g h)} = {!!} open import Data.Empty open import Relation.Nullary @@ -123,7 +126,6 @@ std-∧ (iv f f1) g h t with eval ( iv f f1) | inspect eval (iv f f1 ) std-∧ (iv π < f1 , f2 >) g h refl | iv π < g , h > | record { eq = ee } = std-∧ f1 g h ee std-∧ (iv π' < f1 , f2 >) g h refl | iv π < g , h > | record { eq = ee } = std-∧ f2 g h ee - std-∧ (iv π (iv f f1)) g h refl | iv π < g , h > | record { eq = ee } = ? std-∧ (iv x (iv f f1)) g h refl | iv π < g , h > | record { eq = ee } = {!!} where lemma : ¬ ( eval (iv x (iv f f1)) ≡ iv π < g , h > ) lemma ee = {!!} @@ -154,29 +156,12 @@ idem-eval (iv f (iv {_} {_} {d} g h)) | iv {a} {_} {d1 ∧ d2} f1 t | m = {!!} -- lemma : eval (iv f ( iv f1 t)) ≡ iv f ( iv f1 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 = refl - assoc-iv x (○ a) g = refl - assoc-iv π < f , f₁ > g = refl - assoc-iv π' < f , f₁ > g = refl - assoc-iv ε < f , f₁ > g = refl - assoc-iv (x *) < f , f₁ > g = refl - assoc-iv x (iv f g) h = begin - eval (iv x (iv f g ・ h)) - ≡⟨ {!!} ⟩ - eval (iv x (iv f g) ・ h) - ∎ where open ≡-Reasoning - - - ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g - ==←≡ eq = cong (λ k → eval k ) eq - PL : Category (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂) PL = record { Obj = Objs; Hom = λ a b → Arrows a b ; _o_ = λ{a} {b} {c} x y → x ・ y ; - _≈_ = λ x y → x == y ; + _≈_ = λ x y → x ≡ y ; Id = λ{a} → id a ; isCategory = record { isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; @@ -186,14 +171,14 @@ associative = λ{a b c d f g h } → associative f g h } } where - identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) == f + identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f 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₁} = refl + 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 + (f ・ (g ・ h)) ≡ ((f ・ g) ・ h) + 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 π < f , f1 > ) g h = associative f g h @@ -201,23 +186,17 @@ associative {a} (iv ε < f , f1 > ) g h = cong ( λ k → iv ε k ) ( associative < f , f1 > g h ) 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) + iv x (id _) ・ (g ・ h) + ≡⟨ {!!} ⟩ + (iv x (id _) ・ g) ・ h ∎ where open ≡-Reasoning associative {a} (iv x (○ _)) g h = refl associative {a} (iv x (iv y f)) g h = begin - eval (iv x (iv y f) ・ (g ・ h)) - ≡⟨ sym (assoc-iv x (iv y f) ( g ・ h)) ⟩ - eval (iv x ((iv y f) ・ (g ・ h))) + iv x (iv y f) ・ (g ・ h) ≡⟨ {!!} ⟩ - eval ((iv x (iv y f) ・ g) ・ h) + (iv x (iv y f) ・ g) ・ h ∎ where open ≡-Reasoning -- 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) + f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g) o-resp-≈ f=g h=i = {!!}