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
: B β Coeq f g
inc : β x β inc (f x) β‘ inc (g x)
glue : is-set (Coeq f g) squash
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} β¦ _ : H-Level C 2 β¦
β (h : B β C)
β (β x β h (f x) β‘ h (g x)) β Coeq f g β C
(inc x) = h x
Coeq-rec h h-coeqs (glue x i) = h-coeqs x i
Coeq-rec h h-coeqs (squash x y p q i j) =
Coeq-rec β¦ cs β¦ h h-coeqs 2 (g x) (g y) (Ξ» i β g (p i)) (Ξ» i β g (q i)) i j
hlevel where g = Coeq-rec β¦ cs β¦ 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
(inc x) = cinc x Coeq-elim-prop cprop cinc
Since C was assumed to be a family of propositions, we automatically
get the necessary coherences for glue
and squash
.
{f = f} {g = g} cprop cinc (glue x i) =
Coeq-elim-prop (Ξ» i β cprop (glue x i)) (cinc (f x)) (cinc (g x)) i
is-propβpathp (squash x y p q i j) =
Coeq-elim-prop cprop cinc (Ξ» i j β cprop (squash x y p q i j))
is-propβsquarep (Ξ» 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
: β {β} (f g : A β B) β Type β β Type _
coeq-cone {B = B} f g C = Ξ£[ h β (B β C) ] (h β f β‘ h β g) coeq-cone
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β.
: β {β} {C : Type β} {f g : A β B} β¦ _ : H-Level C 2 β¦
Coeq-univ β is-equiv {A = Coeq f g β C} {B = coeq-cone f g C}
(Ξ» h β h β inc , Ξ» i z β h (glue z i))
{C = C} {f = f} {g = g} =
Coeq-univ (iso cr' (Ξ» x β refl) islinv) where
is-isoβis-equiv : coeq-cone f g C β Coeq f g β C
cr' (f , f-coeqs) = Coeq-rec f (happly f-coeqs)
cr'
: is-left-inverse cr' (Ξ» h β h β inc , Ξ» i z β h (glue z i))
islinv = trivial! islinv f
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:
: β {β} {f g : A β B} {C : Coeq f g β Type β}
Coeq-elim β (β 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
(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) =
Coeq-elim cset ci cg (Ξ» i j β cset (squash x y p q i j))
is-setβsquarep (Ξ» i β g x) (Ξ» i β g (p i)) (Ξ» i β g (q i)) (Ξ» i β g y) i j
where g = Coeq-elim cset ci cg
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
: β {β} β (A β A β Type β) β Type (level-of A β β)
tot {A = A} R = Ξ£[ x β A ] Ξ£[ y β A ] R x y
tot
: β {β} {R : A β A β Type β} β tot R β A
/-left (x , _ , _) = x
/-left
: β {β} {R : A β A β Type β} β tot R β A
/-right (_ , x , _) = x /-right
We form the quotient as the aforementioned coequaliser of the two projections from the total space of
_/_ : β {β β'} (A : Type β) (R : A β A β Type β') β Type (β β β')
= Coeq (/-left {R = R}) /-right
A / R
infixl 25 _/_
: β {β β'} {A : Type β} {R : A β A β Type β'} {x y : A} β R x y
quot β Path (A / R) (inc x) (inc y)
= glue (_ , _ , r) quot r
Using Coeq-elim
, we can recover
the elimination principle for quotients:
: β {β} {B : A / R β Type β}
Quot-elim β (β 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
= Coeq-elim bset f Ξ» { (x , y , w) β r x y w } Quot-elim bset f r
Conversely, we can describe coequalisers in terms of quotients. In order to form the coequaliser of we interpret the span formed by and as a binary relation on a witness that are related is an element of the fibre of at that is an such that and
spanβR: β {β β'} {A : Type β} {B : Type β'} (f g : A β B)
β B β B β Type (β β β')
= curry (fibre β¨ f , g β©) spanβR f g
We then recover the coequaliser of and as the quotient of by this relation.
Coeqβquotient: β {β β'} {A : Type β} {B : Type β'} (f g : A β B)
β Coeq f g β B / spanβR f g
{B = B} f g = IsoβEquiv is where
Coeqβquotient : Iso (Coeq f g) (B / spanβR f g)
is .fst = Coeq-rec inc Ξ» a β quot (a , refl)
is .snd .inv = Coeq-rec inc Ξ» (_ , _ , a , p) β
is (ap (inc β fst) p) Β·Β· glue a Β·Β· ap (inc β snd) p
sym .snd .rinv = elim! Ξ» _ β refl
is .snd .linv = elim! Ξ» _ β refl is
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 β'
: β x y β is-prop (x βΌ y)
has-is-prop : β {x} β x βΌ x
reflαΆ _βαΆ_ : β {x y z} β x βΌ y β y βΌ z β x βΌ z
: β {x y} β x βΌ y β y βΌ x
symαΆ
infixr 30 _βαΆ_
= _βΌ_
relation
: Type _
quotient = A / _βΌ_ quotient
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
: A β quotient β Prop β'
Code = Quot-elim
Code x (Ξ» x β n-Type-is-hlevel 1)
(Ξ» y β el (x βΌ y) (has-is-prop x y) {- 1 -})
Ξ» y z r β
(prop-ext (has-is-prop _ _) (has-is-prop _ _)
n-ua (Ξ» z β z βαΆ r)
Ξ» z β z βαΆ (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 -}
).
: β x y (p : inc x β‘ y) β β£ Code x y β£
encode = subst (Ξ» y β β£ Code x y β£) p reflαΆ
encode x y p
: β x y (p : β£ Code x y β£) β inc x β‘ y
decode = elim! Ξ» x y r β quot r decode
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
.
: β {x y : A} β is-equiv (quot {R = relation})
is-effective {x = x} {y} =
is-effective (has-is-prop x y) (squash _ _) (decode x (inc y)) (encode x (inc y)) .snd prop-ext
Relation to surjectionsπ
As mentioned in the definition of surjection, we can view a cover as expressing a way of gluing together the type by adding paths between the elements of When and are sets, this sounds a lot like a quotient! And, indeed, we can prove that every surjection induces an equivalence between its codomain and a quotient of its domain.
First, we define the kernel pair of a function the congruence on defined to be identity under
Kernel-pair: β {β β'} {A : Type β} {B : Type β'} β is-set B β (A β B)
β Congruence A β'
._βΌ_ a b = f a β‘ f b
Kernel-pair b-set f .has-is-prop x y = b-set (f x) (f y)
Kernel-pair b-set f .reflαΆ = refl
Kernel-pair b-set f ._βαΆ_ = _β_
Kernel-pair b-set f .symαΆ = sym Kernel-pair b-set f
We can then set about proving that, if is a surjection into a set, then is the quotient of under the kernel pair of
surjectionβis-quotient: β {β β'} {A : Type β} {B : Type β'}
β (b-set : is-set B)
β (f : A β B)
β B β Congruence.quotient (Kernel-pair b-set (f .fst))
The construction is pretty straightforward: each fibre defines an element If we have another fibre then because
so the function is constant, and factors through the propositional truncation
: β {x} β fibre f x β c.quotient
gβ (a , p) = inc a
gβ
abstract
: β {x} (pβ pβ : fibre f x) β gβ pβ β‘ gβ pβ
gβ-const (_ , p) (_ , q) = quot (p β sym q)
gβ-const
: β {x} β β₯ fibre f x β₯ β c.quotient
gβ = β₯-β₯-rec-set (hlevel 2) gβ gβ-const f gβ f
Since each is inhabited, all of these functions glue together to give a function A simple calculation shows that this function is both injective and surjective; since its codomain is a set, that means itβs an equivalence.
: B β c.quotient
g' = gβ (surj x)
g' x
: injective g'
g'-inj {x} {y} = β₯-β₯-elimβ {P = Ξ» a b β gβ a β‘ gβ b β x β‘ y}
g'-inj (Ξ» _ _ β fun-is-hlevel 1 (b-set _ _))
(Ξ» (_ , p) (_ , q) r β sym p β c.effective r β q)
(surj x) (surj y)
: is-surjective g'
g'-surj = do
g'-surj x (y , p) β inc-is-surjective x
(f y , ap gβ (squash (surj (f y)) (inc (y , refl))) β p) pure
Closuresπ
We define the reflexive, transitive and symmetric closure of a relation and prove that it induces the same quotient as
module _ {β β'} {A : Type β} (R : A β A β Type β') where
data Closure : A β A β Type (β β β') where
: β {x y} β R x y β Closure x y
inc : β {x} β Closure x x
Closure-refl : β {x y z} β Closure x y β Closure y z β Closure x z
Closure-trans : β {x y} β Closure y x β Closure x y
Closure-sym : β {x y} β is-prop (Closure x y)
squash
: Congruence A _
Closure-congruence .Congruence._βΌ_ = Closure
Closure-congruence .Congruence.has-is-prop _ _ = squash
Closure-congruence .Congruence.reflαΆ = Closure-refl
Closure-congruence .Congruence._βαΆ_ = Closure-trans
Closure-congruence .Congruence.symαΆ = Closure-sym Closure-congruence
Closure-quotient: β {β β'} {A : Type β} (R : A β A β Type β')
β A / R β A / Closure R
{A = A} R = IsoβEquiv is where
Closure-quotient : Iso (A / R) (A / Closure R)
is .fst = Coeq-rec inc Ξ» (a , b , r) β quot (inc r)
is .snd .inv = Coeq-rec inc Ξ» (a , b , r) β Closure-rec-β‘ _ inc quot r
is .snd .rinv = elim! Ξ» _ β refl
is .snd .linv = elim! Ξ» _ β refl is