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

# Eilenberg-Moore Categories🔗

Given a base univalent category $\ca{C}$, we can consider a monad $M$ on $\ca{C}$, and its associated Eilenberg-Moore category $\ca{C}^M$, as a standard way of constructing categories of “algebraic gadgets” backed by objects of $\ca{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 $\ca{C}$, we abbreviate its Eilenberg-Moore category $\ca{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 A .centre = A , EM.id-iso Eilenberg-Moore-is-category (A , Am) .paths ((X , Xm) , A≅X) = Σ-pathp A≡M triv 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, re-using the equality lemma for dependent pairs.

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 $\ca{C}$, such that the diagram below commutes. By forgetting that the square commutes, algebra homomorphisms correspond faithfully to morphisms in the underlying category $\ca{C}$.

Hence, given an *isomorphism* $(A_0, A_m) \cong (X_0, X_m)$ (let us call it $f$) in $\ca{C}^M$, we can forget all of the commutativity data associated with the algebra homomorphisms, and recover an isomorphism between the underlying objects in $\ca{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 $\ca{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₀ = iso→path C isc 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 (iso→path C isc (F-map-iso (Monad.M M) A₀≅X₀) i) (A₀≡X₀ i)) (Am .ν) (Xm .ν) same-mults = Hom-pathp-iso C 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 $\ca{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 (Monad.M M) A₀≅X₀ isc isc (~ j) i) (A₀≡X₀ i)) (Am .ν) (Xm .ν)) same-mults A≡M : Path (Algebra _ M) (A , Am) (X , Xm) A≡M i = A₀≡X₀ i , Am≡Xm i

To finish the proof that $\ca{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≡M i) EM.id-iso A≅X triv = EM.≅-pathp refl _ (Algebra-hom-pathp _ _ _ (Hom-pathp-reflr-iso C isc (C.idr _)))