Mercurial > hg > Members > kono > Proof > category

changeset 445:00cf84846d81

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cont..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 14 Oct 2016 19:44:59 +0900
parents 59e47e75188f
children b9dec59bc706
files limit-to.agda
diffstat 1 files changed, 35 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Fri Oct 14 19:12:01 2016 +0900
+++ b/limit-to.agda	Fri Oct 14 19:44:59 2016 +0900
@@ -25,7 +25,7 @@
    t0 : Object4
    t1 : Object4
    t2 : Object4
-   t4 : Object4
+   t3 : Object4
 
 record TwoHom {c₁ : Level} {Object : Set c₁}   (a b : Object) : Set c₁ where
 
@@ -45,8 +45,8 @@
 
 
 open import Relation.Binary
-TwoCat : {c₁ ℓ : Level  } →  (Object : Set  c₁) → Category   c₁ c₁ c₁ 
-TwoCat   {c₁}  {ℓ} Object = record {
+TwoCat : {c₁ : Level  } →  (Object : Set  c₁) → Category   c₁ c₁ c₁ 
+TwoCat   {c₁} Object = record {
     Obj  = Object   ;
     Hom = λ a b →    ( TwoHom {c₁}  {Object} a b ) ;
     _o_ =  λ{a} {b} {c} x y → _×_ {c₁ }  {Object} {a} {b} {c} x y ;
@@ -61,18 +61,18 @@
        }
    }  where
         identityL :   {A B : Object } {f : ( TwoHom {c₁} {Object}  A B) } →  ((TwoId {_} {Object} B)  × f)   ≡  f
-        identityL = {!!}
+        identityL =  refl
         identityR :  {A B : Object } {f : ( TwoHom {_}  {Object} A B) } →   ( f × TwoId A )   ≡  f
-        identityR = {!!}
+        identityR = refl
         o-resp-≈ :   {A B C : Object  } {f g :  ( TwoHom {c₁}  {Object} A B)} {h i : ( TwoHom B C)} →
             f  ≡  g → h  ≡  i → ( h × f )  ≡  ( i × g )
-        o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  f==g h==i  = {!!}
+        o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  refl refl  = refl
         assoc-× :    {a b c d : Object  }
                {f : (TwoHom {c₁}   {Object} c d )} →
                {g : (TwoHom {c₁}   {Object} b c )} →
                {h : (TwoHom {c₁}   {Object} a b )} →
                ( f × (g × h)) ≡ ((f × g) × h )
-        assoc-×  {a} {b} {c} {d} {f} {g} {h} = {!!}
+        assoc-×  {a} {b} {c} {d} {f} {g} {h} = refl
 
 
 
@@ -87,7 +87,7 @@
 
 
 
-indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj A) ( f g : Hom A a b ) →  Functor (TwoCat Object4 ) A
+indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj A) ( f g : Hom A a b ) →  Functor (TwoCat {c₁} Object4 ) A
 indexFunctor  {c₁} {c₂} {ℓ} A none a b f g = record {
          FObj = λ a → fobj a
        ; FMap = λ {a} {b} f → fmap {a} {b} f
@@ -97,18 +97,40 @@
              ; ≈-cong = λ {a} {b} {c} {f}   → ≈-cong  {a} {b} {c} {f}
        }
       } where
-          I = TwoCat  Object4
+          I = TwoCat  {c₁}  Object4
           fobj :  Obj I → Obj A
-          fobj = {!!}
+          fobj t0 = a
+          fobj t1 = b
+          fobj t2 = a
+          fobj t3 = b
           fmap :  {x y : Obj I } →  (TwoHom {c₁}  {Object4} x y  ) → Hom A (fobj x) (fobj y)
-          fmap  {_} {_} h  = {!!}
+          fmap  {t0} {t0} h  = id1 A a
+          fmap  {t1} {t1} h  = id1 A b
+          fmap  {t2} {t2} h  = id1 A a
+          fmap  {t3} {t3} h  = id1 A b
+          fmap  {t0} {t1} h  = f
+          fmap  {t2} {t3} h  = g
+          fmap  {_} {_} h  =  nil none
           open  ≈-Reasoning A
           ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → I [ f ≈ g ]  → A [ fmap f ≈ fmap g ]
-          ≈-cong   {a} {b} {f1} {g1} f≈g = {!!}
+          ≈-cong   {a} {b} {f1} {g1} f≈g = refl-hom
           identity :  {x : Obj I} → A [ fmap ( id1 I x ) ≈  id1 A (fobj x) ]
-          identity = {!!}
+          identity {t0} = refl-hom
+          identity {t1} = refl-hom
+          identity {t2} = refl-hom
+          identity {t3} = 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}   = begin
+                    id1 A a
+                ≈↑⟨ idL ⟩
+                    A [ id1 A a  o id1 A a ]
+                ∎
+          distr1 {t1} {t1} {t1} {f1} {g1}   = sym idL
+          distr1 {t2} {t2} {t2} {f1} {g1}   = sym idL
+          distr1 {t3} {t3} {t3} {f1} {g1}   = sym idL
+          distr1 {t0} {t1} {t1} {f1} {g1}   = sym idL
+          distr1 {t0} {t1} {_} {f1} {g1}   = ?
           distr1 {a1} {b1} {c1} {f1} {g1}   = {!!}
 
 ---  Equalizer