# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1378287917 -32400
# Node ID 5d96be63053f08cc7e58dbc85992b85b9b8e6e7d
# Parent  2ae029454fb6a6013459bae7a904359e8378905d
eefg

diff -r 2ae029454fb6 -r 5d96be63053f equalizer.agda
--- a/equalizer.agda	Wed Sep 04 17:36:32 2013 +0900
+++ b/equalizer.agda	Wed Sep 04 18:45:17 2013 +0900
@@ -231,6 +231,64 @@
         A [ A [ e eqa o k' ] ≈ j ] → A [ k eqa j (fj=gj j eq) ≈ k' ]
       uniqueness1 = uniqueness eqa
       
+eefeg : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) 
+           → Equalizer A {c} (A [ f o e eqa ])  (A [ g o e eqa ] ) 
+eefeg {a} {b} {c} {d} {f} {g} eqa =  record {
+      e = id1 A c ; -- i  ; -- A [ h-1 o e eqa ]  ;       -- Hom A a d
+      ef=eg = ef=eg1 ;
+      k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ;
+      ek=h = ek=h1 ; 
+      uniqueness = uniqueness1
+   } where
+      i = id1 A c
+      h = e eqa
+      fhj=ghj :  {d' : Obj A } → (j : Hom A d' c ) → 
+           A [ A [ A [ f o h ] o j ] ≈ A [ A [ g o h ] o j ] ] →
+           A [ A [ f o A [ h o j ] ] ≈ A [ g o A [ h o j ] ] ] 
+      fhj=ghj j eq' = let open ≈-Reasoning (A) in
+             begin
+                  f o ( h o j  )
+             ≈⟨ assoc  ⟩
+                  (f o h ) o j  
+             ≈⟨ eq' ⟩
+                  (g o h ) o j  
+             ≈↑⟨ assoc ⟩
+                  g o ( h  o j )
+             ∎
+      ef=eg1 :  A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ]
+      ef=eg1 = let open ≈-Reasoning (A) in 
+             begin
+                   ( f o h ) o i
+             ≈⟨ car ( ef=eg eqa ) ⟩
+                   ( g o h ) o i
+             ∎
+      ek=h1 :  {d' : Obj A} {k' : Hom A d' c} {eq' : A [ A [ A [ f o h ] o k' ] ≈ A [ A [ g o h ] o k' ] ]} →
+                A [ A [ i o k eqa (A [ h o k' ]) (fhj=ghj k' eq') ] ≈ k' ]
+      ek=h1 {d'} {k'} {eq'} = let open ≈-Reasoning (A) in
+             begin
+                   i o k eqa (h o k' ) (fhj=ghj k' eq') --    h-1 (h o i ) o k eqa (h o k' ) = h-1 (h o k')
+             ≈⟨ idL  ⟩
+                   k eqa (e eqa o k' ) (fhj=ghj k' eq')
+             ≈⟨ uniqueness eqa refl-hom ⟩
+                   k'
+             ∎
+      uniqueness1 :  {d' : Obj A} {h' : Hom A d' c} {eq' : A [ A [ A [ f o h ] o h' ] ≈ A [ A [ g o h ] o h' ] ]} {k' : Hom A d' c} →
+                A [ A [ i o k' ] ≈ h' ] → A [ k eqa (A [ h o h' ]) (fhj=ghj h' eq') ≈ k' ]
+      uniqueness1 {d'} {h'} {eq'} {k'} ik=h = let open ≈-Reasoning (A) in
+             begin
+                   k eqa ( e eqa o h')  (fhj=ghj h' eq')
+             ≈⟨ uniqueness eqa ( begin
+                    e eqa o k'
+                ≈↑⟨ cdr idL ⟩
+                    e eqa o (id1 A c o k' )
+                ≈⟨ cdr ik=h ⟩
+                    e eqa o h' 
+             ∎ ) ⟩
+                   k'
+             ∎
+
+      
+
 
 lemma-equ1 :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b c : Obj A} (f g : Hom A a b)  → 
          ( {a b c : Obj A} → (f g : Hom A a b)  → Equalizer A {c} f g ) → EqEqualizer A {c} f g