Mercurial > hg > Members > kono > Proof > category

changeset 406:2fbd92ddecb5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
non recorded arrow does not work
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Mar 2016 20:58:00 +0900
parents 4c34c0e3c4bb
children 7bdc93de2d6e
files limit-to.agda
diffstat 1 files changed, 53 insertions(+), 36 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Mon Mar 21 12:44:43 2016 +0900
+++ b/limit-to.agda	Mon Mar 21 20:58:00 2016 +0900
@@ -32,38 +32,55 @@
    id-t1 : Arrow  
    arrow-f :  Arrow
    arrow-g :  Arrow
-   nil :  Arrow
 
-record Two-Hom { c₁  c₂ : Level }   (a : TwoObject { c₁}  ) (b : TwoObject  { c₁} ) : Set    c₂  where
-   field
-      hom  : Maybe ( Arrow  { c₂ } )
-
-open  Two-Hom 
-
-Two-id :  { c₁ c₂ : Level } -> (a : TwoObject {c₁} ) ->   Two-Hom {c₁} { c₂}  a a 
-Two-id _  = record { hom = just  id-t0  }
 
 -- arrow composition
 
-twocomp-det : {c₁  c₂ : Level } ->  { a b : TwoObject {c₁} } -> Arrow  { c₂ } -> Arrow  { c₂ } ->  Arrow  { c₂ } 
-twocomp-det {_} {_} {t0} {t0} id-t0 id-t0 = id-t0
-twocomp-det {_} {_} {t0} {t1} id-t0 arrow-f = arrow-f
-twocomp-det {_} {_} {t0} {t1} id-t0 arrow-g = arrow-g
-twocomp-det {_} {_} {t1} {t1} id-t0 id-t1 = id-t1
-twocomp-det {_} {_} {t0} {t1} arrow-f id-t1 = arrow-f
-twocomp-det {_} {_} {t0} {t1} arrow-g id-t1 = arrow-g
-twocomp-det _ _ = nil
-
-twocomp : {c₁  c₂ : Level } ->  { a b : TwoObject {c₁} } -> Arrow  { c₂ } -> Arrow  { c₂ } -> Maybe  ( Arrow  { c₂ } )
-twocomp id-t0 f = just f
-twocomp f id-t0 = just f
+twocomp : {c₁  c₂ : Level } ->  { a b c : TwoObject {c₁} } ->  Arrow  { c₂ }  ->  Arrow  { c₂ }  ->  Maybe ( Arrow  { c₂ }  )
+twocomp {_} {_} {t0} {t1} {t1} id-t1  arrow-f  = just arrow-f
+twocomp {_} {_} {t0} {t1} {t1} id-t1  arrow-g  = just arrow-g
+twocomp {_} {_} {t1} {t1} {t1} id-t1  id-t1  = just id-t1
+twocomp {_} {_} {t0} {t0} {t1} arrow-f  id-t0 = just arrow-f
+twocomp {_} {_} {t0} {t0} {t1} arrow-g  id-t0 = just arrow-g
+twocomp {_} {_} {t0} {t0} {t0} id-t0  id-t0 = just id-t0
 twocomp _ _ = nothing
 
-_×_ :  { c₁  c₂ : Level }  -> {A B C : TwoObject { c₁} } →  Two-Hom { c₁}  {c₂}  B C →  Two-Hom { c₁}  {c₂}  A B  →  Two-Hom { c₁}  {c₂}  A C 
-_×_   { c₁} {ℓ} {a} {b} {c} f g with  hom f |  hom g 
-_×_   { c₁} {ℓ} {a} {b} {c} f g | nothing   | _ = record { hom = nothing }
-_×_   { c₁} {ℓ} {a} {b} {c} f g | _   | nothing  = record { hom = nothing }
-_×_   { c₁} {ℓ} {a} {b} {c} _ _ | just f  | just g   = record { hom = twocomp  { c₁} {ℓ} {a} {c} f g }
+_×_ :  { c₁  c₂ : Level }  -> {A B C : TwoObject { c₁} } →  Maybe ( Arrow   { c₂ }) →  Maybe ( Arrow    { c₂ })  →  Maybe ( Arrow  { c₂ })  
+_×_   nothing _  = nothing
+_×_   _ nothing  = nothing
+_×_   { c₁} { c₂} {a} {b} {c} (just f)  (just g)   =  twocomp  { c₁} { c₂} {a} {b} {c} f g  
+
+
+[_==_] : { c₁ c₂ : Level}   {a b : TwoObject {c₁} } ->  Rel (Maybe (Arrow  { c₂ })) (c₂) 
+[_==_]   =  Eq   _≡_ 
+
+--          f    g    h
+--       d <- c <- b <- a
+
+assoc-× :   { c₁  c₂ : Level } {a b c d : TwoObject  { c₁} } {f g h : Maybe (Arrow  { c₂ })} → 
+   [ f × (g × h) == (f × g) × h ]
+assoc-× {_} {_} {_} {_} {_} {_} {nothing} {_} {_} = nothing
+assoc-× {_} {_} {_} {_} {_} {_} {just _} {nothing} {_} = nothing
+assoc-× {_} {_} {_} {_} {_} {_} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} with ((just g ) × (just h)) | ((just f ) × (just g)  )
+assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | nothing | _ = nothing
+assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | just id-t0 | just id-t0 = just refl
+assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | just id-t1 | just id-t1 = just refl
+assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | just id-t1 | just arrow-f = just refl
+assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | just id-t1 | just arrow-g = just refl
+assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | just arrow-f | just id-t0  = just refl
+assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | just arrow-g | just id-t0  = just refl
+assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | just _ | nothing = nothing
+... | just id-t0 | just id-t1 = nothing
+... | just id-t0 | (just arrow-f) = nothing
+... | just id-t0 | (just arrow-g) = nothing
+... | just id-t1 | (just id-t0) = nothing
+... | just arrow-f | (just id-t1) = nothing
+... | just arrow-f | (just arrow-f) = nothing
+... | just arrow-f | (just arrow-g) = nothing
+... | just arrow-g | (just id-t1) = nothing
+... | just arrow-g | (just arrow-f) = nothing
+... | just arrow-g | (just arrow-g) = nothing
 
 
 open import maybeCat  
@@ -73,12 +90,12 @@
 TwoCat : { c₁ c₂ ℓ : Level  } ->  Category   c₁  c₂  c₂
 TwoCat   {c₁}  {c₂} {ℓ} = record {
     Obj  = TwoObject  {c₁} ;
-    Hom = λ a b →    Arrow  { c₂ } ;
-    _o_ =  \{a} {b} x y -> twocomp-det  {c₁}  {c₂} {a} {b} x y ;
-    _≈_ = λ a b →   a ≡ b   ;
-    Id  =  \{a} -> id-t0  ;
+    Hom = λ a b →    Maybe ( Arrow  { c₂ } ) ;
+    _o_ =  \{a} {b} {c} x y -> _×_ { c₁ } {  c₂} {a} {b} {c} x y ;
+    _≈_ =    Eq  _≡_   ;
+    Id  =  \{a} -> just id-t0  ;
     isCategory  = record {
-            isEquivalence =  record {refl = refl  ; trans = ≡-trans  ; sym = ≡-sym   } ;
+            isEquivalence =  record {refl = {!!}  ; trans = {!!}  ; sym = {!!}  } ;
             identityL  = {!!} ;
             identityR  = {!!} ;
             o-resp-≈  =  {!!} ;
@@ -102,11 +119,11 @@
           fobj :  Obj I -> Obj A
           fobj t0 = a
           fobj t1 = b
-          fmap :  {x y : Obj I } ->  (Arrow  {c₂} ) -> Hom MA (fobj x) (fobj y)
-          fmap {t0} {t1} arrow-f = record { hom = just f }
-          fmap {t0} {t1} arrow-g = record { hom = just g }
-          fmap {t0} {t0} id-t0  = record { hom = just ( id1 A a )}
-          fmap {t1} {t1} id-t1  = record { hom = just ( id1 A b )}
+          fmap :  {x y : Obj I } ->  Maybe (Arrow  {c₂} ) -> Hom MA (fobj x) (fobj y)
+          fmap {t0} {t1} (just arrow-f) = record { hom = just f }
+          fmap {t0} {t1} (just arrow-g) = record { hom = just g }
+          fmap {t0} {t0} (just id-t0)  = record { hom = just ( id1 A a )}
+          fmap {t1} {t1} (just id-t1)  = record { hom = just ( id1 A b )}
           fmap {_} {_}   _ = record { hom = nothing }
           open ≈-Reasoning (A) 
           identity :  {x : Obj I} → {!!}