# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1378580205 -32400
# Node ID c02287d3d2dcb96cb838d93bb3c43b6c38b57f29
# Parent  4bba19bc71be8d0d172921858c918249ce8fde07
equalizer iso done.

diff -r 4bba19bc71be -r c02287d3d2dc equalizer.agda
--- a/equalizer.agda	Sun Sep 08 01:37:24 2013 +0900
+++ b/equalizer.agda	Sun Sep 08 03:56:45 2013 +0900
@@ -85,56 +85,58 @@
 --        v|
 --         c'
 
-equalizer+iso : {a b c c' : Obj A } {f g : Hom A a b } {e : Hom A c a } { e' : Hom A c' a }
-                 ( fe=ge' : A [ A [ f o e' ] ≈ A [ g o e' ] ] )
-                ( eqa : Equalizer A e f g ) → (h-1 : Hom A c' c ) → (h : Hom A c c' ) →
-                A [ A [ e o h-1 ]  ≈ e' ] → A [ A [ e'  o h ]  ≈ e ]
-           → Equalizer A e' f g
-equalizer+iso  {a} {b} {c} {c'} {f} {g} {e} {e'} fe=ge' eqa h-1 h e→e' e'→e  =  record {
+equalizer+iso : {a b c c' : Obj A } {f g : Hom A a b } {e : Hom A c a } 
+                (h-1 : Hom A c' c ) → (h : Hom A c c' ) →
+                A [ A [ h o h-1 ]  ≈ id1 A c' ] → A [ A [ h-1  o h ]  ≈ id1 A c ] →
+                 ( fe=ge' : A [ A [ f o A [ e o h-1 ] ] ≈ A [ g o A [  e  o h-1 ] ] ] )
+                ( eqa : Equalizer A e f g ) 
+           → Equalizer A (A [ e  o h-1  ] ) f g
+equalizer+iso  {a} {b} {c} {c'} {f} {g} {e} h-1 h  hh-1=1 h-1h=1  fe=ge' eqa =  record {
       fe=ge = fe=ge1 ;
       k = λ j eq → A [ h o k eqa j eq ] ;
       ek=h = ek=h1 ;
       uniqueness = uniqueness1
   } where
-      fe=ge1 :  A [ A [ f o e' ]  ≈ A [ g o e' ] ]
-      fe=ge1 = let open ≈-Reasoning (A) in
-             begin
-                  f o e'
-             ≈↑⟨ cdr e→e' ⟩
-                  f o ( e o h-1 )
-             ≈⟨ assoc  ⟩
-                  (f o  e ) o h-1 
-             ≈⟨ car (fe=ge eqa) ⟩
-                  (g o  e ) o h-1 
-             ≈↑⟨ assoc ⟩
-                  g o ( e o h-1 )
-             ≈⟨ cdr e→e' ⟩
-                  g o e'
-             ∎
+      fe=ge1 :  A [ A [ f o  A [ e  o h-1  ]  ]  ≈ A [ g o  A [ e  o h-1  ]  ] ]
+      fe=ge1 = fe=ge'
       ek=h1 :   {d : Obj A} {j : Hom A d a} {eq : A [ A [ f o j ] ≈ A [ g o j ] ]} →
-                A [ A [ e' o A [ h o k eqa j eq ] ] ≈ j ]
+                A [ A [  A [ e  o h-1  ]  o A [ h o k eqa j eq ] ] ≈ j ]
       ek=h1 {d} {j} {eq} =  let open ≈-Reasoning (A) in
              begin
-                   e' o ( h o k eqa j eq )
-             ≈⟨ assoc ⟩
-                  ( e' o h)  o k eqa j eq 
-             ≈⟨ car e'→e ⟩
-                  e  o k eqa j eq 
+                   ( e  o h-1 )  o ( h o k eqa j eq )
+             ≈↑⟨ assoc ⟩
+                    e o ( h-1  o ( h  o k eqa j eq  ) )
+             ≈⟨ cdr assoc ⟩
+                    e o (( h-1  o  h)  o k eqa j eq  ) 
+             ≈⟨ cdr (car h-1h=1 )  ⟩
+                    e o (id1 A c  o k eqa j eq  ) 
+             ≈⟨ cdr idL  ⟩
+                    e o  k eqa j eq  
              ≈⟨ ek=h eqa ⟩
                    j
              ∎
       uniqueness1 : {d : Obj A} {h' : Hom A d a} {eq : A [ A [ f o h' ] ≈ A [ g o h' ] ]} {j : Hom A d c'} →
-                A [ A [ e' o j ] ≈ h' ] →
+                A [ A [  A [ e  o h-1 ]  o j ] ≈ h' ] →
                 A [ A [ h o k eqa h' eq ] ≈ j ]
       uniqueness1 {d} {h'} {eq} {j} ej=h  =  let open ≈-Reasoning (A) in
              begin
                    h o k eqa h' eq
-             ≈⟨ {!!} ⟩
+             ≈⟨ cdr (uniqueness eqa ( begin
+                    e o ( h-1 o j  )
+                 ≈⟨ assoc ⟩
+                   (e o  h-1 ) o j  
+                 ≈⟨ ej=h ⟩
+                    h'
+             ∎ )) ⟩
+                   h o  ( h-1 o j )
+             ≈⟨ assoc  ⟩
+                   (h o   h-1 ) o j 
+             ≈⟨ car hh-1=1  ⟩
+                   id1 A c' o j 
+             ≈⟨ idL ⟩
                    j
              ∎
 
-
-
 --
 -- If we have two equalizers on c and c', there are isomorphic pair h, h'
 --
@@ -145,17 +147,16 @@
 
 c-iso-l : { c c' a b : Obj A } {f g : Hom A a b } →  {e : Hom A c a } { e' : Hom A c' a }
        ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
-      →  ( keqa : Equalizer A (k eqa' e {!!} ) (A [ f o e' ])  (A [ g o e' ]) )
+      →  ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ])  (A [ g o e' ]) )
       → Hom A c c'
-c-iso-l  {c} {c'} eqa eqa' eff = {!!}
+c-iso-l  {c} {c'} eqa eqa' keqa = equalizer keqa
 
 c-iso-r : { c c' a b : Obj A } {f g : Hom A a b } {e : Hom A c a } {e' : Hom A c' a} → ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
-      →  ( keqa : Equalizer A (k eqa' e {!!} ) (A [ f o e' ])  (A [ g o e' ]) )
+      →  ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ])  (A [ g o e' ]) )
       →  Hom A c' c
 c-iso-r  {c} {c'} eqa eqa' keqa = k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )
 
-
-     --             e(eqa')       f
+     --               e'          f
      --         c'----------> a ------->b               f e j = g e j
      --         ^                 g
      --         |k      h
@@ -167,15 +168,49 @@
      --                                           h =   j e f   -> j = j'
      --
 
-c-iso : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
-      →  ( keqa : Equalizer A (k eqa' e {!!} ) (A [ f o e' ])  (A [ g o e' ]) )
+c-iso→ : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
+      →  ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ])  (A [ g o e' ]) )
       →  A [ A [ c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ]  ≈ id1 A c' ]
-c-iso {c} {c'} {a} {b} {f} {g} eqa eqa' keqa = let open ≈-Reasoning (A) in begin
+c-iso→ {c} {c'} {a} {b} {f} {g} eqa eqa' keqa = let open ≈-Reasoning (A) in begin
                  c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa
-              ≈⟨ {!!} ⟩
+              ≈⟨⟩
+                 equalizer keqa  o  k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )
+              ≈⟨ ek=h keqa ⟩
                  id1 A c'
               ∎
 
+c-iso← : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
+      →  ( keqa :  Equalizer A (k eqa' e (fe=ge eqa )) (A [ f o e' ])  (A [ g o e' ]) )
+      →  ( keqa' : Equalizer A (k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )) (A [ f o e ])   (A [ g o e ]) )
+      →  { e'->e : A [ e'  ≈  A [ e  o equalizer keqa' ] ] }
+      →  A [ A [ c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa ]  ≈ id1 A c ]
+c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa' {e'->e} = let open ≈-Reasoning (A) in begin
+                 c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa
+              ≈⟨⟩
+                 k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) o k eqa' e (fe=ge eqa )
+              ≈⟨⟩
+                 equalizer keqa'  o k eqa' e (fe=ge eqa )
+              ≈⟨ cdr ( begin
+                     k eqa' e (fe=ge eqa )
+                   ≈⟨ uniqueness eqa' ( begin
+                       e' o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c))
+                   ≈⟨ car e'->e ⟩
+                        ( e  o equalizer keqa' ) o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c))
+                   ≈↑⟨ assoc ⟩
+                         e  o ( equalizer keqa'  o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c)))
+                   ≈⟨ cdr ( ek=h keqa' ) ⟩
+                         e  o id1 A c
+                   ≈⟨ idR ⟩
+                       e
+                   ∎ )⟩
+                     k keqa' (id1 A c) ( f1=g1 (fe=ge eqa) (id1 A c) )
+              ∎ )⟩
+                 equalizer keqa'  o k keqa' (id1 A c) ( f1=g1 (fe=ge eqa) (id1 A c) )
+              ≈⟨ ek=h keqa' ⟩
+                 id1 A c
+              ∎
+
+
 
 ----
 --