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 C\ca{C}, we can consider a monad MM on C\ca{C}, and its associated Eilenberg-Moore category CM\ca{C}^M, as a standard way of constructing categories of β€œalgebraic gadgets” backed by objects of C\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 MM on a univalent category C\ca{C}, we abbreviate its Eilenberg-Moore category CM\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 AA and the identity isomorphism A≅AA \cong A; The hard part is proving that, given a pair of MM-algebras AA and XX, together with a specified isomorphism f:A≅Xf : A \cong X, we can build an identification A≅XA \cong X, such that over this identification, ff 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 A0A_0 (resp X0X_0), together with the structure AmA_m (resp. XmX_m) of an M-algebra on A0A_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 (A0,Am)β†’(X0,Xm)(A_0,A_m) \to (X_0,X_m) is given by a map h:A0β†’X0h : A_0 \to X_0 in C\ca{C}, such that the diagram below commutes. By forgetting that the square commutes, algebra homomorphisms correspond faithfully to morphisms in the underlying category C\ca{C}.

Hence, given an isomorphism (A0,Am)β‰…(X0,Xm)(A_0, A_m) \cong (X_0, X_m) (let us call it ff) in CM\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 C\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 C\ca{C} to be univalent, this isomorphism can be made into a path A0≑X0A_0 \equiv X_0. This covers a third of the task: We must now show first that the algebra structures AmA_m and XmX_m are identified over A₀≑Xβ‚€, and we must prove that the resulting identification makes ff 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 AmA_m’s multiplication to that of XmX_m’s; Using the corresponding lemma for paths in hom-spaces of univalent categories, we can get away with (still calling our isomorphism ff) showing the square below commutes.

Since we have assumed that ff is an MM-algebra isomorphism, we can simultaneously turn the square above into one which has ff and fβˆ’1f^{-1} in adjacent faces and swap AmA_m for XmX_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 C\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 CM\ca{C}^M is univalent, we must show that the identification we’ve built trivialises the isomorphism Aβ‰…XA \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 _)))