open import Cat.Instances.Shape.Parallel
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Equaliser
open import Cat.Instances.Functor
open import Cat.Diagram.Terminal
open import Cat.Prelude

open import Data.Bool

module Cat.Diagram.Limit.Equaliser {o h} (Cat : Precategory o h) where


We establish the correspondence between Equaliser and the Limit of a parallel arrows diagram.

Fork→Cone
: ∀ {E} (F : Functor ·⇉· Cat)
→ (eq : Hom E (F .F₀ false))
→ F .F₁ {false} {true} false ∘ eq ≡ F .F₁ {false} {true} true ∘ eq
→ Cone F
Fork→Cone F eq p .apex     = _
Fork→Cone F eq p .ψ false  = eq
Fork→Cone F eq p .ψ true   = F .F₁ false ∘ eq
Fork→Cone F eq p .commutes {false} {false} tt    = eliml (F .F-id)
Fork→Cone F eq p .commutes {false} {true}  false = refl
Fork→Cone F eq p .commutes {false} {true}  true  = sym p
Fork→Cone F eq p .commutes {true}  {true}  tt    = eliml (F .F-id)

Equaliser→Limit
: ∀ {F : Functor ·⇉· Cat}
→ Equaliser Cat (F .F₁ false) (F .F₁ true)
→ Limit F
Equaliser→Limit {F = F} eq = lim where
module eq = Equaliser eq
lim : Limit _
lim .top = Fork→Cone F eq.equ eq.equal
lim .has⊤ cone .centre .hom      =
eq.limiting (cone .commutes {false} {true} false ∙ sym (cone .commutes true))
lim .has⊤ cone .centre .commutes false = eq.universal
lim .has⊤ cone .centre .commutes true = pullr eq.universal ∙ cone .commutes {false} {true} false
lim .has⊤ cone .paths other = Cone-hom-path _ (sym (eq.unique p)) where
p : cone .ψ false ≡ eq .equ ∘ other .hom
p = sym (other .commutes _)

Limit→Equaliser
: ∀ {F : Functor ·⇉· Cat}
→ Limit F
→ Equaliser Cat (F .F₁ {false} {true} false) (F .F₁ true)
Limit→Equaliser {F} lim = eq where
module lim = Terminal lim
eq : Equaliser Cat _ _
eq .apex = _
eq .equ = lim.top .ψ false
eq .has-is-eq .equal =
lim.top .commutes {false} {true} false ∙ sym (lim.top .commutes true)
eq .has-is-eq .limiting p = lim.has⊤ (Fork→Cone _ _ p) .centre .hom
eq .has-is-eq .universal {p = p} =
lim.has⊤ (Fork→Cone _ _ p) .centre .commutes false
eq .has-is-eq .unique {e′ = e'} {p = p} {lim' = lim'} x =
sym (ap hom (lim.has⊤ (Fork→Cone _ _ p) .paths other))
where
other : Cone-hom _ _ _
other .hom = _
other .commutes false = sym x
other .commutes true = sym (
F .F₁ false ∘ e'                      ≡⟨ ap (_ ∘_) x ⟩≡
F .F₁ false ∘ lim.top .ψ false ∘ lim' ≡⟨ pulll (lim.top .commutes false) ⟩≡
lim.top .ψ true ∘ lim'                ∎
)