Mercurial > hg > Members > kono > Proof > category

changeset 393:15d28525e756

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 15 Mar 2016 16:50:11 +0900
parents 61ec02585597
children aa94fdb12f1a
files limit-to.agda
diffstat 1 files changed, 66 insertions(+), 32 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Tue Mar 15 16:11:37 2016 +0900
+++ b/limit-to.agda	Tue Mar 15 16:50:11 2016 +0900
@@ -29,8 +29,6 @@
    id-t0 : Arrow  
    arrow-f :  Arrow
    arrow-g :  Arrow
-   reverse-f :  Arrow
-   reverse-g :  Arrow
    nil :  Arrow
 
 record RawHom {c₁ ℓ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set  (c₁  ⊔ ℓ) where
@@ -40,12 +38,7 @@
 open RawHom
 
 arrow2hom :  {c₁ ℓ : Level}  -> {a : TwoObject {c₁}  } {b : TwoObject {c₁}  } -> Arrow  {ℓ } -> RawHom  { c₁}  {ℓ } a b
-arrow2hom id-t0 =  record { RawMap = id-t0 } 
-arrow2hom arrow-f =  record { RawMap = arrow-f } 
-arrow2hom arrow-g =  record { RawMap = arrow-g } 
-arrow2hom reverse-f =  record { RawMap = reverse-f } 
-arrow2hom reverse-g =  record { RawMap = reverse-g } 
-arrow2hom nil =  record { RawMap = nil } 
+arrow2hom f =  record { RawMap = f } 
 
 record Two-Hom { c₁  ℓ : Level }   (a : TwoObject { c₁}  ) (b : TwoObject  { c₁} ) : Set   (c₁  ⊔ ℓ)  where
    field
@@ -62,12 +55,51 @@
 twocomp :  {ℓ : Level } -> Arrow {ℓ } -> Arrow {ℓ } -> Arrow {ℓ } 
 twocomp id-t0  f  = f
 twocomp f id-t0 = f
-twocomp arrow-f reverse-f = id-t0
-twocomp arrow-g reverse-g = id-t0
-twocomp reverse-f arrow-f = id-t0
-twocomp reverse-g arrow-g = id-t0
 twocomp _ _ = nil
 
+twocmp-associative :  {ℓ : Level } -> ( f : Arrow {ℓ } ) -> ( g : Arrow {ℓ } ) -> ( h : Arrow {ℓ } ) →  twocomp f  (twocomp g  h)  ≡  twocomp (twocomp f  g)  h 
+twocmp-associative id-t0 _ _ = refl
+twocmp-associative arrow-f id-t0 _  = refl
+twocmp-associative arrow-f arrow-f id-t0  = refl
+twocmp-associative arrow-f arrow-f arrow-f  = refl
+twocmp-associative arrow-f arrow-f arrow-g  = refl
+twocmp-associative arrow-f arrow-f nil  = refl
+twocmp-associative arrow-g id-t0 _  = refl
+twocmp-associative arrow-f arrow-g nil = refl
+twocmp-associative arrow-f arrow-g id-t0 = refl
+twocmp-associative arrow-f arrow-g arrow-f = refl
+twocmp-associative arrow-f arrow-g arrow-g = refl
+twocmp-associative arrow-f nil nil = refl
+twocmp-associative arrow-f nil id-t0 = refl
+twocmp-associative arrow-f nil arrow-f = refl
+twocmp-associative arrow-f nil arrow-g = refl
+twocmp-associative arrow-g arrow-f nil = refl
+twocmp-associative arrow-g arrow-f id-t0 = refl
+twocmp-associative arrow-g arrow-f arrow-f = refl
+twocmp-associative arrow-g arrow-f arrow-g = refl
+twocmp-associative arrow-g arrow-g nil = refl
+twocmp-associative arrow-g arrow-g id-t0 = refl
+twocmp-associative arrow-g arrow-g arrow-f = refl
+twocmp-associative arrow-g arrow-g arrow-g = refl
+twocmp-associative arrow-g nil nil = refl
+twocmp-associative arrow-g nil id-t0 = refl
+twocmp-associative arrow-g nil  arrow-f = refl
+twocmp-associative arrow-g nil  arrow-g = refl
+twocmp-associative nil id-t0 _ = refl
+twocmp-associative nil nil nil  = refl
+twocmp-associative nil nil id-t0  = refl
+twocmp-associative nil nil arrow-f  = refl
+twocmp-associative nil nil arrow-g  = refl
+twocmp-associative nil arrow-f nil  = refl
+twocmp-associative nil arrow-f id-t0 = refl
+twocmp-associative nil arrow-f arrow-f = refl
+twocmp-associative nil arrow-f arrow-g = refl
+twocmp-associative nil arrow-g nil  = refl
+twocmp-associative nil arrow-g id-t0 = refl
+twocmp-associative nil arrow-g arrow-f = refl
+twocmp-associative nil arrow-g arrow-g = refl
+
+
 _×_ :  { c₁  ℓ : Level }  -> {A B C : TwoObject { c₁} } →  Two-Hom { c₁}  {ℓ}  B C →  Two-Hom { c₁}  {ℓ}  A B  →  Two-Hom { c₁}  {ℓ}  A C 
 _×_   { c₁} {ℓ} {a} {b} {c} f g  = record { hom =  arrow ;
                     arrow-iso =  arrow-iso   (RawMap arrow  ) }
@@ -78,8 +110,6 @@
       arrow-iso   id-t0 = refl
       arrow-iso  arrow-f = refl
       arrow-iso  arrow-g = refl
-      arrow-iso  reverse-f = refl
-      arrow-iso  reverse-g = refl
       arrow-iso  nil = refl
 
 open Two-Hom
@@ -104,34 +134,38 @@
         ≡-cong = Relation.Binary.PropositionalEquality.cong 
         identityL : {A B : TwoObject} {f : Two-Hom A B} →  Map ( Two-id B × f ) ≡ Map f
         identityL {a} {b} {f} with Map f
-        identityL {t0} {t0} {f}  | id-t0 =  refl
-        identityL {t1} {t0} {f}  | id-t0 =  refl
-        identityL {t0} {t0} {f}  | nil =  refl
-        identityL {t0} {t1} {f}  | nil =  refl
-        identityL {t1} {t0} {f}  | nil =  refl
-        identityL {t1} {t1} {f}  | nil =  refl
-        identityL {a} {t1} {f}  | id-t0 =  let open ≡-Reasoning in
-              begin
-                  {!!}
-              ≡⟨ {!!} ⟩
-                 id-t0
-              ∎
-        identityL {_} {_} {f}  | _ =  {!!}
-
+        identityL {_} {_} {f}  | id-t0 =  refl
+        identityL {_} {_} {f}  | arrow-f =  refl
+        identityL {_} {_} {f}  | arrow-g =  refl
+        identityL {_} {_} {f}  | nil =  refl
         identityR : {A B : TwoObject} {f : Two-Hom A B} →  Map ( f × Two-id A  ) ≡ Map f
-        identityR {a} {b} {f} = {!!}
+        identityR {a} {b} {f} with Map f
+        identityR {_} {_} {f}  | id-t0 =  refl
+        identityR {_} {_} {f}  | arrow-f =  refl
+        identityR {_} {_} {f}  | arrow-g =  refl
+        identityR {_} {_} {f}  | nil =  refl
         o-resp-≈ : {A B C : TwoObject} {f g :  Two-Hom A B} {h i : Two-Hom B C} →
             Map f ≡ Map g → Map h ≡ Map i → Map ( h × f ) ≡ Map ( i × g )
         o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = let open ≡-Reasoning in
               begin
                  Map (h × f)
-              ≡⟨  ≡-cong (\x ->  RawMap ( arrow2hom  ( twocomp (Map h) x ) ) )  f≡g  ⟩
+              ≡⟨  ≡-cong (\x ->  RawMap ( arrow2hom {_} {_} {a} {c}  ( twocomp (Map h) x ) ) )  f≡g  ⟩
                  Map (h × g)
-              ≡⟨  ≡-cong (\x ->  RawMap ( arrow2hom  ( twocomp x (Map g) ) ) )  h≡i  ⟩
+              ≡⟨  ≡-cong (\x ->  RawMap ( arrow2hom {_} {_} {a} {c}  ( twocomp x (Map g) ) ) )  h≡i  ⟩
                  Map (i × g)
               ∎
         associative : {A B C D : TwoObject} {f : Two-Hom C D} {g : Two-Hom B C} {h : Two-Hom A B} → Map ( f × (g × h) ) ≡ Map ( (f × g) × h )
-        associative {_} {_} {_} {_} {f} {g} {h} = {!!}
+        associative {_} {_} {_} {_} {f} {g} {h}  =   let open ≡-Reasoning in
+              begin
+                 Map ( f × (g × h) )
+              ≡⟨⟩
+                 twocomp (RawMap (hom f)) (twocomp (RawMap (hom g)) (RawMap (hom h)))
+              ≡⟨ twocmp-associative   (RawMap (hom f)) (RawMap (hom g)) (RawMap (hom h))   ⟩
+                 twocomp (twocomp (RawMap (hom f)) (RawMap (hom g))) (RawMap (hom h))
+              ≡⟨⟩
+                 Map ( (f × g) × h )
+              ∎
+
 
 indexFunctor :  {c₁ c₂ ℓ : Level}  (A : Category c₁ c₂ ℓ) 
         ( a b : Obj A ) ( f g : Hom A a b )  ( nf : Hom A a b ) ( nf-rev : Hom A b a ) ( nidA : Hom A a a ) ( nidB : Hom A b b ) ->  Functor (TwoCat {c₁} {c₂} {ℓ} ) A