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 , then the coequaliser can be thought of as β, with the images of and 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
are maps out of
,
satisfying a certain property. Specifically, for a map
,
if we have
,
then the map
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
which coequalise
and
β
and the maps
.
In this sense, inc
is the
universal map which coequalises
and
.
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
which coequalise
and
β
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-cone
s.
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
,
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 when is a family of propositions, and what it means to define a non-dependent function . 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-recβ
.
{-# TERMINATING #-} Coeq-elim-propβ : β {β} {f g : A β B} {f' g' : A' β B'} {C : Coeq f g β Coeq f' g' β Type β} β (β x y β is-prop (C x y)) β (β x y β C (inc x) (inc y)) β β x y β C x y Coeq-elim-propβ prop f (inc x) (inc y) = f x y Coeq-elim-propβ {f' = f'} {g'} prop f (inc x) (glue y i) = is-propβpathp (Ξ» i β prop (inc x) (glue y i)) (f x (f' y)) (f x (g' y)) i Coeq-elim-propβ prop f (inc x) (squash y y' p q i j) = is-propβsquarep (Ξ» i j β prop (inc x) (squash y y' p q i j)) (Ξ» i β Coeq-elim-propβ prop f (inc x) y) (Ξ» i β Coeq-elim-propβ prop f (inc x) (p i)) (Ξ» i β Coeq-elim-propβ prop f (inc x) (q i)) (Ξ» i β Coeq-elim-propβ prop f (inc x) y') i j Coeq-elim-propβ {f = f'} {g = g'} prop f (glue x i) y = is-propβpathp (Ξ» i β prop (glue x i) y) (Coeq-elim-propβ prop f (inc (f' x)) y) (Coeq-elim-propβ prop f (inc (g' x)) y) i Coeq-elim-propβ prop f (squash x x' p q i j) y = is-propβsquarep (Ξ» i j β prop (squash x x' p q i j) y) (Ξ» i β Coeq-elim-propβ prop f x y) (Ξ» i β Coeq-elim-propβ prop f (p i) y) (Ξ» i β Coeq-elim-propβ prop f (q i) y) (Ξ» i β Coeq-elim-propβ prop f x' y) i j Coeq-elim-propβ : β {β} {f g : A β B} {f' g' : A' β B'} {f'' g'' : A'' β B''} {C : Coeq f g β Coeq f' g' β Coeq f'' g'' β Type β} β (β x y z β is-prop (C x y z)) β (β x y z β C (inc x) (inc y) (inc z)) β β x y z β C x y z Coeq-elim-propβ cprop f (inc a) y z = Coeq-elim-propβ (Ξ» x y β Ξ -is-hlevel 1 Ξ» z β cprop z x y) (Ξ» x y β Coeq-elim-prop (Ξ» z β cprop z (inc x) (inc y)) Ξ» z β f z x y) y z (inc a) Coeq-elim-propβ cprop f (glue x i) y z = Coeq-elim-propβ (Ξ» x y β Ξ -is-hlevel 1 Ξ» z β cprop z x y) (Ξ» x y β Coeq-elim-prop (Ξ» z β cprop z (inc x) (inc y)) Ξ» z β f z x y) y z (glue x i) Coeq-elim-propβ cprop f (squash x x' p q i j) y z = is-propβsquarep (Ξ» i j β cprop (squash x x' p q i j) y z) (Ξ» i β Coeq-elim-propβ cprop f x y z) (Ξ» i β Coeq-elim-propβ cprop f (p i) y z) (Ξ» i β Coeq-elim-propβ cprop f (q i) y z) (Ξ» i β Coeq-elim-propβ cprop f x' y z) i j Coeq-recβ : β {β} {f g : A β B} {f' g' : A' β B'} {C : Type β} β is-set C β (ci : B β B' β C) β (β a x β ci (f x) a β‘ ci (g x) a) β (β a x β ci a (f' x) β‘ ci a (g' x)) β Coeq f g β Coeq f' g' β C Coeq-recβ cset ci r1 r2 (inc x) (inc y) = ci x y Coeq-recβ cset ci r1 r2 (inc x) (glue y i) = r2 x y i Coeq-recβ cset ci r1 r2 (inc x) (squash y z p q i j) = cset (Coeq-recβ cset ci r1 r2 (inc x) y) (Coeq-recβ cset ci r1 r2 (inc x) z) (Ξ» j β Coeq-recβ cset ci r1 r2 (inc x) (p j)) (Ξ» j β Coeq-recβ cset ci r1 r2 (inc x) (q j)) i j Coeq-recβ cset ci r1 r2 (glue x i) (inc xβ) = r1 xβ x i Coeq-recβ {f = f} {g} {f'} {g'} cset ci r1 r2 (glue x i) (glue y j) = is-setβsquarep (Ξ» i j β cset) (Ξ» j β r1 (f' y) x j) (Ξ» j β r2 (f x) y j) (Ξ» j β r2 (g x) y j) (Ξ» j β r1 (g' y) x j) i j Coeq-recβ {f = f} {g} {f'} {g'} cset ci r1 r2 (glue x i) (squash y z p q j k) = is-hlevel-suc 2 cset (go (glue x i) y) (go (glue x i) z) (Ξ» j β go (glue x i) (p j)) (Ξ» j β go (glue x i) (q j)) (Ξ» i j β exp i j) (Ξ» i j β exp i j) i j k where go = Coeq-recβ cset ci r1 r2 exp : I β I β _ exp l m = cset (go (glue x i) y) (go (glue x i) z) (Ξ» j β go (glue x i) (p j)) (Ξ» j β go (glue x i) (q j)) l m Coeq-recβ cset ci r1 r2 (squash x y p q i j) z = cset (go x z) (go y z) (Ξ» j β go (p j) z) (Ξ» j β go (q j) z) i j where go = Coeq-recβ cset ci r1 r2 instance H-Level-coeq : β {f g : A β B} {n} β H-Level (Coeq f g) (2 + n) H-Level-coeq = basic-instance 2 squash
Quotientsπ
With dependent sums, we can recover quotients as a special case of coequalisers. Observe that, by taking the total space of a relation , we obtain two projection maps which have as image all of the possible related elements in . By coequalising these projections, we obtain a space where any related objects are identified: The quotient .
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 :
_/_ : β {β β'} (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
takes values in propositions, is reflexive, transitive and symmetric (an
equivalence relation). In this case, we have that the quotient
is effective: The map quot
is an equivalence.
record Congruence {β} (A : Type β) β' : Type (β β lsuc β') where field _βΌ_ : A β A β Type β' has-is-prop : β x y β is-prop (x βΌ y) reflαΆ : β {x} β x βΌ x _βαΆ_ : β {x y z} β x βΌ y β y βΌ z β x βΌ z symαΆ : β {x y} β x βΌ y β y βΌ x relation = _βΌ_ quotient : Type _ quotient = A / _βΌ_ module _ {A : Type β} (R : Congruence A β') where private module R = Congruence R
We will show this using an encode-decode method. For each , we define a type family , which represents an equality . Importantly, the fibre over will be , so that the existence of functions converting between and paths is enough to establish effectivity of the quotient.
private Code : A β R.quotient β Prop β' Code x = Quot-elim (Ξ» x β n-Type-is-hlevel 1) (Ξ» y β el (x R.βΌ y) (R.has-is-prop x y) {- 1 -}) Ξ» y z r β n-ua (prop-ext (R.has-is-prop _ _) (R.has-is-prop _ _) (Ξ» z β z R.βαΆ r) Ξ» z β z R.βαΆ (R.symαΆ r))
We do quotient induction into the type of propositions
, which by
univalence is a set
. Since the fibre over
must be
,
thatβs what we give for the inc
constructor
({- 1 -}
,
above). For this to respect the quotient, it suffices to show that,
given
,
we have
,
which follows from the assumption that
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 R.reflαΆ 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
is reflexive along the given proof, and for decoding, we eliminate from
the quotient to a proposition. It boils down to establishing that
,
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.relation}) effective {x = x} {y} = prop-ext (R.has-is-prop x y) (squash _ _) (decode x (inc y)) (encode x (inc y)) .snd
Quot-opβ : β {C : Type β} {T : C β C β Type β'} β (β x β R x x) β (β y β S y y) β (_β_ : A β B β C) β ((a b : A) (x y : B) β R a b β S x y β T (a β x) (b β y)) β A / R β B / S β C / T Quot-opβ Rr Sr op resp = Coeq-recβ squash (Ξ» x y β inc (op x y)) (Ξ» { z (x , y , r) β quot (resp x y z z r (Sr z)) }) Ξ» { z (x , y , r) β quot (resp z z x y (Rr z) r) } Discrete-quotient : β {A : Type β} (R : Congruence A β') β (β x y β Dec (Congruence.relation R x y)) β Discrete (Congruence.quotient R) Discrete-quotient cong rdec = Coeq-elim-propβ {C = Ξ» x y β Dec (x β‘ y)} (Ξ» x y β hlevel 1) go _ _ where go : β x y β Dec (inc x β‘ inc y) go x y with rdec x y ... | yes xRy = yes (quot xRy) ... | no Β¬xRy = no Ξ» p β Β¬xRy (equivβinverse (effective cong) p)