open import 1Lab.Prelude

open import Data.Set.Coequaliser

module Data.Set.Coequaliser.Split where

Split quotients🔗

Recall that a quotient of a set $A$ by an equivalence relation $x\sim y$ allows us to “replace” the identity type of $A$ by the relation $R\text{,}$ by means of a surjection $[-]:A\twoheadrightarrow A/\sim$ having $[x]=[y]$ equivalent to $x\sim y\text{.}$ However, depending on the specifics of $R\text{,}$ we may not need to actually take a quotient after all! It may be the case that $A/\sim$ is equivalent to a particular subset of $A\text{.}$ When this is the case, we say that the quotient is split. This module outlines sufficient conditions for a quotient to split, by appealing to our intuition about normal forms.

private variable
  ℓ ℓ' : Level
  A : Type ℓ

record is-split-congruence (R : Congruence A ℓ') : Type (level-of A ⊔ ℓ') where
  open Congruence R

  field
    has-is-set : is-set A

A normalisation function $n:A\to A\text{,}$ for an equivalence relation $x\sim y\text{,}$ is one that is the identity “up to $\sim$”, i.e., we have $x\sim n(x)\text{,}$ and which respects the relation, in that, if we have $x\sim y\text{,}$ then $n(x)=n(y)\text{.}$

    normalise : A → A

    represents : ∀ x → x ∼ normalise x
    respects   : ∀ x y → x ∼ y → normalise x ≡ normalise y

  private instance
    hl-a : ∀ {n} → H-Level A ( + n)
    hl-a = basic-instance  has-is-set

It turns out that this is just enough to asking for a splitting of the quotient map $[-]\text{:}$ We can define a function sending each $x:A/\sim$ to a fibre of the quotient map over it, by induction. At the points of $A\text{,}$ we take the fibre over $[x]$ to be $n(x)\text{,}$ and we have $[n(x)]=[x]$ by the first assumption. By the second assumption, this procedure respects the quotient.

  splitting : (x : Congruence.quotient R) → fibre inc x
  splitting (inc x) = record { fst = normalise x ; snd = quot (symᶜ (represents x)) }
  splitting (glue (x , y , r) i) = record
    { fst = respects x y r i
    ; snd = is-prop→pathp (λ i → Coeq.squash (inc (respects x y r i)) (quot r i))
      (quot (symᶜ (represents x))) (quot (symᶜ (represents y))) i
    }
  splitting (squash x y p q i j) = is-set→squarep
    (λ i j → hlevel {T = fibre inc (squash x y p q i j)} )
    (λ i → splitting x) (λ i → splitting (p i)) (λ i → splitting (q i)) (λ i → splitting y) i j

  choose : Congruence.quotient R → A
  choose x = splitting x .fst

Two other consequences of these assumptions are that the normalisation function is literally idempotent, and that it additionally reflects the quotient relation, in that $x\sim y$ is equivalent to $n(x)=n(y)\text{.}$

  normalises : ∀ x → normalise (normalise x) ≡ normalise x
  normalises x = respects (normalise x) x (symᶜ (represents x))

  reflects : ∀ x y → normalise x ≡ normalise y → x ∼ y
  reflects x y p = represents x ∙ᶜ reflᶜ' p ∙ᶜ symᶜ (represents y)

Finally, we show that any splitting of the quotient map generates a normalisation procedure in the above sense: if we have a map $c:A/\sim \to A\text{,}$ we define the normalisation procedure to be $n(x)=c[x]\text{.}$

split-surjection→is-split-congruence
  : ⦃ _ : H-Level A  ⦄ (R : Congruence A ℓ)
  → (∀ x → fibre {B = Congruence.quotient R} inc x)
  → is-split-congruence R
split-surjection→is-split-congruence R split = record
  { has-is-set = hlevel 
  ; normalise  = λ x → split (inc x) .fst
  ; represents = λ x → effective (sym (split (inc x) .snd))
  ; respects   = λ x y p → ap (fst ∘ split) (quot p)
  } where open Congruence R