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 2 }
           ; 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↩