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,$ by means of a surjection $[-] : A ↠ A / \sim$ having $[x] = [y]$ equivalent to $x \sim y .$ However, depending on the specifics of $R,$ 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 .$ 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,$ for an equivalence relation $x \sim y,$ is one that is the identity “up to $\sim$ ”, i.e., we have $x \sim n (x),$ and which respects the relation, in that, if we have $x \sim y,$ then $n (x) = n (y) .$

    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 (2 + n)
    hl-a = basic-instance 2 has-is-set

It turns out that this is just enough to asking for a splitting of the quotient map $[-] :$ 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,$ we take the fibre over $[x]$ to be $n (x),$ 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)} 2)
    (λ 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) .$

  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,$ we define the normalisation procedure to be $n (x) = c [x] .$

split-surjection→is-split-congruence
  : ⦃ _ : H-Level A 2 ⦄ (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 2
  ; 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