{-# OPTIONS --without-K --safe #-}

open import Categories.Category

-- we use duality to prove properties about coequalizer
module Categories.Diagram.Coequalizer.Properties {o  e} (C : Category o  e) where

open Category C

open import Categories.Diagram.Coequalizer C using (Coequalizer; IsCoequalizer)
open import Categories.Morphism C
import Categories.Morphism.Reasoning as MR
open import Categories.Diagram.Equalizer op
open import Categories.Diagram.Equalizer.Properties op
open import Categories.Diagram.Duality C
open import Categories.Diagram.KernelPair C
open import Categories.Diagram.Pullback C
open import Categories.Morphism.Regular C


import Relation.Binary.Reasoning.Setoid as SR

open Pullback hiding (universal; unique)

private
  variable
    A B : Obj
    f g : A  B

module _ (coe : Coequalizer f g) where
  open Coequalizer coe

  private
    equalizer : Equalizer f g
    equalizer = Coequalizer⇒coEqualizer coe

  open Equalizer equalizer
    using (unique′; unique-diagram)
    renaming ( id-equalize      to id-coequalize
             ; equalize-resp-≈  to coequalize-resp-≈
             ; equalize-resp-≈′ to coequalize-resp-≈′
             )
    public

-- a regular epi is a coequalizer of its kernel pair
regular-is-coeq-kp : {A B : Obj} (f : A  B)  RegularEpi f  (kp : KernelPair f)  IsCoequalizer (p₁ kp) (p₂ kp) f
regular-is-coeq-kp {A} {B} f record { C = D ; h = h ; g = g ; coequalizer = coeq } kp = record
  { equality   = IsPullback.commute (isPullback kp)
  ; coequalize = λ {_}{u} u∘p₁≈u∘p₂  coequalize (u∘h≈u∘g u u∘p₁≈u∘p₂)
  ; universal  = universal
  ; unique     = unique
  }

  where
    open IsCoequalizer coeq
    pb-univ : D  P kp
    pb-univ = IsPullback.universal (isPullback kp) equality

    u∘h≈u∘g : {X : Obj}  (u : A  X)  u  (p₁ kp)  u  (p₂ kp)  u  h  u  g
    u∘h≈u∘g {X} u u∘p₁≈u∘p₂ = begin
      u  h                   ≈˘⟨ refl⟩∘⟨ p₁∘universal≈h₁ kp 
      u  (p₁ kp   pb-univ)  ≈⟨ pullˡ u∘p₁≈u∘p₂ 
      (u  p₂ kp)  pb-univ   ≈⟨ pullʳ (p₂∘universal≈h₂ kp) 
      u  g                   
      where
        open Category.HomReasoning C
        open MR C

retract-coequalizer :  {X Y} {f : Y  X} {g : X  Y}  f RetractOf g  IsCoequalizer (g  f) id f
retract-coequalizer f∘g≈id = IscoEqualizer⇒IsCoequalizer (section-equalizer f∘g≈id)