{o β„“} {C : Precategory o β„“}
    (isc : is-category C)
    (M : Monad C)

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

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.

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≅ (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 multiplication to that of 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 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
        : 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β‰… C.∘ Am .Ξ½ C.∘ Monad.M₁ M (map Aβ‰…X.from)                 β‰‘βŸ¨ C.pulll (sq Aβ‰… βŸ©β‰‘
          (Xm .Ξ½ C.∘ Monad.M₁ M (Aβ‰… .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 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' =
          (Ξ» j β†’ PathP
            (Ξ» i β†’ C.Hom (F-map-path (Monad.M M) isc isc Aβ‚€β‰…Xβ‚€ (~ j) i) (A₀≑Xβ‚€ i))
            (Am .Ξ½) (Xm .Ξ½))

    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) Aβ‰…X
    triv = EM.β‰…-pathp refl _
      (Algebra-hom-pathp _ _ _ (Univalent.Hom-pathp-reflr-iso isc (C.idr _)))