---
--
--  Equalizer
--
--         e             f
--    c  --------> a ----------> b
--    ^        .     ---------->
--    |      .            g
--    |k   .                
--    |  . h              
--    d 
--
--                        Shinji KONO <kono@ie.u-ryukyu.ac.jp>
----

open import Category -- https://github.com/konn/category-agda                                                                                     
open import Level
module equalizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where

open import HomReasoning
open import cat-utility

record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (f g : Hom A a b)  : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
   field
      e : Hom A c a 
      ef=eg : A [ A [ f  o  e ] ≈ A [ g  o e ] ]
      k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
      ke=h : {d : Obj A}  → ∀ {h : Hom A d a} →  (eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] ) →  A [ A [ e  o k {d} h eq ] ≈ h ]
      uniqueness : {d : Obj A} →  ∀ {h : Hom A d a} →  (eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] ) →  {k' : Hom A d c } → A [ A [ e  o k' ] ≈ h ] →
                       A [ k {d} h eq  ≈ k' ]
   equalizer : Hom A c a
   equalizer = e

record EqEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
   field
      α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) →  Hom A c a
      γ : {a b d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →  Hom A c d
      δ : {a b c : Obj A } → (f : Hom A a b) → Hom A a c 
      b1 : A [ A [ f  o α {a} {b} {a}  f g ] ≈ A [ g  o α f g ] ]
      b2 :  {d : Obj A } → {h : Hom A d a } → A [ A [ ( α f g) o (γ f g h) ] ≈ A [ h  o α (A [ f o h ]) (A [ g o h ]) ] ]
      b3 :  A [ A [ α f f o δ {a} {b} {a} f ] ≈ id1 A a ]
      -- b4 :  {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o  k ] ) ≈ k ]
      b4 :  {d : Obj A } {k : Hom A d c} → A [ A [ γ f g ( A [ α f g o  k ] ) o δ (A [ f o A [ α f g o  k ] ] ) ] ≈ {!!} ]
   --  A [ α f g o β f g h ] ≈ h
--   β : { d e a b : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) →  (h : Hom A d a ) → Hom A a d
--   β {d} {e} {a} {b} f g h =  A [ γ {a} {b} {d} f g h o δ (A [ f o h ]) ] 

open Equalizer
open EqEqualizer

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
lemma-equ1  A {a} {b} {c} f g eqa = record {
      α = λ f g →  e (eqa f g ) ; -- Hom A c  a
      γ = λ {a} {b} {d} f g h → ( k (eqa f g ) ( A [ h  o (e ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {d} f g h ) ) ;  -- Hom A c d
      δ =  λ {a} f → k (eqa f f) (id1 A a)  (lemma-equ2 f); -- Hom A a c
      b1 = ef=eg (eqa f g) ;
      b2 = lemma-equ5 ;
      b3 = lemma-equ3 ;
      b4 = {!!} 
 } where
     lemma-equ2 : {a b : Obj A} (f : Hom A a b)  → A [ A [ f o id1 A a ]  ≈ A [ f o id1 A a ] ]
     lemma-equ2 f =   let open ≈-Reasoning (A) in refl-hom
     lemma-equ3 : A [ A [ e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ]
     lemma-equ3 = let open ≈-Reasoning (A) in
             begin  
                  e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f)
             ≈⟨ ke=h (eqa f f ) (lemma-equ2 f) ⟩
                  id1 A a
             ∎
     lemma-equ4 :  {a b d : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → 
                      A [ A [ f o A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ] ] ≈ A [ g o A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ] ] ]
     lemma-equ4 {a} {b} {d} f g h  = let open ≈-Reasoning (A) in
             begin
                   f o ( h o e (eqa (f o h) ( g o h )))
             ≈⟨ assoc ⟩
                   (f o h) o e (eqa (f o h) ( g o h ))
             ≈⟨ ef=eg (eqa (A [ f o h ]) (A [ g o h ])) ⟩
                   (g o h) o e (eqa (f o h) ( g o h ))
             ≈↑⟨ assoc ⟩
                   g o ( h o e (eqa (f o h) ( g o h )))
             ∎
     lemma-equ5 :  {d : Obj A} {h : Hom A d a} → A [ 
                      A [ e (eqa f g) o k (eqa f g) (A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 f g h) ]
                    ≈ A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ] ]
     lemma-equ5 {d} {h} = let open ≈-Reasoning (A) in
             begin
                    e (eqa f g) o k (eqa f g) (h o e (eqa (f o h) (g o h))) (lemma-equ4 f g h) 
             ≈⟨ ke=h (eqa f g) (lemma-equ4 f g h) ⟩
                    h o e (eqa (f o h ) ( g o h ))
             ∎