Mercurial > hg > Members > kono > Proof > category
changeset 859:ed0b3d2d1037
idempotent is not finnished but other parts may be proved
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 05 Apr 2020 11:15:41 +0900 |
| parents | 9d9cba1f831e |
| children | d3cf372ac8cd |
| files | CCCGraph1.agda |
| diffstat | 1 files changed, 8 insertions(+), 12 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph1.agda Sun Apr 05 10:44:40 2020 +0900 +++ b/CCCGraph1.agda Sun Apr 05 11:15:41 2020 +0900 @@ -88,9 +88,9 @@ idem-eval (iv ε (iv g h)) | iv ε < t , t₁ > | m = cong ( λ k → iv ε k ) m idem-eval (iv (f *) (iv g h)) | iv ε < t , t₁ > | m = cong ( λ k → iv (f *) k ) m idem-eval (iv (f *) (iv g h)) | iv (f1 *) < t , t₁ > | m = cong ( λ k → iv (f *) k ) m - idem-eval {a} {b} (iv {a} {b} {d} f (iv g h)) | iv {a} {d} {e} f1 (iv {a} {e} {e1} f2 t) | m = lemma f f1 f2 where - lemma : (f : Arrow d b ) → (f1 : Arrow e d ) → (f2 : Arrow e1 e ) → eval (iv f ( iv f1 (iv f2 t))) ≡ iv f ( iv f1 (iv f2 t)) - lemma f f1 f2 = ? + idem-eval (iv f (iv g h)) | iv f1 (iv f₁ t) | m = {!!} + -- lemma : eval (iv f ( iv f1 (iv f₁ t))) ≡ iv f ( iv f1 (iv f₁ t)) + -- lemma = {!!} _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c id a ・ g = g @@ -118,13 +118,9 @@ identityR {a} {b} {iv π' < g , g₁ >} = identityR {_} {_} {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 {c} {d} {e} π (iv g h)} with inspect eval (iv g h) | eval (iv g h) - identityR {.(b ∧ _)} {b} {iv {.(b ∧ _)} {b} {.(b ∧ _)} π (iv g h)} | record {eq = refl } | id .(b ∧ _) = refl - identityR {a} {b} {iv {a} {b} {.(b ∧ _)} π (iv g h)} | record {eq = refl } | < t , t₁ > = {!!} - identityR {a} {b} {iv {a} {b} {.(b ∧ _)} π (iv g h)} | record {eq = refl } | iv f t = {!!} - identityR {a} {b} {iv {c} {d} {e} π' (iv g h)} = {!!} - identityR {a} {b} {iv {c} {d} {e} f (iv g h)} with identityR {_} {_} {iv g h} - ... | t = {!!} + identityR {a} {b} {iv {c} {d} {e} π (iv g h)} = refl + identityR {a} {b} {iv {c} {d} {e} π' (iv g h)} = refl + identityR {a} {b} {iv {c} {d} {e} f (iv g h)} = refl ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g ==←≡ eq = cong (λ k → eval k ) eq @@ -148,10 +144,10 @@ 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₁} = {!!} + identityL {_} {_} {iv f f₁} = refl 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 = {!!} + 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 {a} (iv x f) g h = {!!} -- cong ( λ k → iv x k ) (associative f g h)