module Cat.Diagram.Limit.Equaliser {o h} (C : Precategory o h) where
We establish the correspondence between Equaliser
and the Limit
of a parallel arrows
diagram.
is-equaliser→is-limit : ∀ {e} (F : Functor ·⇉· C) {equ : Hom e (F .F₀ false)} → (eq : is-equaliser C (forkl F) (forkr F) equ) → is-limit {C = C} F e (Fork→Cone F (is-equaliser.equal eq)) is-equaliser→is-limit {e} F {equ} is-eq = to-is-limitp ml λ where {true} → refl {false} → refl where module is-eq = is-equaliser is-eq open make-is-limit ml : make-is-limit F e ml .ψ true = forkl F ∘ equ ml .ψ false = equ ml .commutes idh = eliml (F .F-id) ml .commutes inr = sym is-eq.equal ml .commutes inl = refl ml .universal eps p = is-eq.universal (p inl ∙ sym (p inr)) ml .factors {true} eps p = pullr is-eq.factors ∙ p inl ml .factors {false} eps p = is-eq.factors ml .unique eps p other q = is-eq.unique (q false) is-limit→is-equaliser : ∀ (F : Functor ·⇉· C) {K : Functor ⊤Cat C} → {eps : K F∘ !F => F} → is-ran !F F K eps → is-equaliser C (forkl F) (forkr F) (eps .η false) is-limit→is-equaliser F {K} {eps} lim = eq where module lim = is-limit lim parallel : ∀ {x} → Hom x (F .F₀ false) → (j : Bool) → Hom x (F .F₀ j) parallel e' true = forkl F ∘ e' parallel e' false = e' parallel-commutes : ∀ {x} {e' : Hom x (F .F₀ false)} → forkl F ∘ e' ≡ forkr F ∘ e' → ∀ i j → (h : ·⇉· .Precategory.Hom i j) → F .F₁ {i} {j} h ∘ parallel e' i ≡ parallel e' j parallel-commutes p _ _ idh = eliml (F .F-id) parallel-commutes p _ _ inl = refl parallel-commutes p _ _ inr = sym p eq : is-equaliser C (forkl F) (forkr F) (eps .η false) eq .equal = sym (eps .is-natural _ _ inl) ∙ eps .is-natural _ _ inr eq .universal {e' = e'} p = lim.universal (parallel e') (λ {i} {j} h → parallel-commutes p i j h) eq .factors = lim.factors {j = false} _ _ eq .unique {p = p} {other = other} q = lim.unique _ _ _ λ where true → ap (_∘ other) (intror (K .F-id) ∙ eps .is-natural _ _ inr) ∙∙ pullr q ∙∙ sym p false → q Equaliser→Limit : ∀ {F : Functor ·⇉· C} → Equaliser C (forkl F) (forkr F) → Limit F Equaliser→Limit {F = F} eq = to-limit (is-equaliser→is-limit F (has-is-eq eq)) Limit→Equaliser : ∀ {a b} {f g : Hom a b} → Limit {C = C} (Fork f g) → Equaliser C f g Limit→Equaliser lim .apex = _ Limit→Equaliser lim .equ = _ Limit→Equaliser {f = f} {g} lim .has-is-eq = is-limit→is-equaliser (Fork f g) (Limit.has-limit lim)