Mercurial > hg > Members > kono > Proof > category

changeset 880:543ceeb10191

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 11 Apr 2020 12:07:45 +0900
parents 73bce40fd1c1
children da0a1dd0c2ee
files CCCGraph1.agda
diffstat 1 files changed, 61 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph1.agda	Sat Apr 11 09:49:37 2020 +0900
+++ b/CCCGraph1.agda	Sat Apr 11 12:07:45 2020 +0900
@@ -97,6 +97,27 @@
    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
+   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)) = refl
+   idem-eval (iv f (○ a)) = refl
+   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 (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 | _ = refl
+   idem-eval (iv f (iv g h)) | ○ a | m | _ = refl
+   idem-eval (iv π (iv g h)) | < t , t₁ > | m | _ = refl-<l> m
+   idem-eval (iv π' (iv g h)) | < t , t₁ > | m | _ = refl-<r> m
+   idem-eval (iv ε (iv g h)) | < t , t₁ > | m | _ = cong ( λ k → iv ε k ) m
+   idem-eval (iv (f *) (iv g h)) | < t , t₁ > | m | _ = cong ( λ k → iv (f *) k ) m
+   idem-eval (iv f (iv g h)) | iv f₁ t | m | record { eq = ee } = trans lemma (cong ( λ k → iv f k ) m )  where
+      lemma : eval (iv f (iv f₁ t)) ≡ iv f (eval (iv f₁ t))
+      lemma = {!!}
+
    PL1 :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
    PL1 = record {
             Obj  = Objs;
@@ -112,28 +133,48 @@
                     associative  = λ{a b c d f g h } →  cong (λ k → eval k ) (associative f g h )
                }
            }  where 
-              id-case : {a b : Objs } → (f g : Arrows a b) → (h : Arrows b b) →
-                 eval f ≡ eval g → 
-                 id b ≡ eval h → eval f ≡ eval (h ・ g)
-              id-case {a} {b} f g (id b) f=g h=i = f=g
-              id-case {a} {b} f g (iv π  < h1 , h2 >)  f=g h=i = id-case f g h1 f=g h=i
-              id-case {a} {b} f g (iv π' < h1 , h2 >)  f=g h=i = id-case f g h2 f=g h=i
-              id-case {a} {b} f g (iv x (iv f₁ h)) f=g h=i with eval (iv f₁ h) | inspect eval (iv f₁ h)
-              id-case {a} {b} f g (iv π (iv f₁ h)) f=g h=i | < t , t₁ > | record { eq = ee } = lemma where
-                  lemma : eval f ≡ eval (iv π (iv f₁ (h ・ g)))
-                  lemma = {!!}
-              id-case {a} {b} f g (iv π' (iv f₁ h)) f=g h=i | < t , t₁ > | record { eq = ee } = {!!}
+              iv-e : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ iv x (eval g)
+              iv-e = ?
+              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 (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 f g) = {!!}
+              iv-d π' (id _) = refl
+              iv-d π' < g , g₁ > = sym (idem-eval g₁)
+              iv-d π' (iv f g) = {!!}
+              iv-d ε g = {!!}
+              iv-d (x *) g = {!!}
+              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 = {!!}
+              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 = {!!}
+              d-eval (iv (x *) < f , f₁ >) g = {!!}
+              d-eval (iv x (iv f f₁)) g = {!!}
               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 (id a) i1 f=g h=i = id-case f g i1 f=g h=i  
-              ore f g (○ a) (○ a) f=g h=i = refl
-              ore f g (○ a) (iv x i) f=g h=i = {!!}
-              ore f g < h1 , h2 > < i1 , i2 > f=g h=i = cong₂ (λ j k → < j , k >) (ore f g h1 i1 f=g {!!}) (ore f g h2 i2 f=g {!!})
-              ore f g < h1 , h2 > (iv x i) f=g h=i = {!!}
-              ore f g (iv x h) (id a) f=g h=i = sym ( id-case g f (iv x h) (sym f=g) (sym h=i))
-              ore f g (iv x h) (○ a) f=g h=i = {!!}
-              ore f g (iv x h) < i , i₁ > f=g h=i = {!!}
-              ore f g (iv x h) (iv y i) f=g h=i = {!!}
+              ore f g h i f=g h=i = begin
+                    eval (h ・ f)
+                ≡⟨ d-eval h f ⟩
+                    eval (eval h ・ eval f)
+                ≡⟨ cong₂ (λ j k → eval ( j ・ k )) h=i f=g  ⟩
+                    eval (eval i ・ eval g)
+                ≡⟨ sym ( d-eval i g ) ⟩
+                    eval (i ・ g)
+                ∎  where open ≡-Reasoning
+
 
    fmap : {A B : Obj PL} → Hom PL A B → Hom PL A B
    fmap f = {!!}