---
--
--  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 
      fe=ge : 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
      ek=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 c d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →  Hom A d c
      δ : {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 (γ {a} {b} {c} 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 [ γ {a} {b} {c} {d} f g ( A [ α {a} {b} {c} f g o k ] ) o δ (A [ f o A [ α f g o  k ] ] ) ] ≈ 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 d c
   β {d} {e} {a} {b} f g h =  A [ γ {a} {b} {c} f g h o δ (A [ f o h ]) ] 

open Equalizer
open EqEqualizer


f1=g1 : { a b : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → A [ A [ f o id1 A a ] ≈ A [ g o id1 A a ]  ]
f1=g1 eq = let open ≈-Reasoning (A) in (resp refl-hom eq )


equalizer-eq-k  : { a b : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → ( eqa : Equalizer A {a} f g) → 
      A [ e eqa ≈ id1 A a ] →
      A [ k eqa (id1 A a) (f1=g1 eq) ≈ id1 A a ] 
equalizer-eq-k {a} {b} {f} {g} eq eqa e=1 =  let open ≈-Reasoning (A) in
             begin
                   k eqa (id1 A a) (f1=g1 eq)     
             ≈⟨ uniqueness eqa ( begin
                    e eqa o id1 A a
                 ≈⟨ idR ⟩
                    e eqa 
                 ≈⟨ e=1 ⟩
                    id1 A a
             ∎ )⟩
                   id1 A a
             ∎

--           e eqa f g        f
--         c ----------> a ------->b
--         ^ ---> d ---> 
--         |  i      h
--        j|    k' (d' → d)
--         |    k  (d' → a)
--         d'            

equalizer+h : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) (i : Hom A c d ) → (h : Hom A d a ) → (h-1 : Hom A a d ) 
           → A [ A [ h  o i ]  ≈ e eqa ] → A [ A [ h-1  o h ]  ≈ id1 A d ]
           → Equalizer A {c} (A [ f o h ])  (A [ g o h ] ) 
equalizer+h  {a} {b} {c} {d} {f} {g} eqa i h h-1 eq h-1-id =  record {
      e = i  ; -- A [ h-1 o e eqa ]  ;       -- Hom A a d
      fe=ge = fe=ge1 ;
      k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ;
      ek=h = ek=h1 ; 
      uniqueness = uniqueness1
   } where
      fhj=ghj :  {d' : Obj A } → (j : Hom A d' d ) → 
           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 )
             ∎
      fe=ge1 :  A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ]
      fe=ge1 = let open ≈-Reasoning (A) in 
             begin
                   ( f o h ) o i
             ≈↑⟨ assoc  ⟩
                   f o (h  o i )
             ≈⟨ cdr eq ⟩
                   f o (e eqa)
             ≈⟨ fe=ge eqa ⟩
                   g o (e eqa)
             ≈↑⟨ cdr eq ⟩
                   g o (h  o i )
             ≈⟨ assoc ⟩
                   ( g o h ) o i
             ∎
      ek=h1 :  {d' : Obj A} {k' : Hom A d' d} {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  ⟩
                   (id1 A d ) o ( i o k eqa (h o k' ) (fhj=ghj k' eq')) 
             ≈↑⟨ car h-1-id ⟩
                   ( h-1 o h ) o ( i o k eqa (h o k' ) (fhj=ghj k' eq')) 
             ≈↑⟨ assoc  ⟩
                    h-1 o ( h  o ( i o k eqa (h o k' ) (fhj=ghj k' eq')) )
             ≈⟨ cdr assoc  ⟩
                    h-1 o ( (h  o  i ) o k eqa (h o k' ) (fhj=ghj k' eq'))
             ≈⟨ cdr (car eq ) ⟩
                    h-1 o ( (e eqa) o k eqa (h o k' ) (fhj=ghj k' eq'))
             ≈⟨ cdr (ek=h eqa)  ⟩
                    h-1 o ( h  o k' )
             ≈⟨ assoc  ⟩
                    ( h-1 o  h ) o k' 
             ≈⟨ car h-1-id ⟩
                    id1 A d o k' 
             ≈⟨ idL ⟩
                   k'
             ∎
      uniqueness1 :  {d' : Obj A} {h' : Hom A d' d} {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 (A [ h o h' ])  (fhj=ghj h' eq')
             ≈⟨ uniqueness eqa ( begin
                    e eqa o k'
                ≈↑⟨ car eq  ⟩
                    (h o i ) o k'
                ≈↑⟨ assoc   ⟩
                    h o (i  o k')
                ≈⟨ cdr ik=h ⟩
                     h o h' 
             ∎ ) ⟩
                   k'
             ∎

h+equalizer : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) (h : Hom A b d ) 
           → (h-1 : Hom A d b ) → A [ A [ h-1  o h ]  ≈ id1 A b ]
           → Equalizer A {c} (A [ h o f ])  (A [ h o g ] ) 
h+equalizer  {a} {b} {c} {d} {f} {g} eqa h h-1 h-1-id =  record {
      e = e eqa  ;   
      fe=ge = fe=ge1 ; 
      k = λ j eq' → k eqa j (fj=gj j eq') ;
      ek=h = ek=h1 ; 
      uniqueness = uniqueness1
   }  where
      fj=gj : {e : Obj A} → (j : Hom A e a ) →  A [ A [ A [ h o f ] o  j ] ≈ A [ A [ h o g ] o j ] ] →  A [ A [ f o j ] ≈ A [ g o j ] ]
      fj=gj j eq  = let open ≈-Reasoning (A) in
             begin
                f o j
             ≈↑⟨ idL ⟩
                id1 A b  o ( f o j )
             ≈↑⟨ car h-1-id  ⟩
                (h-1 o h )  o ( f o j )
             ≈↑⟨ assoc  ⟩
                h-1 o (h  o ( f o j ))
             ≈⟨ cdr assoc  ⟩
                h-1 o ((h  o  f) o j )
             ≈⟨ cdr eq ⟩
                h-1 o ((h  o  g) o j )
             ≈↑⟨ cdr assoc  ⟩
                h-1 o (h  o ( g o j ))
             ≈⟨ assoc ⟩
                (h-1 o h)  o ( g o j )
             ≈⟨ car h-1-id  ⟩
                id1 A b  o ( g o j )
             ≈⟨ idL ⟩
                g o j
             ∎
      fe=ge1 :  A [ A [ A [ h o f ] o e eqa ] ≈ A [ A [ h o g ] o e eqa ] ]
      fe=ge1 =  let open ≈-Reasoning (A) in
             begin
                ( h o f ) o e eqa
             ≈↑⟨ assoc  ⟩
                h o (f  o e eqa )
             ≈⟨ cdr (fe=ge eqa)  ⟩
                h o (g  o e eqa )
             ≈⟨ assoc ⟩
                ( h o g ) o e eqa 
             ∎
      ek=h1 :   {d₁ : Obj A} {j : Hom A d₁ a} {eq : A [ A [ A [ h o f ] o j ] ≈ A [ A [ h o g ] o j ] ]} →
        A [ A [ e eqa o k eqa j (fj=gj j eq) ] ≈ j ]
      ek=h1 {d₁} {j} {eq}  = ek=h eqa
      uniqueness1 : {d₁ : Obj A} {j : Hom A d₁ a} {eq : A [ A [ A [ h o f ] o j ] ≈ A [ A [ h o g ] o j ] ]} {k' : Hom A d₁ c} →
        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
      fe=ge = fe=ge1 ;
      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 )
             ∎
      fe=ge1 :  A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ]
      fe=ge1 = let open ≈-Reasoning (A) in 
             begin
                   ( f o h ) o i
             ≈⟨ car ( fe=ge 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'
             ∎

-- Equalizer is unique up to iso

equalizer-iso : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
      → Hom A c c'   --- != id1 A c
equalizer-iso  {c} eqa eqa' = k eqa' (e eqa) (fe=ge eqa)

--
--        
--           e eqa f g        f
--         c ----------> a ------->b
--
equalizer-iso-eq : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
      → A [ A [ equalizer-iso eqa eqa' o   equalizer-iso eqa' eqa ] ≈  id1 A c' ]
equalizer-iso-eq {c} {c'} {f} {g} eqa eqa' =  let open ≈-Reasoning (A) in
             begin
                  k eqa' (e eqa) (fe=ge eqa)  o  k eqa (e eqa' ) (fe=ge eqa' )
             ≈⟨ {!!} ⟩
                 id1 A c'
             ∎

-- ke = e' k'e' = e  → k k' = 1 , k' k = 1
--     ke  = e'
--     k'ke  = k'e' = e   kk' = 1

--     x e = e -> x = id?

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} {c} {d} f g h → k (eqa f g ) {d} ( A [ h  o (e ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {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 = fe=ge (eqa f g) ;
      b2 = lemma-equ5 ;
      b3 = lemma-equ3 ;
      b4 = lemma-equ6 
 } where
     --
     --           e eqa f g        f
     --         c ----------> a ------->b
     --         ^                  g     
     --         |                           
     --         |k₁  = e eqa (f o (e (eqa f g))) (g o (e (eqa f g))))
     --         |        
     --         d
     --         
     --         
     --               e  o id1 ≈  e  →   k e  ≈ id

     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)
             ≈⟨ ek=h (eqa f f )  ⟩
                  id1 A a
             ∎
     lemma-equ4 :  {a b c 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} {c} {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 ))
             ≈⟨ fe=ge (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 {a} {b} {c} 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 {a} {b} {c} f g h) 
             ≈⟨ ek=h (eqa f g)  ⟩
                    h o e (eqa (f o h ) ( g o h ))
             ∎
     lemma-equ6 : {d : Obj A} {k₁ : Hom A d c} → A [ 
          A [ k (eqa f g) (A [ A [ e (eqa f g) o k₁ ] o e (eqa (A [ f o A [ e (eqa f g) o k₁ ] ]) (A [ g o A [ e (eqa f g) o k₁ ] ])) ])
                     (lemma-equ4 {a} {b} {c} f g (A [ e (eqa f g) o k₁ ])) o 
              k (eqa (A [ f o A [ e (eqa f g) o k₁ ] ]) (A [ f o A [ e (eqa f g) o k₁ ] ])) (id1 A d) (lemma-equ2 (A [ f o A [ e (eqa f g) o k₁ ] ])) ]
              ≈ k₁ ]
     lemma-equ6 {d} {k₁} = let open ≈-Reasoning (A) in 
             begin
                     ( k (eqa f g) (( ( e (eqa f g) o k₁ ) o e (eqa (( f o ( e (eqa f g) o k₁ ) )) (( g o ( e (eqa f g) o k₁ ) ))) ))
                            (lemma-equ4 {a} {b} {c} f g (( e (eqa f g) o k₁ ))) o
                       k (eqa (( f o ( e (eqa f g) o k₁ ) )) (( f o ( e (eqa f g) o k₁ ) ))) (id1 A d) (lemma-equ2 (( f o ( e (eqa f g) o k₁ ) ))) )
             ≈⟨ car ( uniqueness (eqa f g) ( begin
                   e (eqa f g) o  k₁ 
                ≈⟨ {!!} ⟩
                   (e (eqa f g) o k₁) o e (eqa (f o e (eqa f g) o k₁) (g o e (eqa f g) o k₁))
             ∎ ))  ⟩
                    k₁ o  k (eqa (( f o ( e (eqa f g) o k₁ ) )) (( f o ( e (eqa f g) o k₁ ) ))) (id1 A d) (lemma-equ2 (( f o ( e (eqa f g) o k₁ ) ))) 
             ≈⟨ cdr ( uniqueness (eqa (( f o ( e (eqa f g) o k₁ ) )) (( f o ( e (eqa f g) o k₁ ) ))) ( begin
                  e (eqa (f o e (eqa f g) o k₁) (f o e (eqa f g) o k₁)) o id1 A d
                ≈⟨ {!!} ⟩
                 id1 A d
             ∎ ))  ⟩
                    k₁  o  id1 A d
             ≈⟨ idR ⟩
                    k₁
             ∎