Mercurial > hg > Members > kono > Proof > category

changeset 416:e4a2544d468c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good so A [ g o f ] should be nothing in codomain Category
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 23 Mar 2016 22:47:32 +0900
parents dd086f5fb29f
children 1e76e611d454
files limit-to.agda
diffstat 1 files changed, 54 insertions(+), 229 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Wed Mar 23 19:52:27 2016 +0900
+++ b/limit-to.agda	Wed Mar 23 22:47:32 2016 +0900
@@ -7,6 +7,7 @@
 open import HomReasoning
 open import Relation.Binary.Core
 open import Data.Maybe
+open import maybeCat
 open Functor
 
 
@@ -27,225 +28,31 @@
    t0 : TwoObject
    t1 : TwoObject
 
-data Arrow {ℓ : Level }  : Set ℓ where
-   id-t0 : Arrow
-   id-t1 : Arrow
-   arrow-f :  Arrow
-   arrow-g :  Arrow
-
-record TwoHom {c₁ c₂ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set   c₂ where
-   field
-       RawHom   :   Maybe ( Arrow {c₂} )
-
-open TwoHom
-
-hom :  ∀{ c₁ c₂ }  { a b : TwoObject  {c₁} } -> ∀ (f :  TwoHom {c₁}  {c₂ } a b ) → Maybe ( Arrow  {c₂} )
-hom {_} {_} {a} {b} f with RawHom  f
-hom {_} {_} {t0} {t0} _ | nothing = nothing
-hom {_} {_} {t0} {t0} _ | just id-t0 = just id-t0
-hom {_} {_} {t1} {t1} _ | just id-t1 = just id-t1
-hom {_} {_} {t0} {t1} _ | just arrow-f = just arrow-f
-hom {_} {_} {t0} {t1} _ | just arrow-g = just arrow-g
-hom {_} {_} {_ } {_ } _ | _ = nothing
-
-
-open TwoHom
-
--- arrow composition
-
-
-_×_ :  ∀ {c₁  c₂}  -> {a b c : TwoObject {c₁}} →  ( TwoHom {c₁}  {c₂} b c ) →  ( TwoHom {c₁} {c₂} a b )  →  ( TwoHom {c₁}  {c₂} a c )
-_×_  {c₁}  {c₂}  {a} {b} {c} f g with hom f | hom g
-... |   nothing       | _                = record { RawHom =  nothing }
-... |  (just _)       | nothing          = record { RawHom =  nothing }
-... |  (just id-t1)   | (just arrow-f)   = record { RawHom =  just arrow-f }
-... |  (just id-t1)   | (just arrow-g)   = record { RawHom =  just arrow-g }
-... |  (just id-t1)   | (just id-t1 )    = record { RawHom =  just id-t1 }
-... |  (just arrow-f) | (just id-t0)     = record { RawHom =  just arrow-f }
-... |  (just arrow-g) | (just id-t0)     = record { RawHom =  just arrow-g }
-... |  (just id-t0)   | (just id-t0 )    = record { RawHom =  just id-t0 }
-... |  (just _)       | (just _)         = record { RawHom =  nothing }
-
-
-_==_ :  ∀{c₂ }   ->  Rel (Maybe (Arrow  {c₂} )) (c₂)
-_==_   =  Eq   _≡_
 
-map2hom :  ∀{ c₁ c₂ } ->  {a b  : TwoObject {c₁}} →  Maybe ( Arrow  {c₂} ) ->  TwoHom {c₁}  {c₂ } a b
-map2hom {_} {_} {t1} {t1} (just id-t1)  = record { RawHom =  just id-t1 }
-map2hom {_} {_} {t0} {t1} (just arrow-f) = record { RawHom =  just arrow-f }
-map2hom {_} {_} {t0} {t1} (just arrow-g) = record { RawHom =  just arrow-g }
-map2hom {_} {_} {t0} {t0} (just id-t0)   = record { RawHom =  just id-t0 }
-map2hom {_} {_} {_} {_} _       = record { RawHom =  nothing }
-
-record TwoHom1 {c₁ c₂ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set   c₂ where
-   field
-       Map       :   TwoHom {c₁}  {c₂ } a b
-       iso-Map   :   Map ≡  map2hom ( hom Map )
-
-==refl :  ∀{  c₂ }  ->  ∀ {x : Maybe (Arrow  {c₂} )} → x == x
-==refl {_} {just x}  = just refl
-==refl {_} {nothing} = nothing
-
-==sym :  ∀{ c₂ }   -> ∀ {x y :  Maybe (Arrow  {c₂} )} → _==_ x  y → _==_ y  x
-==sym (just x≈y) = just (≡-sym x≈y)
-==sym nothing    = nothing
-
-==trans :  ∀{ c₂ }   -> ∀ {x y z :   Maybe (Arrow  {c₂} )  } →
-         x == y → y == z  → x == z
-==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z)
-==trans nothing    nothing    = nothing
-
+record TwoCat  {ℓ c₁ c₂ : Level  } (A : Category  c₁ c₂ ℓ)  ( a b : Obj A ) ( f g : Hom A a b ): Set  (c₂ ⊔ c₁ ⊔ ℓ)  where
+    field
+         obj→ : Obj A  -> TwoObject  { c₁}
+         hom→ : {a b : Obj A} -> Hom A a b -> TwoObject { c₁}
+         inv : {a b : Obj A} -> Hom A a b -> Hom A b a
+         iso→ : {a b : Obj A} -> ( h : Hom A a b ) -> A [ A [ inv h o h ]  ≈  id1 A a ]
+         iso← : {a b : Obj A} -> ( h : Hom A a b ) -> A [ A [ h o inv h ]  ≈  id1 A b ]
+    obj← : TwoObject  {c₁} -> Obj A  
+    obj←  t0 = a
+    obj←  t1 = b
+    hom← :  TwoObject  {c₁} -> Hom A a b 
+    hom← t0 = f
+    hom← t1 = g
 
-module ==-Reasoning {c₁ c₂ : Level} where
-
-        infixr  2 _∎
-        infixr 2 _==⟨_⟩_ _==⟨⟩_
-        infix  1 begin_
-
-
-        data _IsRelatedTo_   (x y : (Maybe (Arrow  {c₂} ))) :
-                             Set  c₂ where
-            relTo : (x≈y : x  == y  ) → x IsRelatedTo y
-
-        begin_ :  { a b : TwoObject  {c₁} } {x : Maybe (Arrow  {c₂} ) } {y : Maybe (Arrow  {c₂} )} →
-                   x IsRelatedTo y →  x ==  y
-        begin relTo x≈y = x≈y
-
-        _==⟨_⟩_ :  { a b : TwoObject  {c₁} } (x :  Maybe (Arrow  {c₂} )) {y z :  Maybe (Arrow  {c₂} ) } →
-                    x == y  → y IsRelatedTo z → x IsRelatedTo z
-        _ ==⟨ x≈y ⟩ relTo y≈z = relTo (==trans x≈y y≈z)
-
-        _==⟨⟩_ :   { a b : TwoObject  {c₁} }(x : Maybe (Arrow  {c₂} )) {y : Maybe (Arrow  {c₂} )}
-                    → x IsRelatedTo y → x IsRelatedTo y
-        _ ==⟨⟩ x≈y = x≈y
-
-        _∎ :   { a b : TwoObject  {c₁} }(x :  Maybe (Arrow  {c₂} )) → x IsRelatedTo x
-        _∎ _ = relTo ==refl
-
+open TwoCat
 
 
---          f    g    h
---       d <- c <- b <- a
-
-assoc-× :   {c₁  c₂ : Level } {a b c d : TwoObject  {c₁} }
-       {f : (TwoHom {c₁}  {c₂ } c d )} →
-       {g : (TwoHom {c₁}  {c₂ } b c )} →
-       {h : (TwoHom {c₁}  {c₂ } a b )} →
-       hom ( f × (g × h)) == hom ((f × g) × h )
-assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with  hom f | hom g | hom h
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t0} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t1} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t1} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t1} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t0} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t1} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t1} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t1} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t0} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t1} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t1} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t1} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t0} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t1} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t1} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t1} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0   | just id-t0   | just id-t0  = ==refl
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0   | just id-t0  = ==refl
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0   | just id-t0  = ==refl
-assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1   | just arrow-f | just id-t0  = ==refl
-assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1   | just arrow-g | just id-t0  = ==refl
-assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1   | just id-t1   | just arrow-f = ==refl
-assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1   | just id-t1   | just arrow-g = ==refl
-assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1   | just id-t1   | just id-t1  = ==refl
---  remaining all failure case
-assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} | just _ | just _ | nothing = {!!}
-assoc-× {c₁} {c₂} {t1} {t0} {_} {_} {f} {g} {h} | just _   | just _   | just _  = let open ==-Reasoning  {c₁}  {c₂} in
-                begin
-                   {!!}
-                ==⟨ {!!}  ⟩
-                  {!!}
-                ∎
-... | just _ | just _ | just _ =  let open ==-Reasoning  {c₁}  {c₂} in
-                begin
-                   {!!}
-                ==⟨ {!!}  ⟩
-                  {!!}
-                ∎
+open MaybeHom
 
 
-TwoId :  {c₁  c₂ : Level } (a : TwoObject  {c₁} ) ->  (TwoHom {c₁}  {c₂ } a a )
-TwoId {_} {_} t0 = record { RawHom =  just id-t0 }
-TwoId {_} {_} t1 = record { RawHom =  just id-t1 }
-
-open import maybeCat
-
---        identityL  {c₁}  {c₂}  {_} {b} {nothing}  =   let open ==-Reasoning  {c₁}  {c₂} in
---                begin
---                   (TwoId b × nothing)
---                ==⟨ {!!}  ⟩
---                  nothing
---                ∎
-
-open import Relation.Binary
-TwoCat : {c₁ c₂ ℓ : Level  } ->  Category   c₁  c₂  c₂
-TwoCat   {c₁}  {c₂} {ℓ} = record {
-    Obj  = TwoObject  {c₁} ;
-    Hom = λ a b →    ( TwoHom {c₁}  {c₂ } a b ) ;
-    _o_ =  \{a} {b} {c} x y -> _×_ {c₁ } { c₂} {a} {b} {c} x y ;
-    _≈_ =  \x y -> hom x == hom y ;
-    Id  =  \{a} -> TwoId {c₁ } { c₂} a ;
-    isCategory  = record {
-            isEquivalence =  record {refl = ==refl ; trans = ==trans ; sym = ==sym } ;
-            identityL  = \{a b f} -> identityL {c₁}  {c₂ } {a} {b} {f} ;
-            identityR  = \{a b f} -> identityR {c₁}  {c₂ } {a} {b} {f} ;
-            o-resp-≈  = \{a b c f g h i} ->  o-resp-≈  {c₁}  {c₂ } {a} {b} {c} {f} {g} {h} {i} ;
-            associative  = \{a b c d f g h } -> assoc-×   {c₁}  {c₂} {a} {b} {c} {d} {f} {g} {h}
-       }
-   }  where
-        identityL :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →  hom ((TwoId B)  × f)  == hom f
-        identityL  {c₁}  {c₂}  {_} {_} {f}  with hom f
-        identityL  {c₁}  {c₂}  {t0} {t0} {_} | nothing  = nothing
-        identityL  {c₁}  {c₂}  {t0} {t1} {_} | nothing  = nothing
-        identityL  {c₁}  {c₂}  {t1} {t0} {_} | nothing  = nothing
-        identityL  {c₁}  {c₂}  {t1} {t1} {_} | nothing  = nothing
-        identityL  {c₁}  {c₂}  {t0} {t0} {_} | just id-t0 = ==refl
-        identityL  {c₁}  {c₂}  {t0} {t1} {_} | just id-t0 =  let open ==-Reasoning  {c₁}  {c₂} in
-                begin
-                   nothing
-                ==⟨ {!!}  ⟩
-                  just ?
-                ∎
-        identityL  {c₁}  {c₂}  {_} {_} {_} | just id-t0 = {!!}
-        identityL  {c₁}  {c₂}  {_} {_} {_} | just id-t1 = {!!}
-        identityL  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-f = ==refl
-        identityL  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-g = ==refl
-        identityL  {c₁}  {c₂}  {_} {_} {_} | just arrow-f = {!!}
-        identityL  {c₁}  {c₂}  {_} {_} {_} | just arrow-g = {!!}
-        identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →   hom ( f × TwoId A )  == hom f
-        identityR  {c₁}  {c₂}  {_} {_} {_}  =   {!!}
-        o-resp-≈ :  {c₁  c₂ : Level } {A B C : TwoObject  {c₁} } {f g :  ( TwoHom {c₁}  {c₂ } A B)} {h i : ( TwoHom B C)} →
-            hom f == hom g → hom h == hom i → hom ( h × f ) == hom ( i × g )
-        o-resp-≈  {_} {_} {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = {!!}
-
-
-indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj (MaybeCat A )) ( f g : Hom A a b ) ->  Functor (TwoCat {c₁} {c₂} {c₂} ) (MaybeCat A )
-indexFunctor  {c₁} {c₂} {ℓ} A  a b f g = record {
+indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) ->  
+    TwoCat A a b f g ->
+    Functor A (MaybeCat A )
+indexFunctor  {c₁} {c₂} {ℓ} A  a b f g two = record {
          FObj = λ a → fobj a
        ; FMap = λ {a} {b} f → fmap {a} {b} f
        ; isFunctor = record {
@@ -254,21 +61,39 @@
              ; ≈-cong = \ {a} {b} {c} {f}   -> ≈-cong  {a} {b} {c} {f}
        }
       } where
-          I = TwoCat  {c₁} {c₂} {ℓ}
           MA = MaybeCat A
           open ≈-Reasoning (MA)
-          fobj :  Obj I -> Obj A
-          fobj t0 = a
-          fobj t1 = b
-          fmap :  {x y : Obj I } ->  (TwoHom {c₁}  {c₂} x y  ) -> Hom MA (fobj x) (fobj y)
-          fmap  = {!!}
-          open ≈-Reasoning (A)
-          identity :  {x : Obj I} → {!!}
-          identity {t0}  =  {!!}
-          identity {t1}  =  {!!}
-          distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → {!!}
-          distr1 {a1} {b1} {c} {f1} {g1}   = {!!}
-          ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → _[_≈_] I f g → {!!}
+          fobj :  Obj A -> Obj A
+          fobj x with obj→ two x
+          fobj _ | t0 = a
+          fobj _ | t1 = b
+          fmap :  {x y : Obj A } ->  (Hom A  x y  ) -> Hom MA (fobj x) (fobj y)
+          fmap  {x} {y} h with  obj→ two x |  obj→ two y | hom→ two f
+          fmap  {_} {_} h | t0 | t1 | t0 = record { hom = just f }
+          fmap  {_} {_} h | t0 | t1 | t1 = record { hom = just g }
+          fmap  {_} {_} h | t1 | t0 | t0 = record { hom = just (inv two f) }
+          fmap  {_} {_} h | t1 | t0 | t1 = record { hom = just (inv two g) }
+          fmap  {x} {_} h | t0 | t0 | _ = id1 MA ( obj←  two t0 )
+          fmap  {x} {_} h | t1 | t1 | _ = id1 MA ( obj←  two t1 )
+          identity :  {x : Obj A} → MA [ fmap ( id1 A x  )  ≈  id1 MA ( fobj x )  ]
+          identity {x} with  obj→ two x
+          identity | t0  = refl-hom 
+          identity | t1  = refl-hom 
+          distr1 : {a₁ : Obj A} {b₁ : Obj A} {c : Obj A} {f₁ : Hom A a₁ b₁} {g₁ : Hom A b₁ c} →  
+                MA [ fmap (A [ g₁ o f₁ ]) ≈  MA [ fmap g₁ o fmap f₁ ] ]
+          distr1 {a1} {b1} {c} {f1} {g1} with  obj→ two a1 |  obj→ two b1  | obj→ two c | hom→ two f | hom→ two g 
+          distr1 {a1} {b1} {c} {f1} {g1} |  t0 | t0 | t0 | _ | _ =  {!!}
+          distr1 {a1} {b1} {c} {f1} {g1} |  t0 | t0 | t1 | _ | _ =  {!!}
+          distr1 {a1} {b1} {c} {f1} {g1} |  t0 | t1 | t1 | _ | _ =  {!!}
+          distr1 {a1} {b1} {c} {f1} {g1} |  t1 | t1 | t1 | _ | _ =  {!!}
+          distr1 {a1} {b1} {c} {f1} {g1} |  t1 | t0 | t0 | _ | _ =  {!!}
+          distr1 {a1} {b1} {c} {f1} {g1} |  t1 | t1 | t0 | _ | _ =  {!!}
+          -- next  two cases require the inverse of f and g
+          -- if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
+          --    so A [ g o  f ] should be nothing in codomain Category
+          distr1 {a1} {b1} {c} {f1} {g1} |  t1 | t0 | t1 | _ | _ =  {!!}
+          distr1 {a1} {b1} {c} {f1} {g1} |  t0 | t1 | t0 | _ | _ =  {!!}
+          ≈-cong :   {a : Obj A} {b : Obj A} {f g : Hom A a b}  → _[_≈_] A f g → {!!}
           ≈-cong   {_} {_} {f1} {g1} f≈g = {!!}
 
 
@@ -294,9 +119,9 @@
         fe=ge =  fe=ge
         ; k = λ {d} h fh=gh → k {d} h fh=gh
         ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
-        ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
-     } where
-         I = TwoCat {c₁} {c₂} {ℓ }
+        ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' } where
+         I = A
+         MA = MaybeCat A
          Γ = {!!}
          nmap :  (x : Obj I) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A I d) x) (FObj Γ x)
          nmap x d h = {!!}