Mercurial > hg > Members > kono > Proof > category

changeset 231:1dc1c697145f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reverse-e
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 07 Sep 2013 23:14:05 +0900
parents 1ef8c70c7054
children b0fe61882014
files equalizer.agda
diffstat 1 files changed, 21 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Sat Sep 07 18:56:46 2013 +0900
+++ b/equalizer.agda	Sat Sep 07 23:14:05 2013 +0900
@@ -49,7 +49,6 @@
    β {d} {e} {a} {b} f g h =  A [ γ {a} {b} {c} f g h o δ (A [ f o h ]) ]
 
 open Equalizer
-
 open Burroni
 
 --
@@ -435,12 +434,28 @@
 --           e eqa f g        f
 --         c ----------> a ------->b
 --           <---------
---    
-reverse-e : {a b c : Obj A} (f g : Hom A a b)  →
+--             k (eff) id1a
+--                                (e eqa f g)  o k (eff) id1 A a = id1 A a
+--
+--      eqa (f (e eqa f g) ) (g (e eqa f g) )
+--      e (eqa (f (e eqa f g) ) (g (e eqa f g) ) ) = k (eff) id1 a
+--
+--      (e α) o k α (id1 A c)  = id1 A c
+--      c       a           c
+--      ((k (eff) id1a ))  o k α e = id1 A c
+
+
+reverse-e : {a b c : Obj A} (f g : Hom A a b)  → (h i : Hom A c b ) →
          ( eqa : {a b c : Obj A} → (f g : Hom A a b)  → Equalizer A {c} f g ) → 
-             A [ A [  k (eqa (A [ f o e (eqa f g) ]) (A [ g o e (eqa f g) ]) ) (id1 A a) 
-                  (f1=g1 (fe=ge (eqa f g) ) (id1 A a) ) o e (eqa f g ) ] ≈ id1 A c ]
-reverse-e {a} {b} {c} f g eqa = ?
+             A [ 
+   A [ e (eqa ( A [ f  o (e (eqa f g)) ] )  (A [ g  o (e (eqa f g )) ] ))  o k (eqa ( A [ f  o (e (eqa f g)) ] )  (A [ g  o (e (eqa f g )) ] ))  (id1 A c) {!!} ]
+             ≈ id1 A c ]
+reverse-e {a} {b} {c} f g h i eqa =  let open ≈-Reasoning (A) in
+             begin
+                  e (eqa ( A [ f  o (e (eqa f g)) ] )  (A [ g  o (e (eqa f g )) ] ))  o k (eqa ( A [ f  o (e (eqa f g)) ] )  (A [ g  o (e (eqa f g )) ] ))  (id1 A c) {!!}
+             ≈⟨  ek=h   (eqa ( A [ f  o (e (eqa f g)) ] )  (A [ g  o (e (eqa f g )) ] ))   ⟩
+                  id1 A c
+             ∎
 
 ----
 --