Mercurial > hg > Members > kono > Proof > category

changeset 423:b5519e954b57

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TwoCat / indexFunctor all done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 24 Mar 2016 13:44:27 +0900
parents 3a4a99a8edbe
children 4329525f5085
files limit-to.agda maybeCat.agda
diffstat 2 files changed, 17 insertions(+), 29 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Thu Mar 24 13:11:50 2016 +0900
+++ b/limit-to.agda	Thu Mar 24 13:44:27 2016 +0900
@@ -288,7 +288,6 @@
                 ∎
 
 
-
 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
@@ -301,7 +300,6 @@
       } where
           I = TwoCat  {c₁} {c₂} {ℓ}
           MA = MaybeCat A
-          open ≈-Reasoning (MA)
           fobj :  Obj I -> Obj A
           fobj t0 = a
           fobj t1 = b
@@ -312,6 +310,18 @@
           fmap  {t0} {t1} h | just arrow-f = record { hom = just f }
           fmap  {t0} {t1} h | just arrow-g = record { hom = just g }
           fmap  {_} {_} h | _  = record { hom = nothing }
+          ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → I [ f ≈ g ]  → MA [ fmap f ≈ fmap g ]
+          ≈-cong   {a} {b} {f1} {g1} f≈g with hom f1 | hom g1
+          ≈-cong   {t0} {t0} {f1} {g1} nothing | nothing | nothing = nothing
+          ≈-cong   {t0} {t1} {f1} {g1} nothing | nothing | nothing = nothing
+          ≈-cong   {t1} {t0} {f1} {g1} nothing | nothing | nothing = nothing
+          ≈-cong   {t1} {t1} {f1} {g1} nothing | nothing | nothing = nothing
+          ≈-cong   {t0} {t0} {f1} {g1} (just refl) | just id-t0 | just id-t0 = let open  ≡≡-Reasoning A in  ≡≡-refl 
+          ≈-cong   {t1} {t1} {f1} {g1} (just refl) | just id-t1 | just id-t1 = let open  ≡≡-Reasoning A in  ≡≡-refl 
+          ≈-cong   {t0} {t1} {f1} {g1} (just refl) | just arrow-f | just arrow-f = let open  ≡≡-Reasoning A in  ≡≡-refl 
+          ≈-cong   {t0} {t1} {f1} {g1} (just refl) | just arrow-g | just arrow-g = let open  ≡≡-Reasoning A in  ≡≡-refl 
+          ≈-cong   {t1} {t0} {f1} {g1} (just refl) | just inv-f | just inv-f = let open  ≡≡-Reasoning A in  ≡≡-refl 
+          open ≈-Reasoning (MA)
           identity :  {x : Obj I} → MA [ fmap ( id1 I x ) ≈  id1 MA (fobj x) ]
           identity {t0}  =  refl-hom
           identity {t1}  =  refl-hom
@@ -358,33 +368,6 @@
           distr1 {t1} {t0} {t1} {_} {_} | (just arrow-f) |  (just _) = nothing
           distr1 {t1} {t0} {t1} {_} {_} | (just arrow-g) |  (just _) = nothing
 
-          ≈-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 with hom f1 | hom  g1
-          ≈-cong   {t0} {t0} {f1} {g1} f≈g | nothing | nothing = nothing
-          ≈-cong   {t0} {t1} {f1} {g1} f≈g | nothing | nothing = nothing
-          ≈-cong   {t1} {t0} {f1} {g1} f≈g | nothing | nothing = nothing
-          ≈-cong   {t1} {t1} {f1} {g1} f≈g | nothing | nothing = nothing
-          ≈-cong   {t0} {t0} {f1} {g1} f≈g | nothing | just id-t0 =  {!!}
-          ≈-cong   {t0} {t1} {f1} {g1} f≈g | nothing | just arrow-f = {!!}
-          ≈-cong   {t0} {t1} {f1} {g1} f≈g | nothing | just arrow-g = {!!}
-          ≈-cong   {t1} {t0} {f1} {g1} f≈g | nothing | just inv-f = nothing
-          ≈-cong   {t1} {t1} {f1} {g1} f≈g | nothing | just id-t1 = {!!}
-          ≈-cong   {t0} {t0} {f1} {g1} f≈g | just id-t0 | nothing  = {!!}
-          ≈-cong   {t1} {t1} {f1} {g1} f≈g | just id-t1 | nothing  = {!!}
-          ≈-cong   {t0} {t1} {f1} {g1} f≈g | just arrow-f | nothing  = {!!}
-          ≈-cong   {t0} {t1} {f1} {g1} f≈g | just arrow-g | nothing  = {!!}
-          ≈-cong   {t1} {t0} {f1} {g1} f≈g | just inv-f | nothing  = nothing
-          ≈-cong   {t0} {t0} {f1} {g1} f≈g | just id-t0 | just id-t0 = refl-hom
-          ≈-cong   {t1} {t1} {f1} {g1} f≈g | just id-t1 | just id-t1 = refl-hom
-          ≈-cong   {t0} {t1} {f1} {g1} f≈g | just arrow-f | just arrow-f = refl-hom
-          ≈-cong   {t0} {t1} {f1} {g1} f≈g | just arrow-g | just arrow-g = refl-hom
-          ≈-cong   {t0} {t1} {f1} {g1} f≈g | just arrow-g | just arrow-f = {!!}
-          ≈-cong   {t1} {t0} {f1} {g1} f≈g | just inv-f | just inv-f = refl-hom
-          ≈-cong   {t0} {t1} {f1} {g1} f≈g | just arrow-f | just arrow-g = begin
-                     {!!}
-                 ≈⟨ {!!} ⟩
-                     {!!}
-                 ∎
 
 
 ---  Equalizer
--- a/maybeCat.agda	Thu Mar 24 13:11:50 2016 +0900
+++ b/maybeCat.agda	Thu Mar 24 13:44:27 2016 +0900
@@ -6,6 +6,7 @@
 open import cat-utility
 open import HomReasoning
 open import Relation.Binary 
+open import Relation.Binary.Core
 open import Data.Maybe
 
 open Functor
@@ -48,6 +49,10 @@
         ≡≡-trans (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z)  where  open ≈-Reasoning (A)
         ≡≡-trans nothing    nothing    = nothing
 
+        ≡≡-cong :  ∀{ a b c d }   -> ∀ {x y :  Maybe (Hom A a b )} →
+                (f : Maybe (Hom A a b ) -> Maybe (Hom A c d ) )  ->  x  ≡  y  →  A [ f x ≡≡ f y ]
+        ≡≡-cong  {a} {b } {c} {d} {nothing} {nothing} f refl  = ≡≡-refl
+        ≡≡-cong  {a} {b } {c} {d} {just x} {just .x} f refl  = ≡≡-refl
 
         data _IsRelatedTo_  {a b : Obj A}  (x y : (Maybe (Hom A a b ))) :
                              Set  (ℓ ⊔ c₂)  where