module Cat.Monoidal.Diagram.Monoid.Representable where

Externalising monoids as presheaves🔗

Let be a Cartesian monoidal category, and consider a monoid object in it. Our first observation is that, despite the definition of monoid object only referring to (the monoidal structure on and the object each set of generalised elements also carries the structure of a monoid. The unit element is given by

and the multiplication map is given by

  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-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 internal language, where we think of the as being the set of “ in context ”, our observation means that is a monoid in any context. Under this interpretation, pre-composition with a map corresponds to the substitution operation, mapping terms from the context to

Following this line of thinking, the next thing to interrogate is whether the monoid operations on terms is preserved by substitution: is precomposition with 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 fits into a presheaf of monoids, a functor mapping objects of to the monoid of generalised elements 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, and together with a homomorphism We can now consider the postcomposition with a function of sets which maps between the relativizations of and to arbitrary contexts: it has type

Since we’ve equipped these sets with monoid structures using the internal structures on and and is a homomorphism between those, we would like for postcomposition with 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 externalises to a family of where is an arbitrary object we affectionately refer to as the “context”.

  • Maps act by precomposition, which, extending the analogy, corresponds to substitution. Substitution along arbitrary maps is a monoid homomorphism, so extends to a functor a representable presheaf of monoids;

  • Monoid homomorphisms when acting by postcomposition, externalise to homomorphisms

To make this correspondence formal, we’ll define the category of representable presheaves of monoids to be the full subcategory of on the representable objects; for now, it will be denoted — a notation for which the author apologises. As usual, will denote the category of monoid objects on

We have described most of a functor It only remains to verify that the action by postcomposition of a monoid homomorphism is a natural transformation

  Mon→RepPShMon : Functor Mon[C] RepPShMon
  Mon→RepPShMon .F₀ (m , mon) .fst = Mon→PshMon mon
  Mon→RepPShMon .F₀ (m , mon) .snd = 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 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 # 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 yield monoids in the internal language of — giving monoids in arbitrary contexts, in a manner compatible with substitution. We will now establish the converse: If is always a monoid, then 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

    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-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 then, by definition, we have substitution-stable monoid structures on and natural isomorphisms for some object

  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

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

    η* :  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! (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)     

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 , pm) .fst = pm .rep , RepPshMon→Mon P pm
  Mon→RepPShMon-is-split-eso (P , pm) .snd = super-iso→sub-iso _ $ to-natural-iso ni where
    open make-natural-iso
    open RepPshMon→Mon P pm
    open PMon using (identity; _⋆_)
    module P = Functor P
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 pm)) P
    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 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 are really monoids in 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.↩︎