---
--
--  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

-- in 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


--
-- Burroni's 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) (e : Hom A c a) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
   field
      α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) →  (e : Hom A c a ) → 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 } → (e : Hom A c a ) → (f : Hom A a b) → Hom A a c
      cong-α : {a b c :  Obj A } → { e : Hom A c a }
          → {f g g' : Hom A a b } →  A [ g ≈ g' ] → A [ α f g e ≈ α f g' e ]
      cong-γ : {a _ c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } →  A [ h ≈ h' ]
         → A [ γ {a} {b} {c} {d} f g h ≈ γ f g h' ]
      cong-δ : {a b c : Obj A } → {e : Hom A c a} → {f f' : Hom A a b} → A [ f ≈ f' ] →  A [ δ e f ≈ δ e f' ]
      b1 : A [ A [ f  o α {a} {b} {c}  f g e ] ≈ A [ g  o α {a} {b} {c} f g e ] ]
      b2 :  {d : Obj A } → {h : Hom A d a } → A [ A [ ( α {a} {b} {c} f g e ) o (γ {a} {b} {c} f g h) ] ≈ A [ h  o α (A [ f o h ]) (A [ g o h ]) (id1 A d) ] ]
      b3 : {a b d : Obj A} → (f : Hom A a b ) → {h : Hom A d a } → A [ A [ α {a} {b} {d} f f h o δ {a} {b} {d} h 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 e o k ] ) o ( δ {d} {b} {d} (id1 A d) (A [ f o A [ α {a} {b} {c} f g e o  k ] ] )  )] ≈ k ]
   --  A [ α f g o β f g h ] ≈ h
   β : { d a b : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) →  (h : Hom A d a ) → Hom A d c
   β {d} {a} {b} f g h =  A [ γ {a} {b} {c} f g h o δ {d} {b} {d} (id1 A d) (A [ f o h ]) ]


open Equalizer
open IsEqualizer
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 )
             ∎

-------------------------------
-- 
-- Every equalizer is monic
--
--     e i = e j → i = j
--
--           e eqa f g        f
--         c ---------→ a ------→b
--        ^^
--        ||
--       i||j
--        ||
--         d

monoic : { c a b d : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A f g) 
      →  { i j : Hom A d (equalizer-c eqa) }
      →  A [ A [ equalizer eqa o i ]  ≈  A [ equalizer eqa o j ] ] →  A [ i  ≈ j  ]
monoic {c} {a} {b} {d} {f} {g} eqa {i} {j} ei=ej = let open ≈-Reasoning (A) in begin
                 i
              ≈↑⟨ uniqueness (isEqualizer eqa) ( begin
                   equalizer eqa  o i
              ≈⟨ ei=ej ⟩
                   equalizer eqa  o j
              ∎ )⟩
                 k (isEqualizer eqa) (equalizer eqa o j) ( f1=gh (fe=ge (isEqualizer eqa) ) )
              ≈⟨ uniqueness (isEqualizer eqa) ( begin
                   equalizer eqa o j
              ≈⟨⟩
                   equalizer eqa o j
              ∎ )⟩
                 j
              ∎ 

--------------------------------
--
--
--   Isomorphic arrows from c' to c makes another equalizer
--
--           e eqa f g        f
--         c ---------→ a ------→b
--        |^
--        ||
--    h   || h-1
--        v|
--         c'

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

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 : IsEqualizer A e f g) → ( eqa' :  IsEqualizer A e' f g )
      → Hom A c c'         
c-iso-l  {c} {c'} {a} {b} {f} {g} {e} eqa eqa' = k eqa' e ( fe=ge eqa )

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 : IsEqualizer A e f g) → ( eqa' :  IsEqualizer A e' f g )
      → Hom A c' c         
c-iso-r  {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' = k eqa e' ( fe=ge eqa' )

c-iso-lr : { c c' a b : Obj A } {f g : Hom A a b } →  {e : Hom A c a } { e' : Hom A c' a }
       ( eqa : IsEqualizer A e f g) → ( eqa' :  IsEqualizer A e' f g ) →
  A [ A [ c-iso-l eqa eqa' o c-iso-r eqa eqa' ]  ≈ id1 A c' ]
c-iso-lr  {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' =  let open ≈-Reasoning (A) in begin
                  c-iso-l eqa eqa' o c-iso-r eqa eqa'
              ≈⟨⟩
                  k eqa' e ( fe=ge eqa )  o  k eqa e' ( fe=ge eqa' )
              ≈↑⟨ uniqueness eqa' ( begin
                  e' o ( k eqa' e (fe=ge eqa) o k eqa e' (fe=ge eqa') )
              ≈⟨ assoc  ⟩
                  ( e' o  k eqa' e (fe=ge eqa) ) o k eqa e' (fe=ge eqa') 
              ≈⟨ car (ek=h eqa') ⟩
                  e o k eqa e' (fe=ge eqa') 
              ≈⟨ ek=h eqa ⟩
                  e'
              ∎ )⟩
                 k eqa' e' ( fe=ge eqa' )
              ≈⟨ uniqueness eqa' ( begin
                   e' o id c'
              ≈⟨ idR ⟩
                   e'
              ∎ )⟩
                 id c'
              ∎

-- c-iso-rl is obvious from the symmetry



--------------------------------
----
--
-- Existence of equalizer satisfies Burroni equations
--
----

lemma-equ1 : {a b c : Obj A} (f g : Hom A a b)  → (e : Hom A c a ) →
         ( eqa : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a }  → IsEqualizer A e f g ) 
              → Burroni A {c} {a} {b} f g e
lemma-equ1  {a} {b} {c} f g e eqa  = record {
      α = λ {a} {b} {c}  f g e  →  equalizer1 (eqa {a} {b} {c} f g {e} ) ; -- Hom A c a
      γ = λ {a} {b} {c} {d} f g h → k (eqa {a} {b} {c} f g ) {d} ( A [ h  o (equalizer1 ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] ) 
                            (lemma-equ4 {a} {b} {c} {d} f g h ) ;  -- Hom A c d
      δ =  λ {a} {b} {c} e f → k (eqa {a} {b} {c} f f {e} ) {a} (id1 A a)  (f1=f1 f); -- Hom A a c
      cong-α = λ {a b c e f g g'} eq → cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq ;
      cong-γ = λ {a} {_} {c} {d} {f} {g} {h} {h'} eq → cong-γ1 {a}  {c} {d} {f} {g} {h} {h'} eq  ;
      cong-δ = λ {a b c e f f'} f=f' → cong-δ1 {a} {b} {c} {e} {f} {f'} f=f'  ;
      b1 = fe=ge (eqa {a} {b} {c} f g {e}) ;
      b2 = λ {d} {h} → lemma-b2 {d} {h};
      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-b3 : {a b d : Obj A} (f : Hom A a b ) { h : Hom A d a } → A [ A [ equalizer1 (eqa f f ) o k (eqa f f) (id1 A a) (f1=f1 f) ] ≈ id1 A a  ]
     lemma-b3 {a} {b} {d} f {h} = let open ≈-Reasoning (A) in
             begin
                  equalizer1 (eqa f f) o k (eqa f f) (id a) (f1=f1 f)
             ≈⟨ ek=h (eqa f f )  ⟩
                  id 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 equalizer1 (eqa (A [ f o h ]) (A [ g o h ])) ] ] ≈ A [ g o A [ h o equalizer1 (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 equalizer1 (eqa (f o h) ( g o h )))
             ≈⟨ assoc ⟩
                   (f o h) o equalizer1 (eqa (f o h) ( g o h ))
             ≈⟨ fe=ge (eqa (A [ f o h ]) (A [ g o h ])) ⟩
                   (g o h) o equalizer1 (eqa (f o h) ( g o h ))
             ≈↑⟨ assoc ⟩
                   g o ( h o equalizer1 (eqa (f o h) ( g o h )))
             ∎
     cong-α1 : {a b c :  Obj A } → { e : Hom A c a }
          → {f g g' : Hom A a b } →  A [ g ≈ g' ] → A [ equalizer1 (eqa {a} {b} {c} f g {e} )≈ equalizer1 (eqa {a} {b} {c} f g' {e} ) ] 
     cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq = let open ≈-Reasoning (A) in refl-hom 
     cong-γ1 :  {a c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } →  A [ h ≈ h' ] →  { e : Hom A c a} →
                     A [  k (eqa f g {e} ) {d} ( A [ h  o (equalizer1 ( eqa (A [ f  o  h  ] ) (A [ g o h  ] ) {id1 A d} )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) 
                       ≈  k (eqa f g {e} ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f  o  h' ] ) (A [ g o h' ] ) {id1 A d} )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )  ]
     cong-γ1 {a} {c} {d} {f} {g} {h} {h'} h=h' {e} = let open ≈-Reasoning (A) in begin
                 k (eqa f g ) {d} ( A [ h  o (equalizer1 ( eqa (A [ f  o  h  ] ) (A [ g o h  ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h )
             ≈⟨ uniqueness (eqa f g) ( begin
                 e o k (eqa f g ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f  o  h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )
             ≈⟨ ek=h (eqa f g ) ⟩
                 h' o (equalizer1 ( eqa (A [ f  o  h' ] ) (A [ g o h' ] )))
             ≈↑⟨ car h=h'  ⟩
                 h o (equalizer1 ( eqa (A [ f  o  h' ] ) (A [ g o h' ] )))
             ∎ )⟩    
                 k (eqa f g ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f  o  h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )
             ∎
     cong-δ1 : {a b c : Obj A} {e : Hom A c a } {f f' : Hom A a b} → A [ f ≈ f' ] →  A [ k (eqa {a} {b} {c} f f {e} ) (id1 A a)  (f1=f1 f)  ≈ 
                                                                            k (eqa {a} {b} {c} f' f' {e} ) (id1 A a)  (f1=f1 f') ]
     cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' =  let open ≈-Reasoning (A) in
             begin
                 k (eqa {a} {b} {c} f  f  {e} ) (id a)  (f1=f1 f) 
             ≈⟨  uniqueness (eqa f f) ( begin
                 e o k (eqa {a} {b} {c} f' f' {e} ) (id a)  (f1=f1 f') 
             ≈⟨ ek=h (eqa {a} {b} {c} f' f' {e} ) ⟩
                 id a
             ∎ )⟩
                 k (eqa {a} {b} {c} f' f' {e} ) (id a)  (f1=f1 f') 
             ∎

     lemma-b2 :  {d : Obj A} {h : Hom A d a} → A [
                      A [ equalizer1 (eqa f g) o k (eqa f g) (A [ h o equalizer1 (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 {a} {b} {c} f g h) ]
                    ≈ A [ h o equalizer1 (eqa (A [ f o h ]) (A [ g o h ])) ] ]
     lemma-b2 {d} {h} = let open ≈-Reasoning (A) in
             begin
                    equalizer1 (eqa f g) o k (eqa f g) (h o equalizer1 (eqa (f o h) (g o h))) (lemma-equ4 {a} {b} {c} f g h)
             ≈⟨ ek=h (eqa f g)  ⟩
                    h o equalizer1 (eqa (f o h ) ( g o h ))
             ∎

     lemma-b4 : {d : Obj A} {j : Hom A d c} → A [
              A [ k (eqa f g) (A [ A [ equalizer1 (eqa f g) o j ] o 
                              equalizer1 (eqa (A [ f o A [ equalizer1 (eqa f g {e}) o j ] ]) (A [ g o A [ equalizer1 (eqa f g {e} ) o j ] ])) ])
                     (lemma-equ4 {a} {b} {c} f g (A [ equalizer1 (eqa f g) o j ])) 
                 o k (eqa (A [ f o A [ equalizer1 (eqa f g) o j ] ]) (A [ f o A [ equalizer1 (eqa f g) o j ] ])) 
                     (id1 A d) (f1=f1 (A [ f o A [ equalizer1 (eqa f g) o j ] ])) ]
              ≈ j ]
     lemma-b4 {d} {j} = let open ≈-Reasoning (A) in
             begin
                ( k (eqa f g) (( ( equalizer1 (eqa f g) o j ) o equalizer1 (eqa (( f o ( equalizer1 (eqa f g {e}) o j ) )) (( g o ( equalizer1 (eqa f g {e}) o j ) ))) ))
                            (lemma-equ4 {a} {b} {c} f g (( equalizer1 (eqa f g) o j ))) o
                   k (eqa (( f o ( equalizer1 (eqa f g) o j ) )) (( f o ( equalizer1 (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer1 (eqa f g) o j ) ))) )
             ≈⟨ car ((uniqueness (eqa f g) ( begin
                         equalizer1 (eqa f g) o j 
                ≈↑⟨ idR  ⟩
                         (equalizer1 (eqa f g) o j )  o id d
                ≈⟨⟩         -- here we decide e (fej) (gej)' is id d
                        ((equalizer1 (eqa f g) o j) o equalizer1 (eqa (f o equalizer1 (eqa f g {e}) o j) (g o equalizer1 (eqa f g {e}) o j)))
             ∎ ))) ⟩
                    j o k (eqa (( f o ( equalizer1 (eqa f g) o j ) )) (( f o ( equalizer1 (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer1 (eqa f g) o j ) ))) 
             ≈⟨ cdr ((uniqueness (eqa (( f o ( equalizer1 (eqa f g) o j ) )) (( f o ( equalizer1 (eqa f g) o j ) ))) ( begin
                     equalizer1 (eqa (f o equalizer1 (eqa f g {e} ) o j) (f o equalizer1 (eqa f g {e}) o j))  o id d
                ≈⟨ idR ⟩
                     equalizer1 (eqa (f o equalizer1 (eqa f g {e}) o j) (f o equalizer1 (eqa f g {e}) o j))  
                ≈⟨⟩         -- here we decide e (fej) (fej)' is id d
                    id d
             ∎ ))) ⟩
                    j o id d
                ≈⟨ idR ⟩
                    j
             ∎ 

--------------------------------
--
-- Bourroni equations gives an Equalizer
--

lemma-equ2 : {a b c : Obj A} (f g : Hom A a b)  (e : Hom A c a )
         → ( bur : Burroni A {c} {a} {b} f g e ) → IsEqualizer A {c} {a} {b} (α bur f g e) f g 
lemma-equ2 {a} {b} {c} f g e bur = record {
      fe=ge = fe=ge1 ;  
      k = k1 ;
      ek=h = λ {d} {h} {eq} → ek=h1 {d} {h} {eq} ;
      uniqueness  = λ {d} {h} {eq} {k'} ek=h → uniqueness1  {d} {h} {eq} {k'} ek=h
   } where
      k1 :  {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
      k1 {d} h fh=gh = β bur {d} {a} {b} f g h
      fe=ge1 : A [ A [ f o (α bur f g e) ] ≈ A [ g o (α bur f g e) ] ]
      fe=ge1 = b1 bur
      ek=h1 : {d : Obj A}  → ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] } →  A [ A [ (α bur f g e)  o k1 {d} h eq ] ≈ h ]
      ek=h1 {d} {h} {eq} =  let open ≈-Reasoning (A) in
             begin
                 α bur f g e o k1 h eq 
             ≈⟨⟩
                 α bur f g e o ( γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id d) (f o h) )
             ≈⟨ assoc ⟩
                 ( α bur f g e o  γ bur {a} {b} {c} f g h ) o δ bur {d} {b} {d} (id d) (f o h) 
             ≈⟨ car (b2 bur) ⟩
                  ( h o ( α bur ( f o h ) ( g o h ) (id d))) o δ bur {d} {b} {d} (id d) (f o h) 
             ≈↑⟨ assoc ⟩
                   h o ((( α bur ( f o h ) ( g o h ) (id d) )) o δ bur {d} {b} {d} (id d) (f o h)  )
             ≈↑⟨ cdr ( car ( cong-α bur eq)) ⟩
                   h o ((( α bur ( f o h ) ( f o h ) (id d)))o δ bur {d} {b} {d} (id d) (f o h)  )
             ≈⟨ cdr (b3 bur {d} {b} {d} (f  o h) {id d} ) ⟩
                   h o id d
             ≈⟨ idR ⟩
                 h 
             ∎
      uniqueness1 : {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 [ (α bur f g e) o k' ] ≈ h ] → A [ k1 {d} h eq  ≈ k' ]
      uniqueness1 {d} {h} {eq} {k'} ek=h =   let open ≈-Reasoning (A) in
             begin
                k1 {d} h eq
             ≈⟨⟩
                γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id d) (f o h)
             ≈↑⟨ car (cong-γ bur {a} {b} {c} {d} ek=h ) ⟩
                γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id d) (f o h)
             ≈↑⟨ cdr (cong-δ bur (resp ek=h refl-hom )) ⟩
                γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id d) ( f o ( α bur f g e o k') ) 
             ≈⟨ b4 bur ⟩
                 k'
             ∎


-- end