module Data.Set.Coequaliser.Split where

# Split quotientsπ

Recall that a quotient of a set
$A$
by an equivalence relation
$xβΌy$
allows us to βreplaceβ the identity type of
$A$
by the relation
$R,$
by means of a surjection
$[β]:AβA/βΌ$
having
$[x]=[y]$
equivalent to
$xβΌ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/βΌ$
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*.

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βA,$ for an equivalence relation $xβΌy,$ is one that is the identity βup to $βΌ$β, i.e., we have $xβΌn(x),$ and which respects the relation, in that, if we have $xβΌy,$ then $n(x)=n(y).$

normalise : A β A represents : β x β x βΌ normalise x respects : β x y β x βΌ y β normalise x β‘ normalise y

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/βΌ$ 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

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βΌ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/βΌβ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