open import Algebra.Monoid.Category
open import Algebra.Semigroup
open import Algebra.Monoid renaming (idr to mon-idr; idl to mon-idl)
open import Algebra.Magma

open import Cat.Monoidal.Instances.Cartesian
open import Cat.Displayed.Univalence.Thin
open import Cat.Functor.Hom.Representable
open import Cat.Functor.FullSubcategory
open import Cat.Diagram.Product.Solver
open import Cat.Functor.Equivalence
open import Cat.Functor.Properties
open import Cat.Instances.Functor
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Displayed.Total
open import Cat.Instances.Sets
open import Cat.Functor.Base
open import Cat.Functor.Hom
open import Cat.Prelude

import Cat.Reasoning

module Cat.Monoidal.Diagram.Monoid.Representable where

-- Under the module header to prevent sorting from ruining the import list
open import Cat.Monoidal.Diagram.Monoid
  renaming (Monoid-on to Monoid-ob;
            is-monoid-hom to internal-monoid-hom)

module _
  {o ℓ} {C : Precategory o ℓ}
  (prod : has-products C)
  (term : Terminal C)
  where

  open Cat.Reasoning C
  open Binary-products C prod
  open Terminal term
  open Monoid-ob
  open internal-monoid-hom
  open Monoid-hom
  open Functor
  open _=>_
  open Total-hom
  open Representation

Externalising monoids as presheaves🔗

Let $\mathcal{C}$ be a Cartesian monoidal category, and consider a monoid object $(M,\eta ,\mu )$ in it. Our first observation is that, despite the definition of monoid object only referring to (the monoidal structure on $\mathcal{C}\text{)}$ and the object $M\text{,}$ each set of generalised elements $X\to M$ also carries the structure of a monoid. The unit element is given by

and the multiplication map is given by

  private
    C-Monoid : Ob → Type ℓ
    C-Monoid m = Monoid-ob (Cartesian-monoidal prod term) m

    C-Monoid-hom : ∀ {m n} → Hom m n → C-Monoid m → C-Monoid n → Type ℓ
    C-Monoid-hom f m-mon n-mon =
      internal-monoid-hom (Cartesian-monoidal prod term) f m-mon n-mon

  Mon→Hom-mon : ∀ {m} (x : Ob) → C-Monoid m → Monoid-on (Hom x m)
  Mon→Hom-mon {m} x mon = hom-mon where
    has-semigroup : is-semigroup λ f g → mon .μ ∘ ⟨ f , g ⟩
    hom-mon : Monoid-on (Hom x m)

    hom-mon .Monoid-on.identity = mon .η ∘ !
    hom-mon .Monoid-on._⋆_ f g  = mon .μ ∘ ⟨ f , g ⟩

    hom-mon .Monoid-on.has-is-monoid .has-is-semigroup = has-semigroup
    hom-mon .Monoid-on.has-is-monoid .mon-idl {f} =
      mon .μ ∘ ⟨ mon .η ∘ ! , f ⟩         ≡⟨ products! C prod ⟩≡
      mon .μ ∘ (mon .η ⊗₁ id) ∘ ⟨ ! , f ⟩ ≡⟨ pulll (mon .μ-unitl) ⟩≡
      π₂ ∘ ⟨ ! , f ⟩                      ≡⟨ π₂∘⟨⟩ ⟩≡
      f                                   ∎
    hom-mon .Monoid-on.has-is-monoid .mon-idr {f} =
      mon .μ ∘ ⟨ f , mon .η ∘ ! ⟩         ≡⟨ products! C prod ⟩≡
      mon .μ ∘ (id ⊗₁ mon .η) ∘ ⟨ f , ! ⟩ ≡⟨ pulll (mon .μ-unitr) ⟩≡
      π₁ ∘ ⟨ f , ! ⟩                      ≡⟨ π₁∘⟨⟩ ⟩≡
      f                                   ∎

    has-semigroup .has-is-magma .has-is-set = Hom-set _ _
    has-semigroup .associative {f} {g} {h} =
      mon .μ ∘ ⟨ f , mon .μ ∘ ⟨ g , h ⟩ ⟩                                            ≡⟨ products! C prod ⟩≡
      mon .μ ∘ (id ⊗₁ mon .μ) ∘ ⟨ f , ⟨ g , h ⟩ ⟩                                    ≡⟨ extendl (mon .μ-assoc) ⟩≡
      mon .μ ∘ ((mon .μ ⊗₁ id) ∘ ⟨ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩) ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≡⟨ products! C prod ⟩≡
      mon .μ ∘ ⟨ mon .μ ∘ ⟨ f , g ⟩ , h ⟩                                            ∎

Thinking in terms of $M\text{’s}$ internal language, where we think of the $\mathbf{Hom}\text{-set}$ $X\to M$ as being the set of “$M\text{-elements}$ in context $X$”, our observation means that $M$ is a monoid in any context. Under this interpretation, pre-composition with a map $f:X\to Y$ corresponds to the substitution operation, mapping terms from the context $Y$ to $X\text{.}$

Following this line of thinking, the next thing to interrogate is whether the monoid operations on terms $Y\to M$ is preserved by substitution: is precomposition with $f$ a monoid homomorphism? The answer is yes!

  precompose-hom-mon-hom
    : ∀ {x y m} {mon : C-Monoid m}
    → (f : Hom x y)
    → Monoid-hom (Mon→Hom-mon y mon) (Mon→Hom-mon x mon) (_∘ f)
  precompose-hom-mon-hom {mon = mon} f .pres-id =
    (mon .η ∘ !) ∘ f ≡⟨ pullr (sym (!-unique (! ∘ f))) ⟩≡
    mon .η ∘ !       ∎
  precompose-hom-mon-hom {mon = mon} f .pres-⋆ g h =
    (mon .μ ∘ ⟨ g , h ⟩) ∘ f   ≡⟨ pullr (⟨⟩∘ f) ⟩≡
    mon .μ ∘ ⟨ g ∘ f , h ∘ f ⟩ ∎

We’ve almost shown that a monoid object $M:\mathcal{C}$ fits into a presheaf of monoids, a functor ${\mathcal{C}}^{\mathrm{op}}\to \mathbf{Mon}\text{,}$ mapping objects of $\mathcal{C}$ to the monoid of generalised elements $X\to M\text{.}$ All that remains is to show functoriality, which follows immediately:

  Mon→PshMon
    : ∀ {m} → C-Monoid m
    → Functor (C ^op) (Monoids ℓ)
  Mon→PshMon {m} mon .F₀ x .fst = el! (Hom x m)
  Mon→PshMon {m} mon .F₀ x .snd = Mon→Hom-mon x mon

  Mon→PshMon {m} mon .F₁ f .hom       = _∘ f
  Mon→PshMon {m} mon .F₁ f .preserves = precompose-hom-mon-hom {mon = mon} f

  Mon→PshMon {m} mon .F-id    = ext idr
  Mon→PshMon {m} mon .F-∘ f g = ext λ h → assoc h g f

And, since this presheaf is by definition given by the set of maps into an object, it’s representable!

  Mon→PshMon-rep
    : ∀ {m} → (mon : C-Monoid m)
    → Representation {C = C} (Mon↪Sets F∘ Mon→PshMon mon)
  Mon→PshMon-rep {m = m} mon .rep = m
  Mon→PshMon-rep {m = m} mon .represents = to-natural-iso ni where
    open make-natural-iso

    ni : make-natural-iso (Mon↪Sets F∘ Mon→PshMon mon) (Hom-into C m)
    ni .eta _ f   = f
    ni .inv _ f   = f
    ni .eta∘inv _ = refl
    ni .inv∘eta _ = refl
    ni .natural _ _ _ = refl

Now, suppose we have a pair of monoid objects, $M$ and $N\text{,}$ together with a homomorphism $f:M\to N\text{.}$ We can now consider the postcomposition with $f\text{,}$ a function of sets which maps between the relativizations of $M$ and $N$ to arbitrary contexts: it has type

Since we’ve equipped these sets with monoid structures using the internal structures on $M$ and $N\text{,}$ and $f$ is a homomorphism between those, we would like for postcomposition with $f$ to also be a monoid homomorphism…. which it is!

  internal-mon-hom→hom-mon-hom
    : ∀ {x m n} {f : Hom m n} {m-mon : C-Monoid m} {n-mon : C-Monoid n}
    → C-Monoid-hom f m-mon n-mon
    → Monoid-hom (Mon→Hom-mon x m-mon) (Mon→Hom-mon x n-mon) (f ∘_)
  internal-mon-hom→hom-mon-hom {f = f} {m-mon} {n-mon} hom .pres-id =
    f ∘ m-mon .η ∘ ! ≡⟨ pulll (hom .pres-η) ⟩≡
    n-mon .η ∘ !     ∎
  internal-mon-hom→hom-mon-hom {f = f} {m-mon} {n-mon} hom .pres-⋆ g h =
    f ∘ m-mon .μ ∘ ⟨ g , h ⟩       ≡⟨ extendl (hom .pres-μ) ⟩≡
    n-mon .μ ∘ f ⊗₁ f ∘ ⟨ g , h ⟩  ≡⟨ products! C prod ⟩≡
    n-mon .μ ∘ ⟨ f ∘ g , f ∘ h ⟩   ∎

To recap, these are the facts:

• A monoid object $M$ externalises to a family of $\mathbf{Sets}\text{-monoids}$ $\mathbf{Hom}(X,M)\text{,}$ where $X:\mathcal{C}$ is an arbitrary object we affectionately refer to as the “context”.

• Maps $f:X\to Y$ act by precomposition, which, extending the analogy, corresponds to substitution. Substitution along arbitrary maps is a monoid homomorphism, so $よ(M)$ extends to a functor ${\mathcal{C}}^{\mathrm{op}}\to \mathbf{Mon}\text{,}$ a representable presheaf of monoids;

• Monoid homomorphisms $f:M\to N\text{,}$ when acting by postcomposition, externalise to $\mathbf{Sets}\text{-monoid}$ homomorphisms $\mathbf{Hom}(X,M)\to \mathbf{Hom}(X,N)\text{.}$

  private
    Mon[C] : Precategory (o ⊔ ℓ) (ℓ ⊔ ℓ)
    Mon[C] = ∫ Mon[ Cartesian-monoidal prod term ]

  PShMon : ∀ κ → Precategory (o ⊔ ℓ ⊔ lsuc κ) (o ⊔ ℓ ⊔ κ)
  PShMon κ = Cat[ C ^op , Monoids κ ]

  RepPShMon : Precategory (o ⊔ lsuc ℓ) (o ⊔ ℓ)
  RepPShMon = Restrict {C = PShMon ℓ} (λ P → Representation {C = C} (Mon↪Sets F∘ P))

To make this correspondence formal, we’ll define the category of representable presheaves of monoids to be the full subcategory of ${\mathcal{C}}^{\mathrm{op}}\to \mathbf{Mon}$ on the representable objects; for now, it will be denoted $\mathrm{PSh}(\mathcal{C}{)}_M$ — a notation for which the author apologises. As usual, ${\mathbf{Mon}}_{\mathcal{C}}$ will denote the category of monoid objects on $\mathcal{C}\text{.}$

We have described most of a functor ${\mathbf{Mon}}_{\mathcal{C}}\to \mathrm{PSh}(\mathcal{C}{)}_M\text{.}$ It only remains to verify that the action by postcomposition of a monoid homomorphism $f:M\to N$ is a natural transformation $\mathbf{Hom}(-,M)\to \mathbf{Hom}(-,N)\text{.}$

  Mon→RepPShMon : Functor Mon[C] RepPShMon
  Mon→RepPShMon .F₀ (m , mon) .object  = Mon→PshMon mon
  Mon→RepPShMon .F₀ (m , mon) .witness = Mon→PshMon-rep mon

  Mon→RepPShMon .F₁ f .η x .hom = f .hom ∘_
  Mon→RepPShMon .F₁ f .η x .preserves =
    internal-mon-hom→hom-mon-hom (f .preserves)
  Mon→RepPShMon .F₁ f .is-natural x y g = ext λ h → assoc (f .hom) h g

  Mon→RepPShMon .F-id = ext λ x f → idl f
  Mon→RepPShMon .F-∘ f g = ext λ x h → sym (assoc (f .hom) (g .hom) h)

This functor is a simultaneous restriction and corestriction of the Yoneda embedding on $\mathcal{C}\text{.}$ After calculating that natural transformations between representable presheaves of monoids determine monoid homomorphisms¹, the usual argument will suffice to show that this functor is also fully faithful.

  Nat→internal-mon-hom
    : ∀ {m n} {m-mon : C-Monoid m} {n-mon : C-Monoid n}
    → (α : Mon→PshMon m-mon => Mon→PshMon n-mon)
    → C-Monoid-hom (α .η m # id) m-mon n-mon
  Nat→internal-mon-hom {m} {n} {m-mon} {n-mon} α .pres-η =
    (α .η m # id) ∘ (m-mon .η) ≡˘⟨ ap hom (α .is-natural _ _ _) $ₚ _ ⟩≡˘
    α .η top # (id ∘ m-mon .η) ≡⟨ ap (α .η _ #_) (id-comm-sym ∙ ap (m-mon .η ∘_) (sym (!-unique _))) ⟩≡
    α .η top # (m-mon .η ∘ !)  ≡⟨ α .η _ .preserves .pres-id ⟩≡
    n-mon .η ∘ !               ≡⟨ elimr (!-unique _) ⟩≡
    n-mon .η                   ∎
  Nat→internal-mon-hom {m} {n} {m-mon} {n-mon} α .pres-μ =
    α .η m # id ∘ (m-mon .μ)                               ≡˘⟨ ap hom (α .is-natural _ _ _) $ₚ _ ⟩≡˘
    α .η (m ⊗₀ m) # (id ∘ m-mon .μ)                        ≡⟨ ap (α .η _ #_) (id-comm-sym ∙ ap (m-mon .μ ∘_) (sym ⟨⟩-η)) ⟩≡
    α .η (m ⊗₀ m) # (m-mon .μ ∘ ⟨ π₁ , π₂ ⟩)               ≡⟨ α .η _ .preserves .pres-⋆ _ _ ⟩≡
    n-mon .μ ∘ ⟨ α .η _ # π₁ , α .η _ # π₂ ⟩               ≡˘⟨ ap (n-mon .μ ∘_) (ap₂ ⟨_,_⟩ (ap (α .η _ #_) (idl _)) (ap (α .η _ #_) (idl _))) ⟩≡˘
    n-mon .μ ∘ ⟨ α .η _ # (id ∘ π₁) , α .η _ # (id ∘ π₂) ⟩ ≡⟨ ap (n-mon .μ ∘_) (ap₂ ⟨_,_⟩ (ap hom (α .is-natural _ _ _) $ₚ _) (ap hom (α .is-natural _ _ _) $ₚ _)) ⟩≡
    n-mon .μ ∘ (α .η m # id ⊗₁ α .η m # id)                ∎

  open is-iso

  Mon→RepPShMon-is-ff : is-fully-faithful Mon→RepPShMon
  Mon→RepPShMon-is-ff = is-iso→is-equiv λ where
    .inv α .hom       → α .η _ # id
    .inv α .preserves → Nat→internal-mon-hom α
    .rinv α → ext λ _ f →
      α .η _ # id ∘ f   ≡˘⟨ ap hom (α .is-natural _ _ _) $ₚ _ ⟩≡˘
      α .η _ # (id ∘ f) ≡⟨ ap (α .η _ #_) (idl f) ⟩≡
      α .η _ # f        ∎
    .linv h → total-hom-path _ (idr _) prop!

Internalizing presheaves of monoids🔗

Intuitively, what we have just shown is that monoids internal to $\mathcal{C}$ yield monoids in the internal language of $\mathcal{C}$ — giving monoids in arbitrary contexts, in a manner compatible with substitution. We will now establish the converse: If $\mathbf{Hom}(-,M)$ is always a monoid, then $M$ is a monoid object, as long as the monoid structures are stable under substitution — dropping the analogy, as long as the monoid structure is natural.

  module _ {m : Ob} (mon : ∀ x → Monoid-on (Hom x m)) where
    private module mon {x} = Monoid-on (mon x)
    open mon using (identity; _⋆_)

    Hom-mon→Mon
      : (∀ {x y} (f : Hom x y) → identity ∘ f ≡ identity)
      → (∀ {x y} (f g : Hom y m) (h : Hom x y) → (f ⋆ g) ∘ h ≡ f ∘ h ⋆ g ∘ h)
      → C-Monoid m

The monoid operations are defined in the smallest context possible. For identity this is the empty context², for multiplication, this is the context $M\times M\text{.}$

    Hom-mon→Mon id-nat ⋆-nat .η = identity {top}
    Hom-mon→Mon id-nat ⋆-nat .μ = π₁ ⋆ π₂

To establish the monoid laws, we’ll use the naturality conditions we imposed on the monoids $\mathbf{Hom}(-,M)\text{.}$

    Hom-mon→Mon id-nat ⋆-nat .μ-unitl =
      (π₁ ⋆ π₂) ∘ (identity ⊗₁ id)                    ≡⟨ ⋆-nat _ _ _ ⟩≡
      (π₁ ∘ identity ⊗₁ id) ⋆ (π₂ ∘ identity ⊗₁ id)   ≡⟨ ap₂ _⋆_ π₁∘⟨⟩ π₂∘⟨⟩ ⟩≡
      (identity ∘ π₁) ⋆ (id ∘ π₂)                     ≡⟨ ap₂ _⋆_ (id-nat _) (idl _) ⟩≡
      identity ⋆ π₂                                   ≡⟨ mon.idl ⟩≡
      π₂                                              ∎

    Hom-mon→Mon id-nat ⋆-nat .μ-unitr =
      (π₁ ⋆ π₂) ∘ (id ⊗₁ identity)                  ≡⟨ ⋆-nat _ _ _ ⟩≡
      (π₁ ∘ id ⊗₁ identity) ⋆ (π₂ ∘ id ⊗₁ identity) ≡⟨ ap₂ _⋆_ π₁∘⟨⟩ π₂∘⟨⟩ ⟩≡
      (id ∘ π₁) ⋆ (identity ∘ π₂)                   ≡⟨ ap₂ _⋆_ (idl _) (id-nat _) ⟩≡
      π₁ ⋆ identity                                 ≡⟨ mon.idr ⟩≡
      π₁                                            ∎

    Hom-mon→Mon id-nat ⋆-nat .μ-assoc =
      (π₁ ⋆ π₂) ∘ (id ⊗₁ (π₁ ⋆ π₂))                                  ≡⟨ ⋆-nat _ _ _ ⟩≡
      (π₁ ∘ id ⊗₁ (π₁ ⋆ π₂)) ⋆ (π₂ ∘ id ⊗₁ (π₁ ⋆ π₂))                ≡⟨ ap₂ _⋆_ π₁∘⟨⟩ π₂∘⟨⟩ ⟩≡
      (id ∘ π₁) ⋆ ((π₁ ⋆ π₂) ∘ π₂)                                   ≡⟨ ap₂ _⋆_ (idl _) (⋆-nat _ _ _) ⟩≡
      π₁ ⋆ ((π₁ ∘ π₂) ⋆ (π₂ ∘ π₂))                                   ≡⟨ mon.associative ⟩≡
      (π₁ ⋆ (π₁ ∘ π₂)) ⋆ (π₂ ∘ π₂)                                   ≡˘⟨ ap₂ _⋆_ (⋆-nat _ _ _ ∙ ap₂ _⋆_ π₁∘⟨⟩ π₂∘⟨⟩) (idl _) ⟩≡˘
      ((π₁ ⋆ π₂) ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩) ⋆ (id ∘ π₂ ∘ π₂)                ≡⟨ ap₂ _⋆_ (ap ((π₁ ⋆ π₂) ∘_) (sym π₁∘⟨⟩)) (ap (id ∘_) (sym π₂∘⟨⟩)) ⟩≡
      ((π₁ ⋆ π₂) ∘ π₁ ∘ _) ⋆ (id ∘ π₂ ∘ _)                           ≡⟨ ap₂ _⋆_ (extendl (sym π₁∘⟨⟩)) (extendl (sym π₂∘⟨⟩)) ⟩≡
      (π₁ ∘ _) ⋆ (π₂ ∘ _)                                            ≡˘⟨ ⋆-nat _ _ _ ⟩≡˘
      (π₁ ⋆ π₂) ∘ ((π₁ ⋆ π₂) ⊗₁ id) ∘ ⟨ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩ ∎

We will use this construction to construct the inverse of our externalisation functor. If we have a representable presheaf of monoids $P\text{,}$ then, by definition, we have substitution-stable monoid structures on $P(-)\text{,}$ and natural isomorphisms $P(-)\cong \mathbf{Hom}(-,M)\text{,}$ for some object $M:\mathcal{C}\text{.}$

  RepPshMon→Mon
    : ∀ (P : Functor (C ^op) (Monoids ℓ))
    → (P-rep : Representation {C = C} (Mon↪Sets F∘ P))
    → C-Monoid (P-rep .rep)
  RepPshMon→Mon P P-rep = Hom-mon→Mon hom-mon η*-nat μ*-nat
    module RepPshMon→Mon where

    m : Ob
    m = P-rep .rep

    PMon : Ob → Type ℓ
    PMon x = ∣ P .F₀ x .fst ∣

    module PMon {x} = Monoid-on (P .F₀ x .snd)
    module repr = Isoⁿ (P-rep .represents)

    open PMon hiding (idl; idr; associative)

    gen : ∀ {x} → PMon x → Hom x m
    gen {x} px = repr.to .η x px

    elt : ∀ {x} → Hom x m → PMon x
    elt {x} f = repr.from .η x f

As noted, the representability condition means we have specified isomorphisms between the sets $P(x)$ — the sections of $P$ — and generalised objects $x\to M\text{,}$ where $M$ is the representing object. It follows, even if this isomorphism is not natural, that we can transfer the monoid structure $P(x)$ to a monoid structure on $x\to M\text{.}$

    η* : ∀ x → Hom x m
    η* x = gen identity

    μ* : ∀ {x} → Hom x m → Hom x m → Hom x m
    μ* {x = x} f g = gen $ (elt f) ⋆ (elt g)

    η*-idl : ∀ {x} → (f : Hom x m) → μ* (η* x) f ≡ f
    η*-idl {x} f =
      gen (⌜ elt (gen identity) ⌝ ⋆ elt f) ≡⟨ ap! (unext repr.invr _ _) ⟩≡
      gen (identity ⋆ elt f)               ≡⟨ ap gen PMon.idl ⟩≡
      gen (elt f)                          ≡⟨ unext repr.invl _ _ ⟩≡
      f                                    ∎

    η*-idr : ∀ {x} → (f : Hom x m) → μ* f (η* x) ≡ f
    η*-idr {x} f =
      gen (elt f ⋆ ⌜ elt (gen identity) ⌝) ≡⟨ ap! (unext repr.invr _ _) ⟩≡
      gen (elt f ⋆ identity)               ≡⟨ ap gen PMon.idr ⟩≡
      gen (elt f)                          ≡⟨ unext repr.invl _ _ ⟩≡
      f                                    ∎

    μ*-assoc : ∀ {x} → (f g h : Hom x m) → μ* f (μ* g h) ≡ μ* (μ* f g) h
    μ*-assoc {x} f g h =
      gen (elt f ⋆ ⌜ elt (gen (elt g ⋆ elt h)) ⌝) ≡⟨ ap! (unext repr.invr _ _) ⟩≡
      gen (elt f ⋆ (elt g ⋆ elt h))               ≡⟨ ap gen PMon.associative ⟩≡
      gen (⌜ elt f ⋆ elt g ⌝ ⋆ elt h)             ≡⟨ ap! (sym $ unext repr.invr _ _) ⟩≡
      gen (elt (gen (elt f ⋆ elt g)) ⋆ elt h)     ∎

    hom-mon : ∀ x → Monoid-on (Hom x m)
    hom-mon x .Monoid-on.identity = η* x
    hom-mon x .Monoid-on._⋆_ = μ*
    hom-mon x .Monoid-on.has-is-monoid .has-is-semigroup .has-is-magma .has-is-set =
      Hom-set x m
    hom-mon x .Monoid-on.has-is-monoid .has-is-semigroup .associative = μ*-assoc _ _ _
    hom-mon x .Monoid-on.has-is-monoid .mon-idl = η*-idl _
    hom-mon x .Monoid-on.has-is-monoid .mon-idr = η*-idr _

It remains to show that this assignment is natural — which is why we asked for a natural isomorphism! A calculation mildly annoying establishes the stability of identity and multiplication under substitution.

    η*-nat
      : ∀ {w x} (f : Hom w x)
      → η* x ∘ f ≡ η* w
    η*-nat {w} {x} f =
      (η* x) ∘ f                  ≡˘⟨ repr.to .is-natural _ _ _ $ₚ _ ⟩≡˘
      gen (P .F₁ f .hom identity) ≡⟨ ap gen (P .F₁ f .preserves .pres-id) ⟩≡
      η* w ∎

    μ*-nat
      : ∀ {w x} (f g : Hom x m) (h : Hom w x)
      → μ* f g ∘ h ≡ μ* (f ∘ h) (g ∘ h)
    μ*-nat f g h =
      μ* f g ∘ h                                            ≡˘⟨ repr.to .is-natural _ _ _ $ₚ _ ⟩≡˘
      gen (P .F₁ h .hom ((elt f) ⋆ (elt g)))                ≡⟨ ap gen (P .F₁ h .preserves .pres-⋆ _ _) ⟩≡
      gen ((P .F₁ h .hom (elt f)) ⋆ (P .F₁ h .hom (elt g))) ≡˘⟨ ap gen (ap₂ _⋆_ (repr.from .is-natural _ _ _ $ₚ _) (repr.from .is-natural _ _ _ $ₚ _)) ⟩≡˘
      μ* (f ∘ h) (g ∘ h) ∎

We now have a construction mapping representable presheaves to monoid objects. The last bit of algebra in this module establishes that internalisation followed by externalisation produces a presheaf of monoids isomorphic to the one we started with.

  Mon→RepPShMon-is-split-eso : is-split-eso Mon→RepPShMon
  Mon→RepPShMon-is-split-eso P .fst =
    P .witness .rep , RepPshMon→Mon (P .object) (P .witness)
  Mon→RepPShMon-is-split-eso P .snd = super-iso→sub-iso _ $ to-natural-iso ni where
    open make-natural-iso
    open RepPshMon→Mon (P .object) (P .witness)
    open PMon using (identity; _⋆_)
    module P = Functor (P .object)

    ni : make-natural-iso (Mon→PshMon (RepPshMon→Mon (P .object) (P .witness))) (P .object)
    ni .eta x .hom = repr.from .η x
    ni .inv x .hom = repr.to .η x

    ni .eta x .preserves .pres-id =
      elt (η* top ∘ !)           ≡⟨ ap elt (η*-nat !) ⟩≡
      elt (η* x)                 ≡⟨ unext repr.invr _ _ ⟩≡
      identity                   ∎
    ni .eta x .preserves .pres-⋆ f g =
      elt (μ* π₁ π₂ ∘ ⟨ f , g ⟩)                 ≡⟨ ap elt (μ*-nat _ _ _) ⟩≡
      elt (μ* (π₁ ∘ ⟨ f , g ⟩) (π₂ ∘ ⟨ f , g ⟩)) ≡⟨ ap elt (ap₂ μ* π₁∘⟨⟩ π₂∘⟨⟩) ⟩≡
      elt (μ* f g)                               ≡⟨ unext repr.invr _ _ ⟩≡
      (elt f ⋆ elt g)                            ∎

    ni .inv x .preserves .pres-id = sym (η*-nat _)
    ni .inv x .preserves .pres-⋆ f g =
      gen (f ⋆ g)                                          ≡˘⟨ ap gen (ap₂ _⋆_ (unext repr.invr _ _) (unext repr.invr _ _)) ⟩≡˘
      μ* (gen f) (gen g)                                   ≡˘⟨ ap₂ μ* π₁∘⟨⟩ π₂∘⟨⟩ ⟩≡˘
      μ* (π₁ ∘ ⟨ gen f , gen g ⟩) (π₂ ∘ ⟨ gen f , gen g ⟩) ≡˘⟨ μ*-nat _ _ _ ⟩≡˘
      μ* π₁ π₂ ∘ ⟨ gen f , gen g ⟩                         ∎

    ni .eta∘inv x = ext (unext repr.invr x)
    ni .inv∘eta x = ext (unext repr.invl x)
    ni .natural x y f = ext (sym (repr.from .is-natural _ _ _) $ₚ_)

Put another way, our functor ${\mathbf{Mon}}_{\mathcal{C}}\to \mathrm{PSh}(\mathcal{C}{)}_M$ is a split essential surjection — so, remembering that it was fully faithful, we conclude it’s an equivalence.

  Mon→RepPShMon-is-equiv : is-equivalence Mon→RepPShMon
  Mon→RepPShMon-is-equiv = ff+split-eso→is-equivalence
    Mon→RepPShMon-is-ff
    Mon→RepPShMon-is-split-eso

The big picture🔗

It’s easy to lose the forest for the trees here, so let’s take a step back and examine what we have done. This equivalence of categories shows that monoids in the internal language of $\mathcal{C}$ are really monoids in $\mathcal{C}\text{.}$ Furthermore, nothing we have done relies on the structure of monoids; we could repeat the same argument with internal groups and everything would go through smoothly.

The lesson is that category theorists prefer to define internal structure in the smallest context possible, and then rely on weakening to obtain a well-behaved object in the internal language. This works, but is somewhat unnatural, and can summon pullback nasal demons that will ruin your day. For instance, defining internal categories in this manner requires taking pullbacks to ensure that the composition operation is well formed, which spirals out of control when quantifying over multiple morphisms due to coherence issues. If we take this generalized object perspective instead, such coherence issues can be avoided!