Mercurial > hg > Members > kono > Proof > category
changeset 892:ad0732c51d38
clean up CCCGraph1.agda
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 13 Apr 2020 08:56:52 +0900 |
| parents | 2685eaaa8763 |
| children | 4a66f48ffee5 |
| files | CCCGraph1.agda |
| diffstat | 1 files changed, 14 insertions(+), 216 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph1.agda Mon Apr 13 08:52:35 2020 +0900 +++ b/CCCGraph1.agda Mon Apr 13 08:56:52 2020 +0900 @@ -94,187 +94,6 @@ eval (iv (f *) (iv g h)) | < t , t₁ > = iv ((eval f) *) < t , t₁ > eval (iv f (iv g h)) | iv f1 t = iv f (iv f1 t) - refl-<l> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c } → < f , g > ≡ < f1 , g1 > → f ≡ f1 - refl-<l> refl = refl - - refl-<r> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c } → < f , g > ≡ < f1 , g1 > → g ≡ g1 - refl-<r> refl = refl - - idem-eval : {a b : Objs } (f : Arrows a b ) → eval (eval f) ≡ eval f - - iv-e-arrow : { a : Objs } → {b c : vertex G } → (x : edge G b c ) ( g : Arrows a (atom b) ) - → eval (iv (arrow x) g) ≡ iv (arrow x) (eval g) - iv-e-arrow x (id (atom _)) = refl - iv-e-arrow x (iv f g) with eval (iv f g) - iv-e-arrow x (iv f g) | id (atom _) = refl - iv-e-arrow x (iv f g) | iv f₁ t = refl - iv-e-ε : { a b c : Objs } → ( g : Arrows a ((c <= b) ∧ b ) ) - → eval (iv ε g) ≡ iv ε (eval g) - iv-e-ε (id _) = refl - iv-e-ε < g , g₁ > = refl - iv-e-ε (iv f g) with eval (iv f g) - iv-e-ε (iv f g) | id _ = refl - iv-e-ε (iv f g) | < t , t₁ > = refl - iv-e-ε (iv f g) | iv f₁ t = refl - iv-e-* : { a b c d : Objs } → { f : Arrows (d ∧ b) c} → ( g : Arrows a d ) - → eval (iv (f *) g) ≡ iv ((eval f) *) (eval g) - iv-e-* (id a) = refl - iv-e-* (○ a) = refl - iv-e-* < g , g₁ > = refl - iv-e-* (iv f g) with eval (iv f g) - iv-e-* (iv f g) | id a = refl - iv-e-* (iv f g) | ○ a = refl - iv-e-* (iv f g) | < t , t₁ > = refl - iv-e-* (iv (f *) g) | iv f₁ t = {!!} - iv-e-* (iv f g) | iv f₁ t = {!!} - - iv-e : { a b c : Objs } → (x : Arrow b c ) ( f : Arrows a b) - → { d : Objs } { y : Arrow d b } { g : Arrows a d } → eval f ≡ iv y g - → eval (iv x f) ≡ iv x (eval f) - iv-e x (id a) () - iv-e x (○ a) () - iv-e x < f , f₁ > () - iv-e x (iv f g) {_} {y} {h} eq with eval (iv f g) - iv-e x (iv f g) {_} {y} {h} refl | iv y h = {!!} - - π-lemma : {a b c : Objs } → ( g : Arrows a ( b ∧ c ) ) ( f1 : Arrows a b ) ( f2 : Arrows a c ) - → eval g ≡ < f1 , f2 > → eval (iv π g ) ≡ f1 - π-lemma < g , g₁ > f1 f2 refl = refl - π-lemma (iv π g) f1 f2 eq with eval (iv π g) - π-lemma (iv π g) f1 f2 refl | < t , t₁ > = refl - π-lemma (iv π' g) f1 f2 eq with eval (iv π' g) - π-lemma (iv π' g) f1 f2 refl | < t , t₁ > = refl - π-lemma (iv ε g) f1 f2 eq with eval (iv ε g) - π-lemma (iv ε g) f1 f2 refl | < t , t₁ > = refl - - π'-lemma : {a b c : Objs } → ( g : Arrows a ( b ∧ c ) ) ( f1 : Arrows a b ) ( f2 : Arrows a c ) - → eval g ≡ < f1 , f2 > → eval (iv π' g ) ≡ f2 - π'-lemma < g , g₁ > f1 f2 refl = refl - π'-lemma (iv π g) f1 f2 eq with eval (iv π g) - π'-lemma (iv π g) f1 f2 refl | < t , t₁ > = refl - π'-lemma (iv π' g) f1 f2 eq with eval (iv π' g) - π'-lemma (iv π' g) f1 f2 refl | < t , t₁ > = refl - π'-lemma (iv ε g) f1 f2 eq with eval (iv ε g) - π'-lemma (iv ε g) f1 f2 refl | < t , t₁ > = refl - - iv-d : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ eval (iv x (eval g)) - iv-d (arrow x) g = begin - eval (iv (arrow x) g) - ≡⟨ iv-e-arrow x g ⟩ - iv (arrow x) (eval g) - ≡⟨ cong (λ k → iv (arrow x) k ) ( sym ( idem-eval g) ) ⟩ - iv (arrow x) (eval (eval g)) - ≡⟨ sym (iv-e-arrow x (eval g)) ⟩ - eval (iv (arrow x) (eval g)) - ∎ where open ≡-Reasoning - iv-d π (id _) = refl - iv-d π < g , g₁ > = sym (idem-eval g) - iv-d π (iv x f ) with eval (iv x f) | inspect eval (iv x f) - ... | id _ | m = refl - ... | < f1 , f2 > | record {eq = ee } = begin - f1 - ≡⟨ sym ( π-lemma (iv x f) f1 f2 ee ) ⟩ - eval (iv π (iv x f)) - ≡⟨ sym (idem-eval (iv π (iv x f))) ⟩ - eval (eval (iv π (iv x f))) - ≡⟨ cong (λ k → eval k ) (π-lemma (iv x f) f1 f2 ee ) ⟩ - eval f1 - ∎ where open ≡-Reasoning - iv-d π (iv x f) | iv x1 f1 | record { eq = ee } = begin - iv π (iv x1 f1) - ≡⟨ sym (cong (λ k → iv π k ) ee) ⟩ - iv π (eval (iv x f)) - ≡⟨ sym (iv-e π (iv x f) ee ) ⟩ - eval (iv π (iv x f)) - ≡⟨ sym (idem-eval (iv π (iv x f))) ⟩ - eval (eval (iv π (iv x f))) - ≡⟨ cong (λ k → eval k ) ( iv-e π (iv x f) ee ) ⟩ - eval (iv π (eval (iv x f))) - ≡⟨ cong (λ k → eval (iv π k)) ee ⟩ - eval (iv π (iv x1 f1)) - ∎ where open ≡-Reasoning - iv-d π' (id _) = refl - iv-d π' < g , g₁ > = sym (idem-eval g₁) - iv-d π' (iv x f ) with eval (iv x f) | inspect eval (iv x f) - ... | id _ | m = refl - ... | < f1 , f2 > | record {eq = ee } = begin - f2 - ≡⟨ sym ( π'-lemma (iv x f) f1 f2 ee ) ⟩ - eval (iv π' (iv x f)) - ≡⟨ sym (idem-eval (iv π' (iv x f))) ⟩ - eval (eval (iv π' (iv x f))) - ≡⟨ cong (λ k → eval k ) (π'-lemma (iv x f) f1 f2 ee ) ⟩ - eval f2 - ∎ where open ≡-Reasoning - iv-d π' (iv x f) | iv x1 f1 | record { eq = ee } = begin - iv π' (iv x1 f1) - ≡⟨ sym (cong (λ k → iv π' k ) ee) ⟩ - iv π' (eval (iv x f)) - ≡⟨ sym (iv-e π' (iv x f) ee ) ⟩ - eval (iv π' (iv x f)) - ≡⟨ sym (idem-eval (iv π' (iv x f))) ⟩ - eval (eval (iv π' (iv x f))) - ≡⟨ cong (λ k → eval k ) ( iv-e π' (iv x f) ee ) ⟩ - eval (iv π' (eval (iv x f))) - ≡⟨ cong (λ k → eval (iv π' k)) ee ⟩ - eval (iv π' (iv x1 f1)) - ∎ where open ≡-Reasoning - iv-d ε g = begin - eval (iv ε g) - ≡⟨ iv-e-ε g ⟩ - iv ε (eval g) - ≡⟨ cong (λ k → iv ε k ) ( sym ( idem-eval g) ) ⟩ - iv ε (eval (eval g)) - ≡⟨ sym (iv-e-ε (eval g)) ⟩ - eval (iv ε (eval g)) - ∎ where open ≡-Reasoning - iv-d (x *) g = begin - eval (iv (x *) g) - ≡⟨ iv-e-* g ⟩ - iv ((eval x) *) (eval g) - ≡⟨ cong (λ k → iv ((eval x) *) k ) ( sym ( idem-eval g) ) ⟩ - iv ((eval x) *) (eval (eval g)) - ≡⟨ sym (iv-e-* (eval g)) ⟩ - eval (iv (x *) (eval g)) - ∎ where open ≡-Reasoning - - idem-eval (id a) = refl - idem-eval (○ a) = refl - idem-eval < f , f₁ > = cong₂ ( λ j k → < j , k > ) (idem-eval f) (idem-eval f₁) - idem-eval (iv (f *) (id a)) = {!!} - idem-eval (iv f (id a)) = {!!} - idem-eval (iv (f *) (○ a)) = {!!} - idem-eval (iv f (○ a)) = {!!} - idem-eval (iv π < g , g₁ >) = idem-eval g - idem-eval (iv π' < g , g₁ >) = idem-eval g₁ - idem-eval (iv ε < f , f₁ >) = cong₂ ( λ j k → iv ε < j , k > ) (idem-eval f) (idem-eval f₁) - idem-eval (iv (x *) < f , f₁ >) = {!!} -- cong₂ ( λ j k → iv ((eval x) *) < j , k > ) (idem-eval f) (idem-eval f₁) - idem-eval (iv f (iv g h)) with eval (iv g h) | idem-eval (iv g h) | inspect eval (iv g h) - idem-eval (iv f (iv g h)) | id a | m | _ = {!!} - idem-eval (iv f (iv g h)) | ○ a | m | _ = {!!} - idem-eval (iv π (iv g h)) | < t , t₁ > | m | _ = refl-<l> {!!} - idem-eval (iv π' (iv g h)) | < t , t₁ > | m | _ = refl-<r> {!!} - idem-eval (iv ε (iv g h)) | < t , t₁ > | m | _ = {!!} -- cong ( λ k → iv ε k ) ? - idem-eval (iv (f *) (iv g h)) | < t , t₁ > | m | _ = {!!} -- cong ( λ k → iv (f *) k ) m - idem-eval (iv ε (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!} -- trans (iv-e-ε (iv f₁ t)) (cong ( λ k → iv ε k ) m ) - idem-eval (iv (x *) (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!} -- trans (iv-e-* (iv f₁ t)) {!!} -- (cong ( λ k → iv (x *) k ) m ) - idem-eval (iv π (iv g h)) | iv f₁ t | m | record { eq = ee } = begin - {!!} - ≡⟨ {!!} ⟩ - eval (iv π ( iv f₁ t)) - ≡⟨ {!!} ⟩ - eval (iv π (eval (iv g h ))) - ≡⟨ {!!} ⟩ - eval (iv π (iv g h)) - ≡⟨ iv-e π (iv g h) ee ⟩ - iv π (eval (iv g h)) - ≡⟨ cong (λ k → iv π k ) ee ⟩ - iv π ( iv f₁ t) - ≡⟨ {!!} ⟩ - {!!} - ∎ where open ≡-Reasoning - idem-eval (iv π' (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!} - idem-eval (iv (arrow x) (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!} -- trans (iv-e-arrow x (iv f₁ t)) (cong ( λ k → iv (arrow x) k ) m ) PL1 : Category (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂) PL1 = record { @@ -293,28 +112,7 @@ } where d-eval : {A B C : Objs} (f : Arrows B C) (g : Arrows A B) → eval (f ・ g) ≡ eval (eval f ・ eval g) - d-eval (id a) g = sym (idem-eval g) - d-eval (○ a) g = refl - d-eval < f , f₁ > g = cong₂ (λ j k → < j , k > ) (d-eval f g) (d-eval f₁ g) - d-eval (iv x (id a)) g = {!!} -- iv-d x g - d-eval (iv (x *) (○ a)) g = {!!} -- refl - d-eval (iv π < f , f₁ >) g = d-eval f g - d-eval (iv π' < f , f₁ >) g = d-eval f₁ g - d-eval (iv ε < f , f₁ >) g = cong₂ (λ j k → iv ε k ) (d-eval f g) ( - cong₂ (λ j k → < j , k > ) ( d-eval f g ) ( d-eval f₁ g )) - d-eval (iv (x *) < f , f₁ >) g = {!!} -- cong₂ (λ j k → iv ((eval x) *) k ) (d-eval f g) ( - -- cong₂ (λ j k → < j , k > ) ( d-eval f g ) ( d-eval f₁ g )) - d-eval (iv x (iv f f₁)) g = begin - eval (iv x (iv f f₁) ・ g) - ≡⟨⟩ - eval (iv x (iv f f₁ ・ g)) - ≡⟨ {!!} ⟩ - eval (iv x (eval (iv f f₁ ・ g))) - ≡⟨ {!!} ⟩ - eval (iv x (eval (iv f f₁) ・ eval g)) - ≡⟨ {!!} ⟩ - eval (eval (iv x (iv f f₁)) ・ eval g) - ∎ where open ≡-Reasoning + d-eval = {!!} ore : {A B C : Objs} (f g : Arrows A B) (h i : Arrows B C) → eval f ≡ eval g → eval h ≡ eval i → eval (h ・ f) ≡ eval (i ・ g) ore f g h i f=g h=i = begin @@ -328,16 +126,16 @@ ∎ where open ≡-Reasoning - fmap : {A B : Obj PL} → Hom PL A B → Hom PL A B - fmap f = {!!} - - PLCCC : Functor PL PL - PLCCC = record { - FObj = λ x → x - ; FMap = fmap - ; isFunctor = record { - identity = {!!} - ; distr = {!!} - ; ≈-cong = {!!} - } - } +-- fmap : {A B : Obj PL} → Hom PL A B → Hom PL A B +-- fmap f = {!!} +-- +-- PLCCC : Functor PL PL +-- PLCCC = record { +-- FObj = λ x → x +-- ; FMap = fmap +-- ; isFunctor = record { +-- identity = {!!} +-- ; distr = {!!} +-- ; ≈-cong = {!!} +-- } +-- }