Mercurial > hg > Members > kono > Proof > category

changeset 405:4c34c0e3c4bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
no Maybe TwoCat in limit-to
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Mar 2016 12:44:43 +0900
parents 07bea66e5ceb
children 2fbd92ddecb5
files limit-to.agda
diffstat 1 files changed, 28 insertions(+), 49 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Sun Mar 20 12:32:13 2016 +0900
+++ b/limit-to.agda	Mon Mar 21 12:44:43 2016 +0900
@@ -29,6 +29,7 @@
 
 data Arrow {ℓ : Level }  : Set ℓ where
    id-t0 : Arrow  
+   id-t1 : Arrow  
    arrow-f :  Arrow
    arrow-g :  Arrow
    nil :  Arrow
@@ -44,6 +45,15 @@
 
 -- 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
@@ -55,58 +65,31 @@
 _×_   { 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 : TwoObject  {c₁} } -> Rel (Maybe (Arrow  { c₂ })) c₂ 
-_==_    =   Eq ( _≡_  ) 
-
-open  import  Relation.Binary.PropositionalEquality
-
-==-refl :    {   c₂ : Level }  {x : Maybe ( Arrow  { c₂ } ) } → x == x 
-==-refl  {_} {just x}  = just refl
-==-refl  {_} {nothing} = nothing
-
-==-sym :  {   c₂ : Level }  {x y : Maybe ( Arrow  { c₂ } ) }  → x == y  →  y == x 
-==-sym  (just x≈y) = just (sym x≈y)  
-==-sym   nothing    = nothing
-
-==-trans :   {   c₂ : Level }  -> {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
-
-
 
 open import maybeCat  
 
 
+open import Relation.Binary 
 TwoCat : { c₁ c₂ ℓ : Level  } ->  Category   c₁  c₂  c₂
 TwoCat   {c₁}  {c₂} {ℓ} = record {
     Obj  = TwoObject  {c₁} ;
-    Hom = λ a b →   Two-Hom {c₁ } { c₂}  a b   ; 
-    _o_ =  _×_  { c₁}  {c₂} ;
-    _≈_ = λ a b →   hom a == hom b  ;
-    Id  =  \{a} -> Two-id a ;
+    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  ;
     isCategory  = record {
-            isEquivalence =  record {refl = ==-refl  ; trans = ==-trans  ; sym = ==-sym   } ;
-            identityL  = \{a b f} -> identityL {a} {b} {f} ;
-            identityR  = \{a b f} -> identityR {a} {b} {f} ;
-            o-resp-≈  = \{a b c f g h i} -> o-resp-≈  {a} {b} {c} {f} {g} {h} {i} ;
-            associative  = \{a b c d f g h } -> associative  {a} {b} {c} {d} {f} {g} {h}
+            isEquivalence =  record {refl = refl  ; trans = ≡-trans  ; sym = ≡-sym   } ;
+            identityL  = {!!} ;
+            identityR  = {!!} ;
+            o-resp-≈  =  {!!} ;
+            associative  = {!!}
        } 
-   } where
-        ≡-cong = Relation.Binary.PropositionalEquality.cong 
-        identityL : {A B : TwoObject} {f : Two-Hom A B} →  hom ( Two-id B × f ) == hom f
-        identityL {a} {b} {f}  = {!!}
-        identityR : {A B : TwoObject} {f : Two-Hom A B} →  hom ( f × Two-id A  ) == hom f
-        identityR {a} {b} {f}  = {!!}
-        o-resp-≈ : {A B C : TwoObject} {f g :  Two-Hom A B} {h i : Two-Hom 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  = {!!}
-        associative : {A B C D : TwoObject} {f : Two-Hom C D} {g : Two-Hom B C} {h : Two-Hom A B} → hom ( f × (g × h) ) == hom ( (f × g) × h )
-        associative {_} {_} {_} {_} {f} {g} {h}  =   {!!}
+   } 
 
 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 {
          FObj = λ a → fobj a
-       ; FMap = λ f → fmap f
+       ; FMap = λ {a} {b} f → fmap {a} {b} f
        ; isFunctor = record {
              identity = \{x} -> identity {x}
              ; distr = \ {a} {b} {c} {f} {g}   -> distr1 {a} {b} {c} {f} {g} 
@@ -119,16 +102,12 @@
           fobj :  Obj I -> Obj A
           fobj t0 = a
           fobj t1 = b
-          fmap1 :  {x y : Obj I } ->  (Arrow  {c₂} ) -> Hom MA (fobj x) (fobj y)
-          fmap1 {t0} {t1} arrow-f = record { hom = just f }
-          fmap1 {t0} {t1} arrow-g = record { hom = just g }
-          fmap1 {t0} {t0} id-t0  = record { hom = just ( id1 A a )}
-          fmap1 {t1} {t1} id-t0  = record { hom = just ( id1 A b )}
-          fmap1 {_} {_}   _ = record { hom = nothing }
-          fmap :  {x y : Obj I } -> Hom I x y -> Hom MA (fobj x) (fobj y)
-          fmap {x} {y} f  with ( hom f )
-          fmap {x} {y} f  | nothing = record { hom = nothing }
-          fmap {x} {y} _  | just f = fmap1 {x} {y}  f 
+          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 {_} {_}   _ = record { hom = nothing }
           open ≈-Reasoning (A) 
           identity :  {x : Obj I} → {!!}
           identity {t0}  =  {!!}