Mercurial > hg > Members > kono > Proof > category

changeset 402:9123f79c0642

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 Thu, 17 Mar 2016 11:26:22 +0900
parents e4c10d6375f6
children 375edfefbf6a
files limit-to.agda maybeCat.agda
diffstat 2 files changed, 40 insertions(+), 37 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Thu Mar 17 10:58:01 2016 +0900
+++ b/limit-to.agda	Thu Mar 17 11:26:22 2016 +0900
@@ -73,7 +73,7 @@
     _≈_ = λ a b →   hom a == hom b  ;
     Id  =  \{a} -> Two-id a ;
     isCategory  = record {
-            isEquivalence = record {refl = ? ; trans = ? ; sym = ? };
+            isEquivalence = record {refl = {!!} ; trans = {!!} ; 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} ;
@@ -83,18 +83,18 @@
         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}  = ?
+        identityL {a} {b} {f}  = {!!}
         identityR : {A B : TwoObject} {f : Two-Hom A B} →  hom ( f × Two-id A  ) == hom f
-        identityR {a} {b} {f}  = ?
+        identityR {a} {b} {f}  = {!!}
         o-resp-≈ : {A B C : TwoObject} {f g :  Two-Hom A B} {h i : Two-Hom B C} →
             hom f == hom g → hom h == hom i → hom ( h × f ) == hom ( i × g )
-        o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = ?
+        o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = {!!}
         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}  =   ?
+        associative {_} {_} {_} {_} {f} {g} {h}  =   {!!}
 
-open import maybeCat  {c₁} {c₂} {ℓ} {A }
+open import maybeCat  
 
-indexFunctor :  {c₁ c₂ ℓ : Level} ( a b : Obj MaybeCat ) ( f g : Hom A a b ) ->  Functor (TwoCat {c₁} {c₂} {ℓ} ) (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 {
          FObj = λ a → fobj a
        ; FMap = λ f → fmap f
@@ -105,28 +105,29 @@
        }
       } where
           I = TwoCat  {c₁} {c₂} {ℓ}
+          MA = MaybeCat A
           fobj :  Obj I -> Obj A
           fobj t0 = a
           fobj t1 = b
-          fmap1 :  {x y : Obj I } ->  (Arrow  {ℓ} ) -> Hom MaybeCat (fobj x) (fobj y)
+          fmap1 :  {x y : Obj I } ->  (Arrow  {ℓ} ) -> 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 )}
           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 MaybeCat (fobj x) (fobj y)
+          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 )
           open ≈-Reasoning (A) 
-          identity :  {x : Obj I} → MaybeCat [ fmap (id1 I  x) ≈ id1 MaybeCat  (fobj x) ]
-          identity {t0}  =  ?
-          identity {t1}  =  ?
+          identity :  {x : Obj I} → MA [ fmap (id1 I  x) ≈ id1 MA  (fobj x) ]
+          identity {t0}  =  {!!}
+          identity {t1}  =  {!!}
           distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → 
-               MaybeCat [ fmap (I [ g₁ o f₁ ]) ≈ MaybeCat [ fmap g₁ o fmap f₁ ] ]
-          distr1 {a1} {b1} {c} {f1} {g1}   = ?
-          ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → I [ f ≈ g ] → MaybeCat [ fmap f ≈ fmap g ]
-          ≈-cong   {_} {_} {f1} {g1} f≈g = ?
+               MA [ fmap (I [ g₁ o f₁ ]) ≈ MA [ fmap g₁ o fmap f₁ ] ]
+          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   {_} {_} {f1} {g1} f≈g = {!!}
 
 
 ---  Equalizer
@@ -154,7 +155,7 @@
         ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
      } where
          I = TwoCat {c₁} {c₂} {ℓ }
-         Γ = ?
+         Γ = {!!}
          nmap :  (x : Obj I) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A I d) x) (FObj Γ x)
          nmap x d h = {!!}
          commute1 : {x y : Obj I}  {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) ->  A [ A [ f  o  h ] ≈ A [ g  o h ] ] 
--- a/maybeCat.agda	Thu Mar 17 10:58:01 2016 +0900
+++ b/maybeCat.agda	Thu Mar 17 11:26:22 2016 +0900
@@ -1,7 +1,7 @@
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
 
-module maybeCat { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
+module maybeCat where
 
 open import cat-utility
 open import HomReasoning
@@ -17,25 +17,25 @@
 
 open MaybeHom
 
-_×_ :    {a b c : Obj A } → MaybeHom A b c  →  MaybeHom A a b  →  MaybeHom A  a c 
-_×_   {a} {b} {c} f g with hom f | hom g
-_×_   {a} {b} {c} f g | nothing  | _  = record { hom =  nothing }
-_×_   {a} {b} {c} f g | _ | nothing   = record { hom =  nothing }
-_×_   {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  : (a  : Obj A ) -> MaybeHom A a a
-MaybeHomId  a  = record { hom = just ( id1 A a)  }
+MaybeHomId  : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } (a  : Obj A ) -> MaybeHom A a a
+MaybeHomId   {_} {_} {_} {A} a  = record { hom = just ( id1 A a)  }
 
-_==_ :  {a b : Obj A } ->  Rel (Maybe (Hom A a b)) (c₂ ⊔ ℓ) 
-_==_   {a} {b}  =   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 ) 
 
 
-MaybeCat : Category   c₁ (ℓ ⊔ c₂)  (ℓ ⊔ c₂)
-MaybeCat =   record {
+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 →    _==_ (hom a) (hom b)  ;
+    _≈_ = λ a b →    _[_==_] { c₁} {c₂} {ℓ} A  (hom a) (hom b)  ;
     Id  =  \{a} -> MaybeHomId a ;
     isCategory  = record {
             isEquivalence = record {refl = *refl ; trans = *trans ; sym = *sym };
@@ -47,29 +47,30 @@
    } where
         open ≈-Reasoning (A) 
 
-        *refl :   {a b : Obj A } -> {x : Maybe ( Hom A a b ) } → x == x
+        *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 ) }  → x == y → y == x
+        *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 ) }  → x == y → y == z → x == z
+        *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 } ->  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 } ->  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 } → hom f == hom g → hom h == hom i → hom (h × f) == hom (i × g)
+        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) ]
         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 )
@@ -78,7 +79,8 @@
         o-resp-≈  {a} {b} {c} {f} {g} {h} {i} nothing nothing | nothing | nothing | nothing | nothing = nothing
 
 
-        associative  :  {a b c d : Obj A} → {f : MaybeHom A c d } → {g : MaybeHom A b c } → {h : MaybeHom A a b } → hom (f × (g × h)) == hom ((f × g) × h)
+        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) ]
         associative  {_} {_} {_} {_} {f} {g} {h}  with hom f | hom g | hom h 
         associative  {_} {_} {_} {_} {f} {g} {h}  | nothing | _ | _ = nothing
         associative  {_} {_} {_} {_} {f} {g} {h}  | just _ | nothing | _ = nothing