module Cat.Monoidal.Diagram.Monoid where

Monoids in a monoidal categoryπŸ”—

Let (C,βŠ—,1)(\mathcal{C}, \otimes, 1) be a monoidal category you want to study. It can be, for instance, one of the endomorphism categories in a bicategory that you like. A monoid object in C\mathcal{C}, generally just called a β€œmonoid in C\mathcal{C}”, is really a collection of diagrams in C\mathcal{C} centered around an object MM, the monoid itself.

In addition to the object, we also require a β€œunit” map Ξ·:1β†’M\eta : 1 \to M and β€œmultiplication” map ΞΌ:MβŠ—Mβ†’M\mu : M \otimes M \to M. Moreover, these maps should be compatible with the unitors and associator of the underlying monoidal category:

  record Monoid-on (M : C.Ob) : Type β„“ where
      Ξ· : C.Hom C.Unit M
      ΞΌ : C.Hom (M C.βŠ— M) M

      ΞΌ-unitl : ΞΌ C.∘ (Ξ· C.βŠ—β‚ ≑ C.λ←
      ΞΌ-unitr : ΞΌ C.∘ ( C.βŠ—β‚ Ξ·) ≑ C.ρ←
      ΞΌ-assoc : ΞΌ C.∘ ( C.βŠ—β‚ ΞΌ) ≑ ΞΌ C.∘ (ΞΌ C.βŠ—β‚ C.∘ C.α← _ _ _

If we think of C\mathcal{C} as a bicategory with a single object βˆ—* β€” that is, we deloop it β€”, then a monoid in C\mathcal{C} is given by precisely the same data as a monad in BC\mathbf{B}\mathcal{C}, on the object βˆ—*.

  monad→monoid : (M : Monad BC tt) → Monoid-on (M .Monad.M)
  monad→monoid M = go where
    module M = Monad M
    go : Monoid-on M.M
    go .Ξ· = M.Ξ·
    go .ΞΌ = M.ΞΌ
    go .ΞΌ-unitl = M.ΞΌ-unitl
    go .ΞΌ-unitr = M.ΞΌ-unitr
    go .ΞΌ-assoc = M.ΞΌ-assoc

  monoidβ†’monad : βˆ€ {M} β†’ Monoid-on M β†’ Monad BC tt
  monoid→monad M = go where
    module M = Monoid-on M
    go : Monad BC tt
    go .Monad.M = _
    go .Monad.ΞΌ = M.ΞΌ
    go .Monad.Ξ· = M.Ξ·
    go .Monad.ΞΌ-assoc = M.ΞΌ-assoc
    go .Monad.ΞΌ-unitr = M.ΞΌ-unitr
    go .Monad.ΞΌ-unitl = M.ΞΌ-unitl

Put another way, a monad is just a monoid in the category of endofunctors endo-1-cells, what’s the problem?

The category Mon(C)πŸ”—

The monoid objects in C\mathcal{C} can be made into a category, much like the monoids in the category of sets. In fact, we shall see later that when Sets\mathbf{Sets} is equipped with its Cartesian monoidal structure, Mon(Sets)β‰…Mon\mathrm{Mon}(\mathbf{Sets}) \cong \mathrm{Mon}. Rather than defining Mon(C)\mathrm{Mon}(\mathcal{C}) directly as a category, we instead define it as a category Mon(C)C\mathrm{Mon}(\mathcal{C}) \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{C} displayed over C\mathcal{C}, which fits naturally with the way we have defined Monoid-object-on.

Therefore, rather than defining a type of monoid homomorphisms, we define a predicate on maps f:m→nf : m \to n expressing the condition of being a monoid homomorphism. This is the familiar condition from algebra, but expressed in a point-free way:

    is-monoid-hom {m n} (f : C.Hom m n)
     (mo : Monoid-on M m) (no : Monoid-on M n) : Type β„“ where

      module m = Monoid-on mo
      module n = Monoid-on no

      pres-Ξ· : f C.∘ m.Ξ· ≑ n.Ξ·
      pres-ΞΌ : f C.∘ m.ΞΌ ≑ n.ΞΌ C.∘ (f C.βŠ—β‚ f)

Since being a monoid homomorphism is a pair of propositions, the overall condition is a proposition as well. This means that we will not need to concern ourselves with proving displayed identity and associativity laws, a great simplification.

  Mon[_] : Displayed C β„“ β„“
  Mon[_] .Ob[_]  = Monoid-on M
  Mon[_] .Hom[_] = is-monoid-hom
  Mon[_] .Hom[_]-set f x y = is-prop→is-set is-monoid-hom-is-prop

The most complicated step of putting together the displayed category of monoid objects is proving that monoid homomorphisms are closed under composition. However, even in the point-free setting of an arbitrary category C\mathcal{C}, the reasoning isn’t that painful:

  Mon[ .id' ] .pres-Ξ· = C.idl _
  Mon[ .id' ] .pres-ΞΌ = C.idl _ βˆ™ C.intror (C.-βŠ—- .F-id)

  Mon[_] ._∘'_ fh gh .pres-Ξ· = C.pullr (gh .pres-Ξ·) βˆ™ fh .pres-Ξ·
  Mon[_] ._∘'_ {x = x} {y} {z} {f} {g} fh gh .pres-μ =
    (f C.∘ g) C.∘ x .Monoid-on.ΞΌ                β‰‘βŸ¨ C.pullr (gh .pres-ΞΌ) βŸ©β‰‘
    f C.∘ y .Monoid-on.ΞΌ C.∘ (g C.βŠ—β‚ g)         β‰‘βŸ¨ C.extendl (fh .pres-ΞΌ) βŸ©β‰‘
    Monoid-on.ΞΌ z C.∘ (f C.βŠ—β‚ f) C.∘ (g C.βŠ—β‚ g) β‰‘Λ˜βŸ¨ C.refl⟩∘⟨ C.-βŠ—- .F-∘ _ _ βŸ©β‰‘Λ˜
    Monoid-on.ΞΌ z C.∘ (f C.∘ g C.βŠ—β‚ f C.∘ g)    ∎

  Mon[_] .idr' f = is-prop→pathp (λ i → is-monoid-hom-is-prop) _ _
  Mon[_] .idl' f = is-prop→pathp (λ i → is-monoid-hom-is-prop) _ _
  Mon[_] .assoc' f g h = is-prop→pathp (λ i → is-monoid-hom-is-prop) _ _

Constructing this displayed category for the Cartesian monoidal structure on the category of sets, we find that it is but a few renamings away from the ordinary category of monoids-on-sets. The only thing out of the ordinary about the proof below is that we can establish the displayed categories themselves are identical, so it is a trivial step to show they induce identical1 total categories.

Mon[Sets]≑Mon : βˆ€ {β„“} β†’ Mon[ Setsβ‚“ ] ≑ Mon {β„“}
Mon[Sets]≑Mon {β„“} = Displayed-path F (Ξ» a β†’ is-isoβ†’is-equiv (fiso a)) ff where
  open Displayed-functor
  open Monoid-on
  open is-monoid-hom

  open Mon.Monoid-hom
  open Mon.Monoid-on

The construction proceeds in three steps: First, put together a functor (displayed over the identity) Mon(C)β†’Mon\mathrm{Mon}(\mathcal{C}) \to \mathbf{Mon}; Then, prove that its action on objects (β€œstep 2”) and action on morphisms (β€œstep 3”) are independently equivalences of types. The characterisation of paths of displayed categories will take care of turning this data into an identification.

  F : Displayed-functor Mon[ Setsβ‚“ ] Mon Id
  F .Fβ‚€' o .identity = o .Ξ· (lift tt)
  F .Fβ‚€' o ._⋆_ x y = o .ΞΌ (x , y)
  F .Fβ‚€' o .has-is-monoid .Mon.has-is-semigroup =
    record { has-is-magma = record { has-is-set = hlevel! }
           ; associative  = o .ΞΌ-assoc $β‚š _
  F .Fβ‚€' o .has-is-monoid .Mon.idl = o .ΞΌ-unitl $β‚š _
  F .Fβ‚€' o .has-is-monoid .Mon.idr = o .ΞΌ-unitr $β‚š _
  F .F₁' wit .pres-id = wit .pres-Ξ· $β‚š _
  F .F₁' wit .pres-⋆ x y = wit .pres-ΞΌ $β‚š _
  F .F-id' = prop!
  F .F-∘' = prop!

  open is-iso

  fiso : βˆ€ a β†’ is-iso (F .Fβ‚€' {a})
  fiso T .inv m .Ξ· _ = m .identity
  fiso T .inv m .ΞΌ (a , b) = m ._⋆_ a b
  fiso T .inv m .ΞΌ-unitl = funext Ξ» _ β†’ m .idl
  fiso T .inv m .ΞΌ-unitr = funext Ξ» _ β†’ m .idr
  fiso T .inv m .ΞΌ-assoc = funext Ξ» _ β†’ m .associative
  fiso T .rinv x = Mon.Monoid-structure _ .id-hom-unique
    (record { pres-id = refl ; pres-⋆ = Ξ» _ _ β†’ refl })
    (record { pres-id = refl ; pres-⋆ = Ξ» _ _ β†’ refl })
  fiso T .linv m = Monoid-pathp Setsβ‚“ refl refl

  ff : βˆ€ {a b : Set _} {f : ∣ a ∣ β†’ ∣ b ∣} {a' b'}
     β†’ is-equiv (F₁' F {a} {b} {f} {a'} {b'})
  ff {a} {b} {f} {a'} {b'} =
    prop-ext (is-monoid-hom-is-prop Setsβ‚“) (hlevel 1)
             (Ξ» z β†’ F₁' F z) invs .snd
      invs : Mon.Monoid-hom (F .Fβ‚€' a') (F .Fβ‚€' b') f
           β†’ is-monoid-hom Setsβ‚“ f a' b'
      invs m .pres-Ξ· = funext Ξ» _ β†’ m .pres-id
      invs m .pres-ΞΌ = funext Ξ» _ β†’ m .pres-⋆ _ _

  1. thus isomorphic, thus equivalentβ†©οΈŽ