Mercurial > hg > Members > kono > Proof > category

changeset 890:f52d21eaada4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
SL is not strictly positive
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 13 Apr 2020 08:10:40 +0900
parents 07fdaecc17b3
children 2685eaaa8763
files CCCGraph.agda
diffstat 1 files changed, 12 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Sun Apr 12 18:18:20 2020 +0900
+++ b/CCCGraph.agda	Mon Apr 13 08:10:40 2020 +0900
@@ -167,10 +167,10 @@
 
    data SL : (t : Objs ) → Set  (c₁ ⊔ c₂) where
       term : SL ⊤
-      type : {x : vertex G} → SL (atom x)
+      value : (x : vertex G) → SL (atom x)
       _::_ : {a b : vertex G} → (f : edge G a b ) → (prev : SL (atom a)) → SL (atom b)
       _,_ : {a b : Objs } → (f : SL a ) → (g : SL b) → SL (a ∧ b)
-      func : {a b : Objs } → ( f : SL b) → SL (b <= a )    -- tail of f should be a SL a
+      func : {a b : Objs } → ( f : SL a → SL b) → SL (b <= a )    -- tail of f should be a SL a
 
    _+_ : { a b c : Objs } → ( SL b → SL c ) → ( SL a → SL b ) → SL a → SL c
    _+_ f g x = f ( g x )
@@ -181,13 +181,13 @@
    fobj : ( a  : Objs  ) → Set (c₁ ⊔ c₂)
    fobj  a = SL a
 
+   fmap : { a b : Objs  } → Hom PL a b → fobj a → fobj b
    amap : { a b : Objs  } → Arrow  a b → fobj a → fobj b
    amap (arrow x) a =  x :: a 
    amap π ( x , y ) = x 
    amap π' ( x , y ) = y
-   amap ε (func f , x ) = append f x
-   amap (f *) x = func {!!}
-   fmap : { a b : Objs  } → Hom PL a b → fobj a → fobj b
+   amap ε (func f , x ) = f x
+   amap (f *) x = func (λ y →  fmap f ( x , y ) )
    fmap (id a) x = x
    fmap (○ a) x = term
    fmap < f , g > x = ( fmap f x , fmap g x )
@@ -204,10 +204,13 @@
         _++_ = Category._o_ PL
         ++idR = IsCategory.identityR ( Category.isCategory PL )
         distr : {a b c : Obj PL}  { f : Hom PL a b } { g : Hom PL b c } → (z : fobj  a ) → fmap (g ++ f) z ≡ fmap g (fmap f z)
-        distr {a} {b} {c} {f} {g} z = {!!}  where
-           -- adistr : fmap (g ++ f) z ≡ fmap g (fmap f z) →
-           --     ( x : Arrow d c ) → fmap ( next x (g ++ f) ) z  ≡ fmap ( next x g ) (fmap f z )
-           -- adistr eq x = cong ( λ k → amap x k ) eq
+        distr {a} {a₁} {a₁} {f} {id a₁} z = refl
+        distr {a} {a₁} {⊤} {f} {○ a₁} z = refl
+        distr {a} {b} {c ∧ d} {f} {< g , g₁ >} z = cong₂ (λ j k  →  j , k  ) (distr {a} {b} {c} {f} {g} z) (distr {a} {b} {d} {f} {g₁} z)
+        distr {a} {b} {c} {f} {iv {_} {_} {d} x g} z = adistr (distr  {a} {b} {d} {f} {g} z) x where 
+           adistr : fmap (g ++ f) z ≡ fmap g (fmap f z) →
+                ( x : Arrow d c ) → fmap ( iv x (g ++ f) ) z  ≡ fmap ( iv x g ) (fmap f z )
+           adistr eq x = cong ( λ k → amap x k ) eq
         isf : IsFunctor PL Sets fobj fmap 
         IsFunctor.identity isf = extensionality Sets ( λ x → refl )
         IsFunctor.≈-cong isf refl = refl