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 $\mathcal{C}$, we can consider a monad $M$ on $\mathcal{C}$, and its associated Eilenberg-Moore category $\mathcal{C}^M$, as a standard way of constructing categories of βalgebraic gadgetsβ backed by objects of $\mathcal{C}$. 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
$M$
on a univalent category
$\mathcal{C}$,
we abbreviate its Eilenberg-Moore category
$\mathcal{C}^M$
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
$A$
and the `identity isomorphism`

$A \cong A$;
The hard part is proving that, given a pair of
$M$-algebras
$A$
and
$X$,
together with a specified isomorphism
$f : A \cong X$,
we can build an identification
$A \cong X$,
such that over this
identification,
$f$
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
$A_0$
(resp
$X_0$),
together with the structure
$A_m$
(resp.
$X_m$)
of an `M-algebra on`

$A_0$.
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
$(A_0,A_m) \to (X_0,X_m)$
is given by a map
$h : A_0 \to X_0$
in
$\mathcal{C}$,
such that the diagram below commutes. By forgetting that the square
commutes, algebra homomorphisms correspond faithfully to morphisms in the
underlying category
$\mathcal{C}$.

Hence, given an *isomorphism*
$(A_0, A_m) \cong (X_0, X_m)$
(let us call it
$f$)
in
$\mathcal{C}^M$,
we can forget all of the commutativity data associated with the algebra
homomorphisms, and recover an isomorphism between the underlying objects
in
$\mathcal{C}$:

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
$\mathcal{C}$
to be univalent, this isomorphism can be `made into a path`

$A_0 \equiv X_0$.
This covers a third of the task: We must now show first that the algebra
structures
$A_m$
and
$X_m$
are identified over `Aββ‘Xβ`

, and we must prove that
the resulting identification makes
$f$
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
$A_m$βs
multiplication to that of
$X_m$βs;
Using the corresponding lemma for `paths in hom-spaces`

of
univalent categories, we can get away with (still calling our
isomorphism
$f$)
showing the square below commutes.

Since we have assumed that $f$ is an $M$-algebra isomorphism, we can simultaneously turn the square above into one which has $f$ and $f^{-1}$ in adjacent faces and swap $A_m$ for $X_m$; 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
$\mathcal{C}$-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
$\mathcal{C}^M$
is univalent, we must show that the identification weβve built
trivialises the isomorphism
$A \cong X$
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 _)))