Mercurial > hg > Members > kono > Proof > category

changeset 878:0793d9adbbdd

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 Fri, 10 Apr 2020 23:07:00 +0900
parents 66dfc4f80ba3
children 73bce40fd1c1
files CCCGraph1.agda
diffstat 1 files changed, 15 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph1.agda	Fri Apr 10 09:21:54 2020 +0900
+++ b/CCCGraph1.agda	Fri Apr 10 23:07:00 2020 +0900
@@ -102,34 +102,31 @@
                     isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
                     identityL  = λ {a b f} → cong (λ k → eval k ) (identityL {a} {b} {f});
                     identityR  = λ {a b f} → cong (λ k → eval k ) (identityR {a} {b} {f});
-                    o-resp-≈  = λ {a b c f g h i} → o-resp-≈-e {a} {b} {c} {f} {g} {h} {i}  ; 
+                    o-resp-≈  = λ {a b c f g h i} → ore {a} {b} {c} f g h i ; 
                     associative  = λ{a b c d f g h } →  cong (λ k → eval k ) (associative f g h )
                }
            }  where 
-              o-resp-≈-e  : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
+              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)
-              o-resp-≈-e f=g h=i = {!!} 
+              ore f g (id a) (id a) f=g refl = cong (λ k → id a ・ k) f=g
+              ore f g (id a) (iv x < i1 , i2 >) f=g h=i = {!!}
+              ore f g (id a) (iv x (iv i1 i2)) 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 = {!!}
+              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 = {!!}
 
    fmap : {A B : Obj PL} → Hom PL A B → Hom PL A B
-   fmap (id a) = id _
-   fmap (○ a) = ○ a
-   fmap < f , g > = < fmap f , fmap g >
-   fmap (iv (arrow x) g) = iv (arrow x) (fmap g)
-   fmap (iv π (id _)) = {!!}
-   fmap (iv π < g , g₁ >) = fmap g
-   fmap (iv π (iv f g)) = {!!}
-   fmap (iv π' (id _)) = {!!}
-   fmap (iv π' < g , g₁ >) = fmap g₁
-   fmap (iv π' (iv f g)) = {!!}
-   fmap (iv ε (id _)) = {!!}
-   fmap (iv ε < f , g >) = {!!}
-   fmap (iv ε (iv f g)) = {!!}
-   fmap (iv (f *) g) = {!!}
+   fmap f = {!!}
 
    PLCCC :  Functor PL PL
    PLCCC = record {
          FObj = λ x → x
-       ; FMap = {!!}
+       ; FMap = fmap
        ; isFunctor = record {
               identity = {!!}
             ; distr = {!!}