module Cat.Univalent.Instances.Algebra {o β} {C : Precategory o β} (isc : is-category C) (M : Monad C) where
Univalence of Eilenberg-Moore categoriesπ
Given a base univalent category , we can consider a monad on , and its associated Eilenberg-Moore category , as a standard way of constructing categories of βalgebraic gadgetsβ backed by objects of . A concrete example is given by the category of monoids: A monoid (in sets) is equivalent to an algebra for the list monad.
Given that βhand-rolledβ categories of this sort tend to be well-behaved, in particular when it comes to identifications (see univalence of monoids, univalence of groups, univalence of semilattices), itβs natural to ask whether all Eilenberg-Moore categories are themselves univalent, assuming that their underlying category is. Here we give a positive answer.
Fixing a monad
on a univalent category
,
we abbreviate its Eilenberg-Moore category
as EM
.
private EM = Eilenberg-Moore C M import Cat.Reasoning EM as EM import Cat.Reasoning C as C
As usual, we take the centre of contraction to be
and the identity isomorphism
;
The hard part is proving that, given a pair of
-algebras
and
,
together with a specified isomorphism
,
we can build an identification
,
such that over this
identification,
is the identity map.
Eilenberg-Moore-is-category : is-category EM Eilenberg-Moore-is-category = Ξ» { .to-path β Aβ‘X ; .to-path-over β triv} where module _ {A} {Am : Algebra-on C M A} {X} {Xm : Algebra-on C M X} (Aβ X : EM.Isomorphism (A , Am) (X , Xm)) where
The first thing we shall note is that an algebra is given by a pair
of two data: An underlying object
(resp
),
together with the structure
(resp.
)
of an M-algebra on
.
Hence, an identification of algebras can be broken down into an
identification of their components.
module A = Algebra-on Am module X = Algebra-on Xm module Aβ X = EM._β _ Aβ X open Algebra-hom renaming (morphism to map ; commutes to sq) open Algebra-on
Recall that a homomorphism of M-algebras
between
is given by a map
in
,
such that the diagram below commutes. By forgetting that the square
commutes, algebra homomorphisms correspond faithfully to morphisms in the
underlying category
.
Hence, given an isomorphism (let us call it ) in , we can forget all of the commutativity data associated with the algebra homomorphisms, and recover an isomorphism between the underlying objects in :
Aββ Xβ : A C.β X Aββ Xβ = C.make-iso (map Aβ X.to) (map Aβ X.from) (ap map Aβ X.invl) (ap map Aβ X.invr)
Since we assumed
to be univalent, this isomorphism can be made into a path
.
This covers a third of the task: We must now show first that the algebra
structures
and
are identified over Aββ‘Xβ
, and we must prove that
the resulting identification makes
into the identity isomorphism.
Aββ‘Xβ : A β‘ X Aββ‘Xβ = isc .to-path Aββ Xβ
By the characterisation of paths in algebras
, it suffices
to show that Aββ‘Xβ
transports
βs
multiplication to that of
βs;
Using the corresponding lemma for paths in hom-spaces
of
univalent categories, we can get away with (still calling our
isomorphism
)
showing the square below commutes.
Since we have assumed that is an -algebra isomorphism, we can simultaneously turn the square above into one which has and in adjacent faces and swap for ; A straightforward calculation then shows that the square above commutes.
Amβ‘Xm : PathP (Ξ» i β Algebra-on C M (Aββ‘Xβ i)) Am Xm Amβ‘Xm = Algebra-on-pathp _ Aββ‘Xβ same-mults' where same-mults : PathP (Ξ» i β C.Hom (isc .to-path (F-map-iso (Monad.M M) Aββ Xβ) i) (Aββ‘Xβ i)) (Am .Ξ½) (Xm .Ξ½) same-mults = Univalent.Hom-pathp-iso isc ( map Aβ X.to C.β Am .Ξ½ C.β Monad.Mβ M (map Aβ X.from) β‘β¨ C.pulll (sq Aβ X.to) β©β‘ (Xm .Ξ½ C.β Monad.Mβ M (Aβ X.to .map)) C.β Monad.Mβ M (map Aβ X.from) β‘β¨ C.cancelr (sym (Monad.M-β M _ _) Β·Β· ap (Monad.Mβ M) (ap map Aβ X.invl) Β·Β· Monad.M-id M) β©β‘ Xm .Ξ½ β )
Note, however, that the path above is not in the correct space! While
it is in a space of
-morphisms,
the source is not of the correct type. This is because functors between
univalent categories can act on paths in βtwoβ ways: One can either
apply the functorβs action on isos
, then take a
path in the codomain category; Or take a path in the domain category,
and then use the canonical action on paths
. Fortunately
these coincide
, and we can correct
the source:
same-mults' : PathP (Ξ» i β C.Hom (Monad.Mβ M (Aββ‘Xβ i)) (Aββ‘Xβ i)) (Am .Ξ½) (Xm .Ξ½) same-mults' = transport (Ξ» j β PathP (Ξ» i β C.Hom (F-map-path isc isc (Monad.M M) Aββ Xβ (~ j) i) (Aββ‘Xβ i)) (Am .Ξ½) (Xm .Ξ½)) same-mults Aβ‘X : Path (Algebra _ M) (A , Am) (X , Xm) Aβ‘X i = Aββ‘Xβ i , Amβ‘Xm i
To finish the proof that
is univalent, we must show that the identification weβve built
trivialises the isomorphism
we were given. This follows immediately from the characterisation of
paths in isomorphism spaces
and
in Hom-spaces
.
triv : PathP (Ξ» i β (A , Am) EM.β Aβ‘X i) EM.id-iso Aβ X triv = EM.β -pathp refl _ (Algebra-hom-pathp _ _ _ (Univalent.Hom-pathp-reflr-iso isc (C.idr _)))