open import Cat.Diagram.Coequaliser.RegularEpi
open import Cat.Diagram.Coproduct.Copower
open import Cat.Diagram.Coproduct.Indexed
open import Cat.Diagram.Coequaliser
open import Cat.Prelude

import Cat.Diagram.Separator.Strong
import Cat.Morphism.StrongEpi
import Cat.Diagram.Separator
import Cat.Reasoning

module Cat.Diagram.Separator.Regular
  {o β„“}
  (C : Precategory o β„“)
  (coprods : (I : Set β„“) β†’ has-coproducts-indexed-by C ∣ I ∣)
  where

open Cat.Morphism.StrongEpi C
open Cat.Diagram.Separator.Strong C coprods
open Cat.Diagram.Separator C
open Cat.Reasoning C
open Copowers coprods

private variable
  s : Ob

Regular separatorsπŸ”—

Let be a category with set-indexed coproducts. An object is a regular separator if the canonical map is a regular epi.

is-regular-separator : Ob β†’ Type (o βŠ” β„“)
is-regular-separator s = βˆ€ {x} β†’ is-regular-epi C (βŠ—!.match (Hom s x) s Ξ» e β†’ e)

A family of objects is a regular separating family if the canonical map is a regular epi.

is-regular-separating-family
  : βˆ€ (Idx : Set β„“)
  β†’ (sα΅’ : ∣ Idx ∣ β†’ Ob)
  β†’ Type (o βŠ” β„“)
is-regular-separating-family Idx sα΅’ =
  βˆ€ {x} β†’ is-regular-epi C (∐!.match (Ξ£[ i ∈ ∣ Idx ∣ ] (Hom (sα΅’ i) x)) (sα΅’ βŠ™ fst) snd)

To motivate this definition, note that dense separators are extremely rare, as they impose a strong discreteness condition on Instead, it is slightly more reasonable to assume that every object of arises via some quotient of a bunch of points. This intuition is what regular separators codify.

As the name suggests, regular separators and regular separating families are separators and separating families, respectively. This follows directly from the fact that regular epis are epis.

regular-separator→separator
  : βˆ€ {s}
  β†’ is-regular-separator s
  β†’ is-separator s
regular-separator→separator regular =
  epi→separator coprods $
  is-regular-epi→is-epic regular

regular-separating-family→separating-family
  : βˆ€ (Idx : Set β„“) (sα΅’ : ∣ Idx ∣ β†’ Ob)
  β†’ is-regular-separating-family Idx sα΅’
  β†’ is-separating-family sα΅’
regular-separating-family→separating-family Idx sᡒ regular =
  epi→separating-family coprods Idx sᡒ $
  is-regular-epi→is-epic regular

Relations to other separatorsπŸ”—

Every dense separator is regular.

dense-separator→regular-separator
  : is-dense-separator s
  β†’ is-regular-separator s

The proof here mirrors the proof that colimits yield regular epis in the presence of enough coproducts. More explicitly, the idea is that is already a sufficient approximation of so we do not need to perform any quotienting. In other words, ought to be a coequalising pair.

dense-separator→regular-separator {s = s} dense {x} = regular where
  module dense = is-dense-separator dense
  open is-regular-epi
  open is-coequaliser

  regular : is-regular-epi C (βŠ—!.match (Hom s x) s Ξ» e β†’ e)
  regular .r = Hom s x βŠ—! s
  regular .arr₁ = id
  regular .arrβ‚‚ = id
  regular .has-is-coeq .coequal = refl

This is straightforward enough to prove with sufficient elbow grease.

  regular .has-is-coeq .universal {e' = e'} _ =
    dense.universal Ξ» e β†’ e' ∘ βŠ—!.ΞΉ (Hom s x) s e
  regular .has-is-coeq .factors {e' = e'} {p = p} =
    βŠ—!.uniqueβ‚‚ (Hom s x) s Ξ» e β†’
      (dense.universal _ ∘ βŠ—!.match _ _ _) ∘ βŠ—!.ΞΉ _ _ e β‰‘βŸ¨ pullr (βŠ—!.commute _ _) βŸ©β‰‘
      dense.universal _ ∘ e                             β‰‘βŸ¨ dense.commute βŸ©β‰‘
      e' ∘ βŠ—!.ΞΉ _ _ e                                   ∎
  regular .has-is-coeq .unique {e' = e'} {colim = h} p =
    dense.unique _ Ξ» e β†’
      h ∘ e                           β‰‘Λ˜βŸ¨ ap (h ∘_) (βŠ—!.commute (Hom s x) s) βŸ©β‰‘Λ˜
      h ∘ βŠ—!.match _ _ _ ∘ βŠ—!.ΞΉ _ _ e β‰‘βŸ¨ pulll p βŸ©β‰‘
      e' ∘ βŠ—!.ΞΉ _ _ e                 ∎

Additionally, note that every regular separator is a strong separator; this follows directly from the fact that every regular epi is strong.

regular-separator→strong-separator
  : βˆ€ {s}
  β†’ is-regular-separator s
  β†’ is-strong-separator s
regular-separator→strong-separator {s} regular {x} =
  is-regular-epi→is-strong-epi _ regular