Mercurial > hg > Members > kono > Proof > category

changeset 409:cb03612d8162

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 Wed, 23 Mar 2016 10:57:00 +0900
parents b265e02b0e0b
children 508c88223aab
files limit-to.agda
diffstat 1 files changed, 73 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Tue Mar 22 15:01:47 2016 +0900
+++ b/limit-to.agda	Wed Mar 23 10:57:00 2016 +0900
@@ -27,48 +27,90 @@
    t0 : TwoObject 
    t1 : TwoObject 
 
-data Arrow {ℓ : Level }  : Set ℓ where
-   id-t0 : Arrow  
-   id-t1 : Arrow  
-   arrow-f :  Arrow
-   arrow-g :  Arrow
-
 
 -- arrow composition
 
 
-_×_ :  { c₁  c₂ : Level }  -> {A B C : TwoObject { c₁} } →  Maybe ( Arrow   { c₂ }) →  Maybe ( Arrow    { c₂ })  →  Maybe ( Arrow  { c₂ })  
+_×_ :  { c₁  c₂ : Level }  -> {A B C : TwoObject { c₁} } →  Maybe ( TwoObject   { c₂ }) →  Maybe ( TwoObject    { c₂ })  →  Maybe ( TwoObject  { c₂ })  
 _×_   nothing _  = nothing
-_×_   _ nothing  = nothing
-_×_   { c₁} { c₂} {t1} {t1} {t1} (just id-t1)  (just id-t1)   =  just id-t1
-_×_   { c₁} { c₂} {t0} {t1} {t1} (just id-t1)  (just f)   =  just f
-_×_   { c₁} { c₂} {t0} {t0} {t0} (just id-t0)  (just id-t0)   =  just id-t0
-_×_   { c₁} { c₂} {t0} {t0} {t1} (just f) (just id-t1)     =  just f
+_×_   (just _) nothing  = nothing
+_×_   { c₁} { c₂} {t1} {t1} {t1} _ f   =  f
+_×_   { c₁} { c₂} {t0} {t1} {t1} _ f   =  f
+_×_   { c₁} { c₂} {t0} {t0} {t0} _ f   =  f
+_×_   { c₁} { c₂} {t0} {t0} {t1} f _   =  f
 _×_   { c₁} { c₂} {a} {b} {c} (just f)  (just g)   =  nothing
 
 
-[_==_] : { c₁ c₂ : Level}   {a b : TwoObject {c₁} } ->  Rel (Maybe (Arrow  { c₂ })) (c₂) 
-[_==_]   =  Eq   _≡_ 
+_==_ : { c₁ c₂ : Level}   {a b : TwoObject {c₁} } ->  Rel (Maybe (TwoObject  { c₂ })) (c₂) 
+_==_   =  Eq   _≡_ 
+
+==refl : ∀ {x} → _==_ x x
+==refl {just x}  = just refl
+==refl {nothing} = nothing
+
+==sym : ∀ {x y} → _==_ x  y → _==_ y  x
+==sym (just x≈y) = just (≡-sym x≈y)
+==sym nothing    = nothing
+
+==trans : ∀ {x y z} → _==_ x  y → _==_ y  z → _==_ x  z
+==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z)
+==trans nothing    nothing    = nothing
+
 
 --          f    g    h
 --       d <- c <- b <- a
 
-assoc-× :   { c₁  c₂ : Level } {a b c d : TwoObject  { c₁} } {f g h : Maybe (Arrow  { c₂ })} → 
-     [_==_] { c₁} { c₂} {a} {d}  (  _×_ { c₁} { c₂} {a} {b} {d} f ( _×_ { c₁} { c₂} {a} {b} {c} g h )  )
+assoc-× :   { c₁  c₂ : Level } {a b c d : TwoObject  { c₁} } {f g h : Maybe (TwoObject  { c₂ })} → 
+     _==_ { c₁} { c₂} {a} {d}  (  _×_ { c₁} { c₂} {a} {b} {d} f ( _×_ { c₁} { c₂} {a} {b} {c} g h )  )
                 (  _×_ { c₁} { c₂} {a} {c} {d}  ( _×_ { c₁} { c₂} {b} {c} {d} f g )   h )
 --    [ f × (g × h) == (f × g) × h ]
 assoc-× {_} {_} {_} {_} {_} {_} {nothing} {_} {_} = nothing
 assoc-× {_} {_} {_} {_} {_} {_} {just _} {nothing} {_} = nothing
-assoc-× {_} {_} {t0} {t0} {t0} {t0} {just id-t0} {just id-t0} {nothing} = nothing
-assoc-× {_} {_} {_} {_} {_} {_} {just _} {just _} {nothing} = {!!}
-assoc-× {_} {_} {t0} {t0} {t0} {t0} {just id-t0 } {just id-t0 } {just id-t0 } = just refl
-assoc-× {_} {_} {t0} {t0} {t0} {t1} {just id-t0 } {just id-t0 } {just id-t0 } = nothing
-assoc-× {_} {_} {_} {_} {_} {_} {just id-t0 } {just id-t0 } {just id-t0 } = ?
-assoc-× {_} {_} {_} {_} {_} {_} {_} {_} {_} = {!!}
+assoc-,AW(B {_} {_} {t0} {t0} {t0} {t0} {just _} {just _} {just _} = just refl
+assoc-,AW(B {_} {_} {t0} {t0} {t0} {t0} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t0} {t0} {t0} {t1} {just _} {just _} {just _} = just refl
+assoc-,AW(B {_} {_} {t0} {t0} {t0} {t1} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t0} {t0} {t1} {t0} {just _} {just _} {just _} =  {!!}
+assoc-,AW(B {_} {_} {t0} {t0} {t1} {t0} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t0} {just t0} = just refl
+assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t0} {just t1} = {!!}
+assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t1} {just t0} = just refl
+assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t1} {just t1} = {!!}
+assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t0} {just t0} = {!!}
+assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t0} {just t1} = just refl
+assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t1} {just t0} = {!!}
+assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t1} {just t1} = just refl
+assoc-,AW(B {_} {_} {t0} {t1} {t0} {t0} {just _} {just _} {just _} = nothing
+assoc-,AW(B {_} {_} {t0} {t1} {t0} {t0} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t0} {t1} {t0} {t1} {just _} {just _} {just _} = nothing
+assoc-,AW(B {_} {_} {t0} {t1} {t0} {t1} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t0} {t1} {t1} {t0} {just _} {just _} {just _} = nothing
+assoc-,AW(B {_} {_} {t0} {t1} {t1} {t0} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t0} {t1} {t1} {t1} {just _} {just _} {just _} = just refl
+assoc-,AW(B {_} {_} {t0} {t1} {t1} {t1} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t1} {t0} {t0} {t0} {just _} {just _} {just _} = nothing
+assoc-,AW(B {_} {_} {t1} {t0} {t0} {t0} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t1} {t0} {t0} {t1} {just _} {just _} {just _} = nothing
+assoc-,AW(B {_} {_} {t1} {t0} {t0} {t1} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t1} {t0} {t1} {t0} {just _} {just _} {just _} = nothing
+assoc-,AW(B {_} {_} {t1} {t0} {t1} {t0} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t1} {t0} {t1} {t1} {just _} {just _} {just _} = {!!}
+assoc-,AW(B {_} {_} {t1} {t0} {t1} {t1} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t1} {t1} {t0} {t0} {just _} {just _} {just _} = nothing
+assoc-,AW(B {_} {_} {t1} {t1} {t0} {t0} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t1} {t1} {t0} {t1} {just _} {just _} {just _} = nothing
+assoc-,AW(B {_} {_} {t1} {t1} {t0} {t1} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t1} {t1} {t1} {t0} {just _} {just _} {just _} = nothing
+assoc-,AW(B {_} {_} {t1} {t1} {t1} {t0} {just _} {just _} {nothing} = nothing
+assoc-,AW(B {_} {_} {t1} {t1} {t1} {t1} {just _} {just _} {just _} = just refl
+assoc-,AW(B {_} {_} {t1} {t1} {t1} {t1} {just _} {just _} {nothing} = nothing
 
-TwoId :  { c₁  c₂ : Level } {a : TwoObject  { c₁} } ->  Maybe (Arrow  { c₂ })
-TwoId {_} {_} {t0} = just id-t0
-TwoId {_} {_} {t1} = just id-t1
+
+
+
+TwoId :  { c₁  c₂ : Level } {a : TwoObject  { c₁} } ->  Maybe (TwoObject  { c₂ })
+TwoId {_} {_} {_} = just t0
 
 
 open import maybeCat  
@@ -78,7 +120,7 @@
 TwoCat : { c₁ c₂ ℓ : Level  } ->  Category   c₁  c₂  c₂
 TwoCat   {c₁}  {c₂} {ℓ} = record {
     Obj  = TwoObject  {c₁} ;
-    Hom = λ a b →    Maybe ( Arrow  { c₂ } ) ;
+    Hom = λ a b →    Maybe ( TwoObject  { c₂ } ) ;
     _o_ =  \{a} {b} {c} x y -> _×_ { c₁ } {  c₂} {a} {b} {c} x y ;
     _≈_ =    Eq  _≡_   ;
     Id  =  \{a} -> TwoId { c₁ } {  c₂} {a} ;
@@ -107,11 +149,11 @@
           fobj :  Obj I -> Obj A
           fobj t0 = a
           fobj t1 = 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 :  {x y : Obj I } ->  Maybe (TwoObject  {c₂} ) -> Hom MA (fobj x) (fobj y)
+          fmap {t0} {t1} (just t0) = record { hom = just f }
+          fmap {t0} {t1} (just t1) = record { hom = just g }
+          fmap {t0} {t0} (just t0)  = record { hom = just ( id1 A a )}
+          fmap {t1} {t1} (just t0)  = record { hom = just ( id1 A b )}
           fmap {_} {_}   _ = record { hom = nothing }
           open ≈-Reasoning (A) 
           identity :  {x : Obj I} → {!!}