open import 1Lab.Prelude

module Data.Set.Coequaliser where


# Set Coequalisersπ

In their most general form, colimits can be pictured as taking disjoint unions and then βgluing togetherβ some parts. The βgluing togetherβ part of that definition is where coequalisers come in: If you have parallel maps $f, g : A \to B$, then the coequaliser $\id{coeq}(f,g)$ can be thought of as β$B$, with the images of $f$ and $g$ identifiedβ.

data Coeq (f g : A β B) : Type (level-of A β level-of B) where
inc    : B β Coeq f g
glue   : β x β inc (f x) β‘ inc (g x)
squash : is-set (Coeq f g)


The universal property of coequalisers, being a type of colimit, is a mapping-out property: Maps from $\id{coeq}(f,g)$ are maps out of $B$, satisfying a certain property. Specifically, for a map $h : B \to C$, if we have $h \circ f = h \circ g$, then the map $f$ factors (uniquely) through inc. The situation can be summarised with the diagram below.

We refer to this unique factoring as Coeq-rec.

Coeq-rec : β {β} {C : Type β} {f g : A β B}
β is-set C β (h : B β C)
β (β x β h (f x) β‘ h (g x)) β Coeq f g β C
Coeq-rec cset h h-coeqs (inc x) = h x
Coeq-rec cset h h-coeqs (glue x i) = h-coeqs x i
Coeq-rec cset h h-coeqs (squash x y p q i j) =
cset (g x) (g y) (Ξ» i β g (p i)) (Ξ» i β g (q i)) i j
where g = Coeq-rec cset h h-coeqs


An alternative phrasing of the desired universal property is precomposition with inc induces an equivalence between the βspace of maps $B \to C$ which coequalise $f$ and $g$β and the maps $\id{coeq}(f,g) \to C$. In this sense, inc is the universal map which coequalises $f$ and $g$.

To construct the map above, we used Coeq-elim-prop, which has not yet been defined. It says that, to define a dependent function from Coeq to a family of propositions, it suffices to define how it acts on inc: The path constructions donβt matter.

Coeq-elim-prop : β {β} {f g : A β B} {C : Coeq f g β Type β}
β (β x β is-prop (C x))
β (β x β C (inc x))
β β x β C x
Coeq-elim-prop cprop cinc (inc x) = cinc x


Since C was assumed to be a family of propositions, we automatically get the necessary coherences for glue and squash.

Coeq-elim-prop {f = f} {g = g} cprop cinc (glue x i) =
is-propβpathp (Ξ» i β cprop (glue x i)) (cinc (f x)) (cinc (g x)) i
Coeq-elim-prop cprop cinc (squash x y p q i j) =
is-propβsquarep (Ξ» i j β cprop (squash x y p q i j))
(Ξ» i β g x) (Ξ» i β g (p i)) (Ξ» i β g (q i)) (Ξ» i β g y) i j
where g = Coeq-elim-prop cprop cinc


Since βthe space of maps $h : B \to C$ which coequalise $f$ and $g$β is a bit of a mouthful, we introduce an abbreviation: Since a colimit is defined to be a certain universal (co)cone, we call these Coeq-cones.

private
coeq-cone : β {β} (f g : A β B) β Type β β Type _
coeq-cone {B = B} f g C = Ξ£[ h β (B β C) ] (h β f β‘ h β g)


The universal property of Coeq then says that Coeq-cone is equivalent to the maps $\id{coeq}(f,g) \to C$, and this equivalence is given by inc, the βuniversal Coequalising mapβ.

Coeq-univ : β {β} {C : Type β} {f g : A β B}
β is-set C
β is-equiv {A = Coeq f g β C} {B = coeq-cone f g C}
(Ξ» h β h β inc , Ξ» i z β h (glue z i))
Coeq-univ {C = C} {f = f} {g = g} cset =
is-isoβis-equiv (iso cr' (Ξ» x β refl) islinv)
where
open is-iso
cr' : coeq-cone f g C β Coeq f g β C
cr' (f , f-coeqs) = Coeq-rec cset f (happly f-coeqs)

islinv : is-left-inverse cr' (Ξ» h β h β inc , Ξ» i z β h (glue z i))
islinv f = funext (Coeq-elim-prop (Ξ» x β cset _ _) Ξ» x β refl)


# Eliminationπ

Above, we defined what it means to define a dependent function $(x : \id{coeq}(f,g)) \to C\ x$ when $C$ is a family of propositions, and what it means to define a non-dependent function $\id{coeq}(f,g) \to C$. Now, we combine the two notions, and allow dependent elimination into families of sets:

Coeq-elim : β {β} {f g : A β B} {C : Coeq f g β Type β}
β (β x β is-set (C x))
β (ci : β x β C (inc x))
β (β x β PathP (Ξ» i β C (glue x i)) (ci (f x)) (ci (g x)))
β β x β C x
Coeq-elim cset ci cg (inc x) = ci x
Coeq-elim cset ci cg (glue x i) = cg x i
Coeq-elim cset ci cg (squash x y p q i j) =
is-setβsquarep (Ξ» i j β cset (squash x y p q i j))
(Ξ» i β g x) (Ξ» i β g (p i)) (Ξ» i β g (q i)) (Ξ» i β g y) i j
where g = Coeq-elim cset ci cg


There is a barrage of combined eliminators, whose definitions are not very enlightening β you can mouse over these links to see their types: Coeq-elim-propβ Coeq-elim-propβ Coeq-elimβ Coeq-recβ.

# Quotientsπ

With dependent sums, we can recover quotients as a special case of coequalisers. Observe that, by taking the total space of a relation $R : A \to A \to \ty$, we obtain two projection maps which have as image all of the possible related elements in $A$. By coequalising these projections, we obtain a space where any related objects are identified: The quotient $A/R$.

private
tot : β {β} β (A β A β Type β) β Type (level-of A β β)
tot {A = A} R = Ξ£[ x β A ] Ξ£[ y β A ] R x y

/-left : β {β} {R : A β A β Type β} β tot R β A
/-left (x , _ , _) = x

/-right : β {β} {R : A β A β Type β} β tot R β A
/-right (_ , x , _) = x


We form the quotient as the aforementioned coequaliser of the two projections from the total space of $R$:

_/_ : β {β β'} (A : Type β) (R : A β A β Type β') β Type (β β β')
A / R = Coeq (/-left {R = R}) /-right

quot : β {β β'} {A : Type β} {R : A β A β Type β'} {x y : A} β R x y
β Path (A / R) (inc x) (inc y)
quot r = glue (_ , _ , r)


Using Coeq-elim, we can recover the elimination principle for quotients:

Quot-elim : β {β} {B : A / R β Type β}
β (β x β is-set (B x))
β (f : β x β B (inc x))
β (β x y (r : R x y) β PathP (Ξ» i β B (quot r i)) (f x) (f y))
β β x β B x
Quot-elim bset f r = Coeq-elim bset f Ξ» { (x , y , w) β r x y w }


## Effectivityπ

The most well-behaved case of quotients is when $R : A \to A \to \ty$ takes values in propositions, is reflexive, transitive and symmetric (an equivalence relation). In this case, we have that the quotient $A / R$ is effective: The map quot is an equivalence.

module _ {A : Type β} {R : A β A β Type β'}
(Rp : β x y β is-prop (R x y))
(rr : β {x} β R x x)
(rt : β {x y z} β R x y β R y z β R x z)
(rs : β {x y} β R x y β R y x)
where


We will show this using an encode-decode method. For each $x : A$, we define a type family $\id{Code}_x(p)$, which represents an equality $\id{inc}(x) = y$. Importantly, the fibre over $\id{inc}(y)$ will be $R(x, y)$, so that the existence of functions converting between $\id{Code}_x(y)$ and paths $\id{inc}(x) = y$ is enough to establish effectivity of the quotient.

  private
Code : A β A / R β Prop β'
Code x = Quot-elim
(Ξ» x β n-Type-is-hlevel 1)
(Ξ» y β {- 1 -} R x y , Rp x y)
Ξ» y z r β
n-ua (prop-ext (Rp _ _) (Rp _ _) (Ξ» z β rt z r) Ξ» z β rt z (rs r))


We do quotient induction into the type of propositions, which by univalence is a set. Since the fibre over $\id{inc}(y)$ must be $R(x, y)$, thatβs what we give for the inc constructor ({- 1 -}, above). For this to respect the quotient, it suffices to show that, given $R(y,z)$, we have $R(x,y) \Leftrightarrow R(x,z)$, which follows from the assumption that $R$ is an equivalence relation ({- 2 -}).

    encode : β x y (p : inc x β‘ y) β β£ Code x y β£
encode x y p = subst (Ξ» y β β£ Code x y β£) p rr

decode : β x y (p : β£ Code x y β£) β inc x β‘ y
decode x y p =
Coeq-elim-prop {C = Ξ» y β (p : β£ Code x y β£) β inc x β‘ y}
(Ξ» _ β Ξ -is-hlevel 1 Ξ» _ β squash _ _) (Ξ» y r β quot r) y p


For encode, it suffices to transport the proof that $R$ is reflexive along the given proof, and for decoding, we eliminate from the quotient to a proposition. It boils down to establishing that $R(x,y) \to \id{inc}(x) \equiv \id{inc}(y)$, which is what the constructor quot says. Putting this all together, we get a proof that equivalence relations are effective.

  effective : β {x y : A} β is-equiv (quot {R = R})
effective {x = x} {y} =
prop-ext (Rp x y) (squash _ _) (decode x (inc y)) (encode x (inc y)) .snd