Mercurial > hg > Members > kono > Proof > category

changeset 419:8919c162b894

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cong is a bit strange...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 24 Mar 2016 02:53:25 +0900
parents 7091104a8cb4
children 3e44951b9bdb
files limit-to.agda
diffstat 1 files changed, 27 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Thu Mar 24 02:07:45 2016 +0900
+++ b/limit-to.agda	Thu Mar 24 02:53:25 2016 +0900
@@ -342,8 +342,33 @@
           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 → {!!}
-          ≈-cong   {_} {_} {f1} {g1} f≈g = {!!}
+          ≈-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