Mercurial > hg > Members > kono > Proof > category

changeset 389:79c7ab66152b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
another try ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 15 Mar 2016 10:52:39 +0900
parents a0ab2643eee7
children 1301270b8942
files limit-to.agda
diffstat 1 files changed, 48 insertions(+), 99 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Mon Mar 14 22:35:47 2016 +0900
+++ b/limit-to.agda	Tue Mar 15 10:52:39 2016 +0900
@@ -27,39 +27,68 @@
 
 data Arrow {ℓ : Level }  : Set ℓ where
    id-t0 : Arrow  
+   id-t1 : Arrow  
    arrow-f :  Arrow
    arrow-g :  Arrow
+   nil :  Arrow -- inconsitent hom
 
 record RawHom {c₁ ℓ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set  (c₁  ⊔ ℓ) where
    field
-       RawMap    : Maybe ( Arrow  {ℓ })
+       RawMap    : Arrow  {ℓ }
 
 open RawHom
 
+arrow2hom :  {c₁ ℓ : Level}  -> (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) -> Arrow  {ℓ } -> RawHom  { c₁}  {ℓ } a b
+arrow2hom t0 t0 id-t0 =  record { RawMap = id-t0  } 
+arrow2hom t1 t1 id-t1 =  record { RawMap = id-t1  } 
+arrow2hom t0 t1 arrow-f =  record { RawMap = arrow-f } 
+arrow2hom t0 t1 arrow-g =  record { RawMap = arrow-g  } 
+arrow2hom _ _ _  =  record { RawMap = nil  } 
+
 record Two-Hom { c₁  ℓ : Level }   (a : TwoObject { c₁}  ) (b : TwoObject  { c₁} ) : Set   (c₁  ⊔ ℓ)  where
    field
       hom : RawHom { c₁}  {ℓ } a b
-   Map : Maybe Arrow
+      arrow-iso : arrow2hom a b ( RawMap hom ) ≡ hom
+   Map : Arrow
    Map = RawMap hom
 
 Two-id :  {c₁ ℓ : Level } -> (a : TwoObject {c₁} ) ->   Two-Hom {c₁} { ℓ} a a 
-Two-id t0  = record { hom = record { RawMap = just id-t0  } }
-Two-id t1  = record { hom = record { RawMap = just id-t0  } }
+Two-id t0  = record { hom = record { RawMap = id-t0  } ;  arrow-iso = refl }
+Two-id t1  = record { hom = record { RawMap = id-t1  } ;  arrow-iso = refl }
 
 Two-nothing : {c₁ ℓ : Level } -> ( a b : TwoObject  {c₁} ) -> Two-Hom  {c₁} { ℓ} a b
-Two-nothing a b  = record { hom = record { RawMap = nothing  } }
-
-open Two-Hom
+Two-nothing a b  = record { hom = record { RawMap = nil } ; arrow-iso = arrow-iso  a b }
+   where
+      arrow-iso : {c₁ ℓ : Level } -> ( a b : TwoObject  {c₁} ) -> arrow2hom {c₁} {ℓ } a b nil ≡ record { RawMap = nil }
+      arrow-iso  t0 t0 =  refl
+      arrow-iso  t0 t1 =  refl
+      arrow-iso  t1 t0 =  refl
+      arrow-iso  t1 t1 =  refl
 
 -- arrow composition
 
-twocomp :  {ℓ : Level } -> Maybe (Arrow {ℓ }) -> Maybe (Arrow {ℓ }) -> Maybe (Arrow {ℓ } )
-twocomp (just id-t0) (just f)  = just f
-twocomp (just f) (just id-t0) = just f
-twocomp _ _ = nothing
+twocomp :  {ℓ : Level } -> Arrow {ℓ } -> Arrow {ℓ } -> Arrow {ℓ } 
+twocomp id-t0  f  = f
+twocomp f id-t0 = f
+twocomp _ _ = nil
 
 _×_ :  { 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 = record { RawMap =  twocomp (Map f) (Map g) }}
+_×_   { c₁} {ℓ} {a} {b} {c} f g  = record { hom = 
+           record { RawMap =     twocomp  {ℓ} (Two-Hom.Map f) (Two-Hom.Map g) } ;  
+                    arrow-iso =  arrow-iso a c ( twocomp  {ℓ} (Two-Hom.Map f) (Two-Hom.Map g) ) }
+   where
+      arrow-iso : {c₁ ℓ : Level } -> ( a b : TwoObject  {c₁} ) -> (f : Arrow { ℓ} ) -> arrow2hom {c₁} {ℓ } a b f ≡ record { RawMap = f }
+      arrow-iso t0 t0 id-t0  = refl
+      arrow-iso t1 t1 id-t1  = refl
+      arrow-iso t0 t1 arrow-f  = refl
+      arrow-iso t0 t1 arrow-g  = refl
+      arrow-iso t0 t0 nil  = refl
+      arrow-iso t0 t1 nil  = refl
+      arrow-iso t1 t0 nil  = refl
+      arrow-iso t1 t1 nil  = refl
+      arrow-iso _ _ _  = {!!}
+
+open Two-Hom
 
 
 TwoCat : { c₁ c₂ ℓ : Level  } ->  Category   c₁  (ℓ ⊔ c₁)  ℓ
@@ -80,33 +109,9 @@
         open  import  Relation.Binary.PropositionalEquality
         ≡-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} | nothing  = refl
-        identityL {t0} {t1} {f} | nothing  = refl
-        identityL {t1} {t0} {f} | nothing  = refl
-        identityL {t1} {t1} {f} | nothing  = refl
-        identityL {t1} {t1} {f} | just id-t0  = refl
-        identityL {t0} {t1} {f} | just arrow-f  = refl
-        identityL {t0} {t1} {f} | just arrow-g  = refl
-        identityL {t0} {t0} {f} | just id-t0  = refl
-        identityL {a} {t0} {f} | just fa =   refl
-        identityL {a} {t1} {f} | just fa =   refl
+        identityL {a} {b} {f}  = {!!}
         identityR : {A B : TwoObject} {f : Two-Hom A B} →  Map ( f × Two-id A  ) ≡ Map f
-        identityR {a} {b} {f} with Map f
-        identityR {t0} {t0} {f} | nothing  = refl
-        identityR {t0} {t1} {f} | nothing  = refl
-        identityR {t1} {t0} {f} | nothing  = refl
-        identityR {t1} {t1} {f} | nothing  = refl
-        identityR {t1} {t1} {f} | just id-t0  = refl
-        identityR {t0} {t1} {f} | just arrow-f  = refl
-        identityR {t0} {t1} {f} | just arrow-g  = refl
-        identityR {t0} {t0} {f} | just id-t0  = refl
-        identityR {t0} {_} {f} | just id-t0 = refl
-        identityR {t0} {_} {f} | just arrow-f = refl
-        identityR {t0} {_} {f} | just arrow-g = refl
-        identityR {t1} {_} {f} | just id-t0 = refl
-        identityR {t1} {_} {f} | just arrow-f = refl
-        identityR {t1} {_} {f} | just arrow-g = refl
+        identityR {a} {b} {f} = {!!}
         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
@@ -122,41 +127,7 @@
                  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} with Map f | Map g | Map h
-        associative {_} {_} {_} {_} {f} {g} {h} | nothing | _ | _ =  refl
-        associative {_} {_} {_} {_} {f} {g} {h} | just id-t0 | nothing | _ = refl
-        associative {_} {_} {_} {_} {f} {g} {h} | just arrow-f | nothing | _ = refl
-        associative {_} {_} {_} {_} {f} {g} {h} | just arrow-g | nothing | _ = refl
-        associative {_} {_} {_} {_} {f} {g} {h} | just id-t0 | just id-t0 | nothing =  refl
-        associative {_} {_} {_} {_} {f} {g} {h} | just id-t0 | just arrow-f | nothing =  refl
-        associative {_} {_} {_} {_} {f} {g} {h} | just id-t0 | just arrow-g | nothing =  refl
-        associative {_} {_} {_} {_} {f} {g} {h} | just arrow-f | just id-t0 | nothing =  refl
-        associative {_} {_} {_} {_} {f} {g} {h} | just arrow-f | just arrow-f | nothing =  refl
-        associative {_} {_} {_} {_} {f} {g} {h} | just arrow-f | just arrow-g | nothing =  refl
-        associative {_} {_} {_} {_} {f} {g} {h} | just arrow-g | just id-t0 | nothing =  refl
-        associative {_} {_} {_} {_} {f} {g} {h} | just arrow-g | just arrow-f | nothing =  refl
-        associative {_} {_} {_} {_} {f} {g} {h} | just arrow-g | just arrow-g | nothing =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just id-t0 | just id-t0 | just h =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just id-t0 | just arrow-f | just id-t0 =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just id-t0 | just arrow-g | just id-t0 =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just id-t0 | just arrow-f | just arrow-f =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just id-t0 | just arrow-f | just arrow-g =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just id-t0 | just arrow-g | just arrow-f =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just id-t0 | just arrow-g | just arrow-g =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just arrow-f | just id-t0 | just h =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just arrow-f | just arrow-f | just id-t0 =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just arrow-f | just arrow-f | just arrow-f =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just arrow-f | just arrow-f | just arrow-g =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just arrow-f | just arrow-g | just id-t0 =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just arrow-f | just arrow-g | just arrow-f =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just arrow-f | just arrow-g | just arrow-g =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just id-t0 | just h =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just arrow-f | just id-t0 =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just arrow-f | just arrow-f =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just arrow-f | just arrow-g =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just arrow-g | just id-t0 =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just arrow-g | just arrow-f =  refl
-        associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just arrow-g | just arrow-g =  refl
+        associative {_} {_} {_} {_} {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
@@ -173,13 +144,8 @@
           fobj :  Obj I -> Obj A
           fobj t0 = a
           fobj t1 = b
-          fmap1 :  {x y : Obj I } -> Hom I x y -> Maybe Arrow -> Hom A (fobj x) (fobj y)
-          fmap1 {t0} {t1} x  ( just arrow-f ) = f
-          fmap1 {t0} {t1} x  ( just arrow-g ) = g
-          fmap1 {t0} {t1} x   _ = nf
-          fmap1 {t0} {t0} x   _ = id1 A a
-          fmap1 {t1} {t1} x   _ = id1 A b
-          fmap1 {t1} {t0} x   _ = nf-rev
+          fmap1 :  {x y : Obj I } -> Hom I x y -> Arrow -> Hom A (fobj x) (fobj y)
+          fmap1 {_} {_} x  f = {!!}
           fmap :  {x y : Obj I } -> Hom I x y -> Hom A (fobj x) (fobj y)
           fmap {x} {y} f  = fmap1 {x} {y} f ( Map f)
           open ≈-Reasoning (A) 
@@ -187,26 +153,9 @@
           identity {t0}  =  refl-hom
           identity {t1}  =  refl-hom
           distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → A [ fmap (I [ g₁ o f₁ ]) ≈ A [ fmap g₁ o fmap f₁ ] ]
-          distr1 {t0} {t0} {t0} {f1} {g1}  = sym idL
-          distr1 {t1} {t0} {t0} {f1} {g1}  = sym idL
-          distr1 {t1} {t1} {t0} {f1} {g1}  = sym idR
-          distr1 {t1} {t1} {t1} {f1} {g1}  = sym idR
-          distr1 {a1} {b1} {c} {f1} {g1}  with Map f1 | Map g1
-          distr1 {t0} {t1} {t1} {f1} {g1} | fa  | just arrow-f  = begin
-                    fmap1 {!!} ( twocomp (just arrow-f)  fa )
-                ≈⟨ {!!} ⟩
-                    fmap1 f1 fa
-                ≈⟨ sym idL  ⟩
-                    id1 A b  o fmap1 f1 fa
-                ≈⟨⟩
-                    fmap1 g1 (just arrow-f)  o fmap1 f1 fa
-                ∎ 
-          distr1 {a1} {b1} {c} {f1} {g1}  | _ | _ = {!!}
+          distr1 = {!!}
           ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → I [ f ≈ g ] → A [ fmap f ≈ fmap g ]
-          ≈-cong {t0} {t0} {f1} {g1}  f≈g = refl-hom
-          ≈-cong {t1} {t1} {f1} {g1}  f≈g = refl-hom
-          ≈-cong {t1} {t0} {f1} {g1}  f≈g = refl-hom
-          ≈-cong {t0} {t1} {f1} {g1}  f≈g = ≡-cong f≈g (\x -> fmap1 g1 x)     
+          ≈-cong   {_} {_} {f1} {g1} f≈g = {!!} -- ≡-cong f≈g (\x -> fmap1 g1 x)     
 
 
 ---  Equalizer