module Cat.Monoidal.Diagram.Monoid where

Monoids in a monoidal categoryπŸ”—

Let 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 , generally just called a β€œmonoid in ”, is really a collection of diagrams in centered around an object the monoid itself.

In addition to the object, we also require a β€œunit” map and β€œmultiplication” map Moreover, these maps should be compatible with the unitors and associator of the underlying monoidal category:

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

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

If we think of as a bicategory with a single object β€” that is, we deloop it β€”, then a monoid in is given by precisely the same data as a monad in 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 can be made into a category, much like the monoids in the category of sets. In fact, we shall see later that when is equipped with its Cartesian monoidal structure, Rather than defining directly as a category, we instead define it as a category displayed over 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 expressing the condition of being a monoid homomorphism. This is the familiar condition from algebra, but expressed in a point-free way:

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

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

    field
      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 = hlevel 2

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 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 = prop!
  Mon[_] .idl' f = prop!
  Mon[_] .assoc' f g h = 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) 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'} = biimp-is-equiv! (Ξ» z β†’ F₁' F z) invs where
    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-⋆ _ _

Monoidal functors preserve monoidsπŸ”—

If is a lax monoidal functor between monoidal categories and and is a monoid in then can be equipped with the structure of a monoid in

We can phrase this nicely as a displayed functor over

  Mon₁[_] : Displayed-functor Mon[ MC ] Mon[ MD ] F
  Mon₁[_] .Fβ‚€' m .Ξ· = F₁ (m .Ξ·) ∘ Ξ΅
  Mon₁[_] .Fβ‚€' m .ΞΌ = F₁ (m .ΞΌ) ∘ Ο†

The unit laws are witnessed by the commutativity of this diagram:

  Mon₁[_] .Fβ‚€' m .ΞΌ-unitl =
    (F₁ (m .ΞΌ) ∘ Ο†) ∘ ((F₁ (m .Ξ·) ∘ Ξ΅) βŠ—β‚ id)          β‰‘βŸ¨ pullr (refl⟩∘⟨ βŠ—.expand (refl ,β‚š F.introl refl)) βŸ©β‰‘
    F₁ (m .ΞΌ) ∘ Ο† ∘ (F₁ (m .Ξ·) βŠ—β‚ F₁ C.id) ∘ (Ξ΅ βŠ—β‚ id) β‰‘βŸ¨ refl⟩∘⟨ extendl (Ο†.is-natural _ _ _) βŸ©β‰‘
    F₁ (m .ΞΌ) ∘ F₁ (m .Ξ· C.βŠ—β‚ C.id) ∘ Ο† ∘ (Ξ΅ βŠ—β‚ id)    β‰‘βŸ¨ F.pulll (m .ΞΌ-unitl) βŸ©β‰‘
    F₁ C.λ← ∘ Ο† ∘ (Ξ΅ βŠ—β‚ id)                            β‰‘βŸ¨ F-λ← βŸ©β‰‘
    λ←                                                 ∎
  Mon₁[_] .Fβ‚€' m .ΞΌ-unitr =
    (F₁ (m .ΞΌ) ∘ Ο†) ∘ (id βŠ—β‚ (F₁ (m .Ξ·) ∘ Ξ΅))          β‰‘βŸ¨ pullr (refl⟩∘⟨ βŠ—.expand (F.introl refl ,β‚š refl)) βŸ©β‰‘
    F₁ (m .ΞΌ) ∘ Ο† ∘ (F₁ C.id βŠ—β‚ F₁ (m .Ξ·)) ∘ (id βŠ—β‚ Ξ΅) β‰‘βŸ¨ refl⟩∘⟨ extendl (Ο†.is-natural _ _ _) βŸ©β‰‘
    F₁ (m .ΞΌ) ∘ F₁ (C.id C.βŠ—β‚ m .Ξ·) ∘ Ο† ∘ (id βŠ—β‚ Ξ΅)    β‰‘βŸ¨ F.pulll (m .ΞΌ-unitr) βŸ©β‰‘
    F₁ C.ρ← ∘ Ο† ∘ (id βŠ—β‚ Ξ΅)                            β‰‘βŸ¨ F-ρ← βŸ©β‰‘
    ρ←                                                 ∎

… and the associativity by this one.

  Mon₁[_] .Fβ‚€' m .ΞΌ-assoc =
    (F₁ (m .ΞΌ) ∘ Ο†) ∘ (id βŠ—β‚ (F₁ (m .ΞΌ) ∘ Ο†))                       β‰‘βŸ¨ pullr (refl⟩∘⟨ βŠ—.expand (F.introl refl ,β‚š refl)) βŸ©β‰‘
    F₁ (m .ΞΌ) ∘ Ο† ∘ (F₁ C.id βŠ—β‚ F₁ (m .ΞΌ)) ∘ (id βŠ—β‚ Ο†)              β‰‘βŸ¨ (refl⟩∘⟨ extendl (Ο†.is-natural _ _ _)) βŸ©β‰‘
    F₁ (m .ΞΌ) ∘ F₁ (C.id C.βŠ—β‚ m .ΞΌ) ∘ Ο† ∘ (id βŠ—β‚ Ο†)                 β‰‘βŸ¨ F.pulll (m .ΞΌ-assoc) βŸ©β‰‘
    F₁ (m .ΞΌ C.∘ (m .ΞΌ C.βŠ—β‚ C.id) C.∘ C.α← _ _ _) ∘ Ο† ∘ (id βŠ—β‚ Ο†)   β‰‘βŸ¨ F.popr (F.popr F-α←) βŸ©β‰‘
    F₁ (m .ΞΌ) ∘ F₁ (m .ΞΌ C.βŠ—β‚ C.id) ∘ Ο† ∘ (Ο† βŠ—β‚ id) ∘ α← _ _ _      β‰‘Λ˜βŸ¨ pullr (extendl (Ο†.is-natural _ _ _)) βŸ©β‰‘Λ˜
    (F₁ (m .ΞΌ) ∘ Ο†) ∘ (F₁ (m .ΞΌ) βŠ—β‚ F₁ C.id) ∘ (Ο† βŠ—β‚ id) ∘ α← _ _ _ β‰‘βŸ¨ refl⟩∘⟨ βŠ—.pulll (refl ,β‚š F.eliml refl) βŸ©β‰‘
    (F₁ (m .ΞΌ) ∘ Ο†) ∘ ((F₁ (m .ΞΌ) ∘ Ο†) βŠ—β‚ id) ∘ α← _ _ _            ∎

Functoriality for means that, given a monoid homomorphism the map is a monoid homomorphism between the induced monoids on and

  Mon₁[_] .F₁' h .pres-Ξ· = F.pulll (h .pres-Ξ·)
  Mon₁[_] .F₁' h .pres-ΞΌ = F.extendl (h .pres-ΞΌ) βˆ™ pushr (sym (Ο†.is-natural _ _ _))
  Mon₁[_] .F-id' = prop!
  Mon₁[_] .F-∘' = prop!

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