---
--
--  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} (e : Hom A c a) (f g : Hom A a b)  : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
   field
      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

--
-- Flat Equational Definition of Equalizer
--
record Burroni { 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 Burroni

--
-- Some obvious conditions for k  (fe = ge) → ( fh = gh )
--

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

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

f1=gh : { a b c d : Obj A } {f g : Hom A a b } → { e : Hom A c a } → { h : Hom A d c } →
       (eq : A [ A [ f  o e ] ≈ A [ g  o e ] ] ) → A [ A [ f o A [ e o h ] ] ≈ A [ g o A [ e  o h ]  ] ]
f1=gh {a} {b} {c} {d} {f} {g} {e} {h} eq = let open ≈-Reasoning (A) in
             begin
                  f o ( e  o h )
             ≈⟨ assoc  ⟩
                  (f o  e ) o h
             ≈⟨ car eq  ⟩
                  (g o  e ) o h
             ≈↑⟨ assoc  ⟩
                  g o ( e  o h )
             ∎

--
--
--   An isomorphic element c' of c makes another equalizer
--
--           e eqa f g        f
--         c ----------> a ------->b
--        |^
--        ||
--    h   || h-1
--        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 {
      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'
             ∎
      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 ]
      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 
             ≈⟨ 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 [ 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
             ≈⟨ {!!} ⟩
                   j
             ∎



--
-- If we have two equalizers on c and c', there are isomorphic pair h, h'
--
--     h : c → c'  h' : c' → c
--     e' = h   o e
--     e  = h'  o e'


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' ]) )
      → Hom A c c'
c-iso-l  {c} {c'} eqa eqa' eff = {!!}

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' ]) )
      →  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
     --         c'----------> a ------->b               f e j = g e j
     --         ^                 g
     --         |k      h
     --         |                                        h =   e(eqaj) o k     jhek = jh (uniqueness)
     --         |
     --         c     j o (k (eqa ef ef) j ) = id c      h =   e(eqaj)
     --
     --                 h j e f = h j e g    →    h =  'j e f
     --                                           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' ]) )
      →  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-l eqa eqa' keqa o c-iso-r eqa eqa' keqa
              ≈⟨ {!!} ⟩
                 id1 A c'
              ∎


----
--
-- An equalizer satisfies Burroni equations
--
--    b4 is not yet done
----

lemma-equ1 : {a b c : Obj A} (f g : Hom A a b)  →
         ( eqa : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a } { fe=ge1 : A [ A [ f o e ] ≈ A [ g o e ] ] } → Equalizer A e f g ) 
              → Burroni A {c} f g
lemma-equ1  {a} {b} {c} f g eqa = record {
      α = λ f g →  equalizer (eqa f g ) ; -- Hom A c a
      γ = λ {a} {b} {c} {d} f g h → k (eqa f g ) {d} ( A [ h  o (equalizer ( 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-b2 ;
      b3 = lemma-b3 ;
      b4 = lemma-b4
 } 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-b3 : A [ A [ equalizer (eqa f f ) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ]
     lemma-b3 = let open ≈-Reasoning (A) in
             begin
                  equalizer (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 equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ] ≈ A [ g o A [ h o equalizer (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 equalizer (eqa (f o h) ( g o h )))
             ≈⟨ assoc ⟩
                   (f o h) o equalizer (eqa (f o h) ( g o h ))
             ≈⟨ fe=ge (eqa (A [ f o h ]) (A [ g o h ])) ⟩
                   (g o h) o equalizer (eqa (f o h) ( g o h ))
             ≈↑⟨ assoc ⟩
                   g o ( h o equalizer (eqa (f o h) ( g o h )))
             ∎
     lemma-b2 :  {d : Obj A} {h : Hom A d a} → A [
                      A [ equalizer (eqa f g) o k (eqa f g) (A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 {a} {b} {c} f g h) ]
                    ≈ A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ]
     lemma-b2 {d} {h} = let open ≈-Reasoning (A) in
             begin
                    equalizer (eqa f g) o k (eqa f g) (h o equalizer (eqa (f o h) (g o h))) (lemma-equ4 {a} {b} {c} f g h)
             ≈⟨ ek=h (eqa f g)  ⟩
                    h o equalizer (eqa (f o h ) ( g o h ))
             ∎

     -------             α(f,g)j id d                                   =                  α(f,g)j
     -------             α(f,g)j id d                                   =                  α(f,g)j
     -------             α(f,g)j α(fα(f,g)j,fα(f,g)j) δ(fα(f,g)j)       =                  α(f,g)j
     ------                    fα = gα
     -------             α(f,g)j α(fα(f,g)j,gα(f,g)j) δ(fα(f,g)j)       =                  α(f,g)j
     -------                    α(f,g) γ(f,g,α(f,g)j) δ(fα(f,g)j)       =                  α(f,g)j
     -------                           γ(f,g,α(f,g)j) δ(fα(f,g)j)       =                        j

     lemma-b4 : {d : Obj A} {j : Hom A d c} → A [
          A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o equalizer (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ g o A [ equalizer (eqa f g) o j ] ])) ])
                     (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ])) o
              k (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ f o A [ equalizer (eqa f g) o j ] ])) (id1 A d) (lemma-equ2 (A [ f o A [ equalizer (eqa f g) o j ] ])) ]
              ≈ j ]
     lemma-b4 {d} {j} = let open ≈-Reasoning (A) in
             begin
                     ( k (eqa f g) (( ( equalizer (eqa f g) o j ) o equalizer (eqa (( f o ( equalizer (eqa f g) o j ) )) (( g o ( equalizer (eqa f g) o j ) ))) ))
                            (lemma-equ4 {a} {b} {c} f g (( equalizer (eqa f g) o j ))) o
                       k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( equalizer (eqa f g) o j ) ))) )
             ≈⟨ {!!} ⟩
                    j
             ∎


-- end