Mercurial > hg > Members > kono > Proof > category

changeset 386:1e136aaad5cb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 14 Mar 2016 17:44:45 +0900
parents ff3803fc0c8a
children 2f59c2db9d98
files limit-to.agda
diffstat 1 files changed, 15 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Mon Mar 14 14:53:54 2016 +0900
+++ b/limit-to.agda	Mon Mar 14 17:44:45 2016 +0900
@@ -84,6 +84,8 @@
 twocomp :  {ℓ : Level } -> Maybe (Arrow {ℓ }) -> Maybe (Arrow {ℓ }) -> Maybe (Arrow {ℓ } )
 twocomp (just arrow-f) (just id-t0) = just arrow-f
 twocomp (just arrow-g) (just id-t0) = just arrow-g
+twocomp (just id-t1) (just arrow-f)  = just arrow-f
+twocomp (just id-t1) (just arrow-g)  = just arrow-g
 twocomp (just id-t0) (just id-t0) = just id-t0
 twocomp (just id-t1) (just id-t1) = just id-t1
 twocomp _ _ = nothing
@@ -133,11 +135,20 @@
         open  import  Relation.Binary.PropositionalEquality
         ≡-cong = Relation.Binary.PropositionalEquality.cong 
         identityL : {A B : TwoObject} {f : Two-Hom A B} →  Map ( Two-id B × f ) ≡ Map f
-        identityL {a} {b} {f} =   let open ≡-Reasoning in
+        identityL {a} {b} {f} with Map f
+        identityL {t0} {t0} {f} | nothing  = refl
+        identityL {t0} {t1} {f} | nothing  = refl
+        identityL {t1} {t0} {f} | nothing  = refl
+        identityL {t1} {t1} {f} | nothing  = refl
+        identityL {t1} {t1} {f} | just id-t1  = refl
+        identityL {t0} {t1} {f} | just arrow-f  = refl
+        identityL {t0} {t1} {f} | just arrow-g  = refl
+        identityL {t0} {t0} {f} | just id-t0  = refl
+        identityL {a} {b} {f} | just fa =   let open ≡-Reasoning in
               begin
-                {!!}
+                  RawMap (arrow2hom a b (twocomp (RawMap (hom (Two-id b))) (just fa)))
               ≡⟨ {!!} ⟩
-                {!!}
+                 just fa
               ∎
         identityR : {A B : TwoObject} {f : Two-Hom A B} →  Map ( f × Two-id A  ) ≡ Map f
         identityR {a} {b} {f} =   let open ≡-Reasoning in
@@ -185,7 +196,7 @@
           fmap {t1} {t1} x  | just id-t1 = id1 A b
           fmap {_} {_} x  | _ = {!!}
           identity :  {x : Obj I} → A [ fmap (id1 I  x) ≈ id1 A  (fobj x) ]
-          identity  = {!!}
+          identity    = {!!}
           distr : {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₁ ] ]
           distr {a₁} {b₁} {c} {f₁} {g₁}  = {!!}
           ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → I [ f ≈ g ] → A [ fmap f ≈ fmap g ]