open import Cat.Diagram.Monad
open import Cat.Functor.Base
open import Cat.Univalent
open import Cat.Prelude

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 _)))