module Cat.Monoidal.Diagram.Monoid.Representable where

Externalising monoids as presheaves🔗

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

X→!1→ηM, X \xrightarrow{!} 1 \xrightarrow{\eta} M\text{,}

and the multiplication map is given by

(X×X)→⟹f,g⟩(M×M)→ΌM. (X \times X) \xrightarrow{\langle f, g \rangle} (M \times M) \xrightarrow{\mu} M\text{.}

  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 ⟩
It’s not very hard to show that the monoid laws from the diagram “relativize” to each Hom\mathbf{Hom}-set.
    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 MM’s internal language, where we think of the Hom\mathbf{Hom}-set X→MX \to M as being the set of “MM-elements in context XX”, our observation means that MM is a monoid in any context. Under this interpretation, pre-composition with a map f:X→Yf : X \to Y corresponds to the substitution operation, mapping terms from the context YY to XX.

Following this line of thinking, the next thing to interrogate is whether the monoid operations on terms Y→MY \to M is preserved by substitution: is precomposition with ff 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:CM : \mathcal{C} fits into a presheaf of monoids, a functor Cop→Mon\mathcal{C}^{\mathrm{op}} \to \mathbf{Mon}, mapping objects of C\mathcal{C} to the monoid of generalised elements X→MX \to M. 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    = Homomorphism-path idr
  Mon→PshMon {m} mon .F-∘ f g = Homomorphism-path λ 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} (Forget 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 (Forget 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, MM and NN, together with a homomorphism f:M→Nf : M \to N. We can now consider the postcomposition with ff, a function of sets which maps between the relativizations of MM and NN to arbitrary contexts: it has type Hom(X,M)→Hom(X,N). \mathbf{Hom}(X, M) \to \mathbf{Hom}(X, N)\text{.} Since we’ve equipped these sets with monoid structures using the internal structures on MM and NN, and ff is a homomorphism between those, we would like for postcomposition with ff 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 MM externalises to a family of Sets\mathbf{Sets}-monoids Hom(X,M)\mathbf{Hom}(X, M), where X:CX : \mathcal{C} is an arbitrary object we affectionately refer to as the “context”.

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

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

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

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

  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 =
    Homomorphism-path λ h → assoc (f .hom) h g

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

This functor is a simultaneous restriction and corestriction of the Yoneda embedding on C\mathcal{C}. After calculating that natural transformations between representable presheaves of monoids determine monoid homomorphisms1, 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 .hom id) m-mon n-mon
  Nat→internal-mon-hom {m} {n} {m-mon} {n-mon} α .pres-η =
    (α .η m .hom id) ∘ (m-mon .η) ≡˘⟚ ap hom (α .is-natural _ _ _) $ₚ _ ⟩≡˘
    α .η top .hom (id ∘ m-mon .η) ≡⟚ ap (α .η _ .hom) (id-comm-sym ∙ ap (m-mon .η ∘_) (sym (!-unique _))) ⟩≡
    α .η top .hom (m-mon .η ∘ !)  ≡⟚ α .η _ .preserves .pres-id ⟩≡
    n-mon .η ∘ !                  ≡⟚ elimr (!-unique _) ⟩≡
    n-mon .η                      ∎
  Nat→internal-mon-hom {m} {n} {m-mon} {n-mon} α .pres-ÎŒ =
    α .η m .hom id ∘ (m-mon .ÎŒ)                                  ≡˘⟚ ap hom (α .is-natural _ _ _) $ₚ _ ⟩≡˘
    α .η (m ⊗₀ m) .hom (id ∘ m-mon .ÎŒ)                           ≡⟚ ap (α .η _ .hom) (id-comm-sym ∙ ap (m-mon .ÎŒ ∘_) (sym ⟚⟩-η)) ⟩≡
    α .η (m ⊗₀ m) .hom (m-mon .ÎŒ ∘ ⟹ π₁ , π₂ ⟩)                  ≡⟚ α .η _ .preserves .pres-⋆ _ _ ⟩≡
    n-mon .ÎŒ ∘ ⟹ α .η _ .hom π₁ , α .η _ .hom π₂ ⟩               ≡˘⟚ ap (n-mon .ÎŒ ∘_) (ap₂ ⟹_,_⟩ (ap (α .η _ .hom) (idl _)) (ap (α .η _ .hom) (idl _))) ⟩≡˘
    n-mon .ÎŒ ∘ ⟹ α .η _ .hom (id ∘ π₁) , α .η _ .hom (id ∘ π₂) ⟩ ≡⟚ ap (n-mon .ÎŒ ∘_) (ap₂ ⟹_,_⟩ (ap hom (α .is-natural _ _ _) $ₚ _) (ap hom (α .is-natural _ _ _) $ₚ _)) ⟩≡
    n-mon .ÎŒ ∘ (α .η m .hom id ⊗₁ α .η m .hom id)                ∎

  open is-iso

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

Internalizing presheaves of monoids🔗

Intuitively, what we have just shown is that monoids internal to C\mathcal{C} yield monoids in the internal language of C\mathcal{C} — giving monoids in arbitrary contexts, in a manner compatible with substitution. We will now establish the converse: If Hom(−,M)\mathbf{Hom}(-, M) is always a monoid, then MM 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.

    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 context2, for multiplication, this is the context M×MM \times M.

    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 Hom(−,M)\mathbf{Hom}(-, M).

    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 PP, then, by definition, we have substitution-stable monoid structures on P(−)P(-), and natural isomorphisms P(−)≅Hom(−,M)P(-) \cong \mathbf{Hom}(-, M), for some object M:CM : \mathcal{C}.

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

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

    η* : ∀ 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)
There is no surprise to the calculation establishing the monoid laws, here.
    η*-idl : ∀ {x} → (f : Hom x m) → ÎŒ* (η* x) f ≡ f
    η*-idl {x} f =
      gen (⌜ elt (gen identity) ⌝ ⋆ elt f) ≡⟚ ap! (repr.invr ηₚ _ $ₚ _) ⟩≡
      gen (identity ⋆ elt f)               ≡⟚ ap gen PMon.idl ⟩≡
      gen (elt f)                          ≡⟚ repr.invl ηₚ _ $ₚ _ ⟩≡
      f                                    ∎

    η*-idr : ∀ {x} → (f : Hom x m) → ÎŒ* f (η* x) ≡ f
    η*-idr {x} f =
      gen (elt f ⋆ ⌜ elt (gen identity) ⌝) ≡⟚ ap! (repr.invr ηₚ _ $ₚ _) ⟩≡
      gen (elt f ⋆ identity)               ≡⟚ ap gen PMon.idr ⟩≡
      gen (elt f)                          ≡⟚ 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! (repr.invr ηₚ _ $ₚ _) ⟩≡
      gen (elt f ⋆ (elt g ⋆ elt h))               ≡⟚ ap gen PMon.associative ⟩≡
      gen (⌜ elt f ⋆ elt g ⌝ ⋆ elt h)             ≡⟚ ap! (sym $ repr.invr ηₚ _ $ₚ _) ⟩≡
      gen (elt (gen (elt f ⋆ elt g)) ⋆ elt h)     ∎

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)
If you still have the patience for some more algebra, you can expand this <details> element.
    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)                 ≡⟚ 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)                               ≡⟚ 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₂ _⋆_ (repr.invr ηₚ _ $ₚ _) (repr.invr ηₚ _ $ₚ _)) ⟩≡˘
      ÎŒ* (gen f) (gen g)                                   ≡˘⟚ ap₂ ÎŒ* π₁∘⟚⟩ π₂∘⟚⟩ ⟩≡˘
      ÎŒ* (π₁ ∘ ⟹ gen f , gen g ⟩) (π₂ ∘ ⟹ gen f , gen g ⟩) ≡˘⟚ ÎŒ*-nat _ _ _ ⟩≡˘
      ÎŒ* π₁ π₂ ∘ ⟹ gen f , gen g ⟩                         ∎

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

Put another way, our functor MonC→PSh(C)M\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 C\mathcal{C} are really monoids in C\mathcal{C}. 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!


  1. Evaluating their components at the identity morphism, as usual!↩

  2. The terminal object.↩