Mercurial > hg > Members > kono > Proof > category

changeset 404:07bea66e5ceb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 20 Mar 2016 12:32:13 +0900
parents 375edfefbf6a
children 4c34c0e3c4bb
files limit-to.agda maybeCat.agda
diffstat 2 files changed, 41 insertions(+), 32 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Sun Mar 20 11:36:44 2016 +0900
+++ b/limit-to.agda	Sun Mar 20 12:32:13 2016 +0900
@@ -33,36 +33,46 @@
    arrow-g :  Arrow
    nil :  Arrow
 
-record RawHom { c₁ c₂ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set   c₂ where
-   field
-       RawMap    : Arrow  { c₂ }
-
-open RawHom
-
 record Two-Hom { c₁  c₂ : Level }   (a : TwoObject { c₁}  ) (b : TwoObject  { c₁} ) : Set    c₂  where
    field
-      hom : Maybe ( RawHom  {c₁} { c₂ } a b )
+      hom  : Maybe ( Arrow  { c₂ } )
 
 open  Two-Hom 
 
 Two-id :  { c₁ c₂ : Level } -> (a : TwoObject {c₁} ) ->   Two-Hom {c₁} { c₂}  a a 
-Two-id _  = record { hom = just ( record { RawMap = id-t0 } ) }
+Two-id _  = record { hom = just  id-t0  }
 
 -- arrow composition
 
-twocomp : {c₁  c₂ : Level } ->  { a b : TwoObject {c₁} } -> Arrow  { c₂ } -> Arrow  { c₂ } -> Maybe  ( RawHom a b )
-twocomp id-t0 f = just ( record { RawMap = f } )
-twocomp f id-t0 = just ( record { RawMap = f } )
+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
 twocomp _ _ = nothing
 
 _×_ :  { c₁  c₂ : Level }  -> {A B C : TwoObject { c₁} } →  Two-Hom { c₁}  {c₂}  B C →  Two-Hom { c₁}  {c₂}  A B  →  Two-Hom { c₁}  {c₂}  A C 
 _×_   { c₁} {ℓ} {a} {b} {c} f g with  hom f |  hom g 
 _×_   { c₁} {ℓ} {a} {b} {c} f g | nothing   | _ = record { hom = nothing }
 _×_   { c₁} {ℓ} {a} {b} {c} f g | _   | nothing  = record { hom = nothing }
-_×_   { c₁} {ℓ} {a} {b} {c} _ _ | just f  | just g   = record { hom = twocomp  { c₁} {ℓ} {a} {c} (RawMap f) (RawMap g ) }
+_×_   { 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
 
-_==_ :  {c₁ c₂ : Level } ->  {a b : TwoObject  {c₁} } -> Rel (Maybe (RawHom  {c₁} {c₂} a b  )) c₂
-_==_    =   Eq ( _≡_  ) 
+==-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  
 
@@ -75,14 +85,13 @@
     _≈_ = λ a b →   hom a == hom b  ;
     Id  =  \{a} -> Two-id a ;
     isCategory  = record {
-            isEquivalence =  record {refl = *refl  {_} {_} {_} {{!!}}; trans = *trans  {_} {_} {_} {{!!}}; sym = *sym  {_} {_} {_} {{!!}}};
+            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}
        } 
    } where
-        open  import  Relation.Binary.PropositionalEquality
         ≡-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}  = {!!}
@@ -106,27 +115,27 @@
       } where
           I = TwoCat  {c₁} {c₂} {ℓ}
           MA = MaybeCat A
+          open ≈-Reasoning (MA)
           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} {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} ( RawMap f )
+          fmap {x} {y} _  | just f = fmap1 {x} {y}  f 
           open ≈-Reasoning (A) 
-          identity :  {x : Obj I} → MA [ fmap (id1 I  x) ≈ id1 MA  (fobj x) ]
+          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} → 
-               MA [ fmap (I [ g₁ o f₁ ]) ≈ MA [ fmap g₁ o fmap f₁ ] ]
+          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 ] → MA [ fmap f ≈ fmap g ]
+          ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → _[_≈_] I f g → {!!}
           ≈-cong   {_} {_} {f1} {g1} f≈g = {!!}
 
 
--- a/maybeCat.agda	Sun Mar 20 11:36:44 2016 +0900
+++ b/maybeCat.agda	Sun Mar 20 12:32:13 2016 +0900
@@ -30,17 +30,17 @@
 _[_≡≡_]  A =  Eq ( Category._≈_ A ) 
 
 
-*refl :   { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } ->  {a b : Obj A } -> {x : Maybe ( Hom A a b ) } → A [ x ≡≡ x ]
-*refl  {_} {_} {_} {A} {_} {_} {just x}  = just refl-hom where  open ≈-Reasoning (A)
-*refl  {_} {_} {_} {A} {_} {_} {nothing} = nothing
+≡≡-refl :   { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } ->  {a b : Obj A } -> {x : Maybe ( Hom A a b ) } → A [ x ≡≡ x ]
+≡≡-refl  {_} {_} {_} {A} {_} {_} {just x}  = just refl-hom where  open ≈-Reasoning (A)
+≡≡-refl  {_} {_} {_} {A} {_} {_} {nothing} = nothing
 
-*sym :  { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } -> {a b : Obj A } -> {x y : Maybe ( Hom A a b ) }  → A [ x ≡≡ y ] → A [ y ≡≡ x ]
-*sym {_} {_} {_} {A} (just x≈y) = just (sym x≈y)  where  open ≈-Reasoning (A)
-*sym {_} {_} {_} {A} nothing    = nothing
+≡≡-sym :  { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } -> {a b : Obj A } -> {x y : Maybe ( Hom A a b ) }  → A [ x ≡≡ y ] → A [ y ≡≡ x ]
+≡≡-sym {_} {_} {_} {A} (just x≈y) = just (sym x≈y)  where  open ≈-Reasoning (A)
+≡≡-sym {_} {_} {_} {A} nothing    = nothing
 
-*trans :  { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } -> {a b : Obj A } -> {x y z : Maybe ( Hom A a b ) }  → A [ x ≡≡ y ] → A [ y ≡≡ z ] → A [ x ≡≡ z ]
-*trans {_} {_} {_} {A} (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z)  where  open ≈-Reasoning (A)
-*trans {_} {_} {_} {A} nothing    nothing    = nothing
+≡≡-trans :  { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } -> {a b : Obj A } -> {x y z : Maybe ( Hom A a b ) }  → A [ x ≡≡ y ] → A [ y ≡≡ z ] → A [ x ≡≡ z ]
+≡≡-trans {_} {_} {_} {A} (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z)  where  open ≈-Reasoning (A)
+≡≡-trans {_} {_} {_} {A} nothing    nothing    = nothing
 
 
 
@@ -52,7 +52,7 @@
     _≈_ = λ a b →    _[_≡≡_] { c₁} {c₂} {ℓ} A  (hom a) (hom b)  ;
     Id  =  \{a} -> MaybeHomId a ;
     isCategory  = record {
-            isEquivalence = record {refl = *refl  {_} {_} {_} {A}; trans = *trans  {_} {_} {_} {A}; sym = *sym  {_} {_} {_} {A}};
+            isEquivalence = record {refl = ≡≡-refl  {_} {_} {_} {A}; trans = ≡≡-trans  {_} {_} {_} {A}; sym = ≡≡-sym  {_} {_} {_} {A}};
             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} ;