Mercurial > hg > Members > kono > Proof > category

changeset 403:375edfefbf6a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
maybe CAT
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 20 Mar 2016 11:36:44 +0900
parents 9123f79c0642
children 07bea66e5ceb
files limit-to.agda maybeCat.agda
diffstat 2 files changed, 48 insertions(+), 47 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Thu Mar 17 11:26:22 2016 +0900
+++ b/limit-to.agda	Sun Mar 20 11:36:44 2016 +0900
@@ -1,7 +1,7 @@
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
 
-module limit-to { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
+module limit-to where
 
 open import cat-utility
 open import HomReasoning
@@ -33,47 +33,49 @@
    arrow-g :  Arrow
    nil :  Arrow
 
-record RawHom {c₁ ℓ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set  (c₁  ⊔ ℓ) where
+record RawHom { c₁ c₂ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set   c₂ where
    field
-       RawMap    : Arrow  {ℓ }
+       RawMap    : Arrow  { c₂ }
 
 open RawHom
 
-record Two-Hom { c₁  ℓ : Level }   (a : TwoObject { c₁}  ) (b : TwoObject  { c₁} ) : Set   (c₁  ⊔ ℓ)  where
+record Two-Hom { c₁  c₂ : Level }   (a : TwoObject { c₁}  ) (b : TwoObject  { c₁} ) : Set    c₂  where
    field
-      hom : Maybe ( RawHom { c₁}  {ℓ } a b )
+      hom : Maybe ( RawHom  {c₁} { c₂ } a b )
 
 open  Two-Hom 
 
-Two-id :  {c₁ ℓ : Level } -> (a : TwoObject {c₁} ) ->   Two-Hom {c₁} { ℓ} a a 
+Two-id :  { c₁ c₂ : Level } -> (a : TwoObject {c₁} ) ->   Two-Hom {c₁} { c₂}  a a 
 Two-id _  = record { hom = just ( record { RawMap = id-t0 } ) }
 
 -- arrow composition
 
-twocomp : {c₁ ℓ : Level } ->  { a b : TwoObject {c₁} } -> Arrow  {ℓ } -> Arrow  {ℓ } -> Maybe  ( RawHom a b )
+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 _ _ = nothing
 
-_×_ :  { c₁  ℓ : Level }  -> {A B C : TwoObject { c₁} } →  Two-Hom { c₁}  {ℓ}  B C →  Two-Hom { c₁}  {ℓ}  A B  →  Two-Hom { c₁}  {ℓ}  A C 
+_×_ :  { 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₁ ℓ : Level } ->  {a b : TwoObject  {c₁} } -> Rel (Maybe (RawHom  {c₁} {ℓ} a b  )) (ℓ ⊔ c₁)
+_==_ :  {c₁ c₂ : Level } ->  {a b : TwoObject  {c₁} } -> Rel (Maybe (RawHom  {c₁} {c₂} a b  )) c₂
 _==_    =   Eq ( _≡_  ) 
 
+open import maybeCat  
+
 
-TwoCat : { c₁ c₂ ℓ : Level  } ->  Category   c₁  (ℓ ⊔ c₁)  (ℓ ⊔ c₁)
+TwoCat : { c₁ c₂ ℓ : Level  } ->  Category   c₁  c₂  c₂
 TwoCat   {c₁}  {c₂} {ℓ} = record {
     Obj  = TwoObject  {c₁} ;
-    Hom = λ a b →   Two-Hom {c₁ } { ℓ}  a b   ; 
-    _o_ =  _×_  { c₁}  {ℓ} ;
+    Hom = λ a b →   Two-Hom {c₁ } { c₂}  a b   ; 
+    _o_ =  _×_  { c₁}  {c₂} ;
     _≈_ = λ a b →   hom a == hom b  ;
     Id  =  \{a} -> Two-id a ;
     isCategory  = record {
-            isEquivalence = record {refl = {!!} ; trans = {!!} ; 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} ;
@@ -92,10 +94,8 @@
         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}  =   {!!}
 
-open import maybeCat  
-
-indexFunctor :  {c₁ c₂ ℓ : Level} ( a b : Obj (MaybeCat A )) ( f g : Hom A a b ) ->  Functor (TwoCat {c₁} {c₂} {ℓ} ) (MaybeCat A )
-indexFunctor  {c₁} {c₂} {ℓ}  a b f g = record {
+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
        ; isFunctor = record {
@@ -109,7 +109,7 @@
           fobj :  Obj I -> Obj A
           fobj t0 = a
           fobj t1 = b
-          fmap1 :  {x y : Obj I } ->  (Arrow  {ℓ} ) -> Hom MA (fobj x) (fobj y)
+          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 )}
@@ -144,11 +144,11 @@
 
 open Limit
 
-lim-to-equ : 
+lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ->
       (lim : (I : Category c₁ c₂ ℓ) ( Γ : Functor I A ) → { a0 : Obj A } { u : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 u ) -- completeness
         →  {a b c : Obj A}      (f g : Hom A  a b ) 
         → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
-lim-to-equ  lim {a} {b} {c}  f g e fe=ge = record {
+lim-to-equ  {c₁} {c₂} {ℓ } A  lim {a} {b} {c}  f g e fe=ge = record {
         fe=ge =  fe=ge
         ; k = λ {d} h fh=gh → k {d} h fh=gh
         ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
--- a/maybeCat.agda	Thu Mar 17 11:26:22 2016 +0900
+++ b/maybeCat.agda	Sun Mar 20 11:36:44 2016 +0900
@@ -17,28 +17,42 @@
 
 open MaybeHom
 
-_×_ :  { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } ->  {a b c : Obj A } → MaybeHom A b c  →  MaybeHom A a b  →  MaybeHom A  a c 
-_×_  {x} {y} {z} {A} {a} {b} {c} f g with hom f | hom g
-_×_  {_} {_} {_} {A} {a} {b} {c} f g | nothing  | _  = record { hom =  nothing }
-_×_  {_} {_} {_} {A} {a} {b} {c} f g | _ | nothing   = record { hom =  nothing }
-_×_  {_} {_} {_} {A} {a} {b} {c} _ _ | (just f) |  (just g)  = record { hom =  just ( A [ f o  g ]  ) }
+_+_ :  { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } ->  {a b c : Obj A } → MaybeHom A b c  →  MaybeHom A a b  →  MaybeHom A  a c 
+_+_  {x} {y} {z} {A} {a} {b} {c} f g with hom f | hom g
+_+_  {_} {_} {_} {A} {a} {b} {c} f g | nothing  | _  = record { hom =  nothing }
+_+_  {_} {_} {_} {A} {a} {b} {c} f g | _ | nothing   = record { hom =  nothing }
+_+_  {_} {_} {_} {A} {a} {b} {c} _ _ | (just f) |  (just g)  = record { hom =  just ( A [ f o  g ]  ) }
 
 MaybeHomId  : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } (a  : Obj A ) -> MaybeHom A a a
 MaybeHomId   {_} {_} {_} {A} a  = record { hom = just ( id1 A a)  }
 
-_[_==_] : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A } ->  Rel (Maybe (Hom A a b)) (c₂ ⊔ ℓ) 
-_[_==_]  A =  Eq ( Category._≈_ A ) 
+_[_≡≡_] : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A } ->  Rel (Maybe (Hom A a b)) (c₂ ⊔ ℓ) 
+_[_≡≡_]  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
+
+*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
+
 
 
 MaybeCat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) -> Category   c₁ (ℓ ⊔ c₂)  (ℓ ⊔ c₂)
 MaybeCat { c₁} {c₂} {ℓ} ( A ) =   record {
     Obj  = Obj A  ;
     Hom = λ a b →   MaybeHom A  a b   ; 
-    _o_ =  _×_   ;
-    _≈_ = λ a b →    _[_==_] { c₁} {c₂} {ℓ} A  (hom a) (hom b)  ;
+    _o_ =  _+_   ;
+    _≈_ = λ a b →    _[_≡≡_] { c₁} {c₂} {ℓ} A  (hom a) (hom b)  ;
     Id  =  \{a} -> MaybeHomId a ;
     isCategory  = record {
-            isEquivalence = record {refl = *refl ; trans = *trans ; sym = *sym };
+            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} ;
@@ -46,31 +60,18 @@
        } 
    } where
         open ≈-Reasoning (A) 
-
-        *refl :   {a b : Obj A } -> {x : Maybe ( Hom A a b ) } → A [ x == x ]
-        *refl  {_} {_} {just x}  = just refl-hom
-        *refl  {_} {_} {nothing} = nothing
-
-        *sym : {a b : Obj A } -> {x y : Maybe ( Hom A a b ) }  → A [ x == y ] → A [ y == x ]
-        *sym (just x≈y) = just (sym x≈y)
-        *sym nothing    = nothing
-
-        *trans : {a b : Obj A } -> {x y z : Maybe ( Hom A a b ) }  → A [ x == y ] → A [ y == z ] → A [ x == z ]
-        *trans (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z)
-        *trans nothing    nothing    = nothing
-
-        identityL : { a b : Obj A } { f : MaybeHom A a b } ->  A [ hom (MaybeHomId b × f) == hom f ]
+        identityL : { a b : Obj A } { f : MaybeHom A a b } ->  A [ hom (MaybeHomId b + f) ≡≡ hom f ]
         identityL {a} {b} {f}  with hom f
         identityL {a} {b} {_} | nothing  = nothing
         identityL {a} {b} {_} | just f = just ( IsCategory.identityL ( Category.isCategory A )  {a} {b} {f}  )
 
-        identityR : { a b : Obj A } { f : MaybeHom A a b } ->  A [ hom (f × MaybeHomId a  ) == hom f ]
+        identityR : { a b : Obj A } { f : MaybeHom A a b } ->  A [ hom (f + MaybeHomId a  ) ≡≡ hom f ]
         identityR {a} {b} {f}  with hom f
         identityR {a} {b} {_} | nothing  = nothing
         identityR {a} {b} {_} | just f = just ( IsCategory.identityR ( Category.isCategory A )  {a} {b} {f}  )
 
         o-resp-≈  :  {a b c : Obj A} → {f g : MaybeHom A a b } → {h i : MaybeHom A  b c } → 
-                A [ hom f == hom g ] → A [ hom h == hom i ] → A [ hom (h × f) == hom (i × g) ]
+                A [ hom f ≡≡ hom g ] → A [ hom h ≡≡ hom i ] → A [ hom (h + f) ≡≡ hom (i + g) ]
         o-resp-≈  {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi with hom f | hom g  | hom h | hom i
         o-resp-≈  {a} {b} {c} {_} {_} {_} {_}  (just eq-fg)  (just eq-hi) | just f | just g | just h | just i =  
              just ( IsCategory.o-resp-≈ ( Category.isCategory A )  {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi )
@@ -80,7 +81,7 @@
 
 
         associative  :  {a b c d : Obj A} → {f : MaybeHom A c d } → {g : MaybeHom A b c } → {h : MaybeHom A a b } → 
-           A [ hom (f × (g × h)) == hom ((f × g) × h) ]
+           A [ hom (f + (g + h)) ≡≡ hom ((f + g) + h) ]
         associative  {_} {_} {_} {_} {f} {g} {h}  with hom f | hom g | hom h 
         associative  {_} {_} {_} {_} {f} {g} {h}  | nothing | _ | _ = nothing
         associative  {_} {_} {_} {_} {f} {g} {h}  | just _ | nothing | _ = nothing