Monoid.idr

Monoidal Category

One of the defining features of $\mathcal{C}ont$ is the plurality of monoidal products within it. To represent them we give the definition of a monoidal category which we will instanciate with multiple monoidal product in $\mathcal{C}ont$.

Definition

A monoidal product on a Category $\mathcal{C}$ is given by:

• A bifunctor $\otimes :\mathcal{C}\times \mathcal{C}\to \mathcal{C}$
• An object $I\in \mathcal{C}$
• Natural Isomorphisms:
  • For associativity $\alpha :X\otimes (Y\otimes Z)\cong (X\otimes Y)\otimes Z$
  • For units on the left : $\lambda :X\otimes I\cong X$
  • For units on the right : $\rho :I\otimes X\cong X$

record Monoidal {0 o : Type} (c : Category o) where
  constructor MkMonoidal
 
  mult : Bifunctor c c c
 
  i : o

  alpha : let f1, f2 : (c × (c × c)) ->> c
              f1 = ((idF _) `pair` mult) ⨾⨾ mult
              f2 = assocR ⨾⨾ ((mult `pair` idF _) ⨾⨾ mult)
          in f1 =~= f2

TODO: add diagram

  leftUnitor :
      let 0 leftAppliedMult : c ->> c
          leftAppliedMult = applyL {a = c, b = c, c} i mult
      in leftAppliedMult =~= idF c

TODO: add diagram

  rightUnitor :
      let 0 rightAppliedMult : c ->> c
          rightAppliedMult = applyR i mult
      in rightAppliedMult =~= idF c

Like before, we define a couple of utility functions to more easily manipulate monoidal products. $(\times )$ uses the product’s bifunctor to combine objects and $(\otimes )$ uses the same functor to combine morphisms.

(⊗) : {auto 0 cat : Category o} -> (mon : Monoidal cat) => o -> o -> o
(⊗) a b = mon.mult.mapObj (a && b)
 
public export 0
(-⊗-)  : {auto 0 cat : Category o} -> {0 x, y, a, b : o} -> (mon : Monoidal cat) =>
       x ~> y -> a ~> b -> x ⊗ a ~> y ⊗ b
(-⊗-) m1 m2 = mon.mult.mapHom (x && a) (y && b) (m1 && m2)

Monoids in a Monoidal Category

Given a monoidal category, we define monoids in that category by leveraging the monoidal structure of the category.

Definition

Given a category $\mathcal{C}$ and $(\otimes ,I,\alpha ,\lambda ,\rho )$ a monoidal product on it. A monoid object with respect to this structure is a triple $(M,\mu ,\eta )$ where:

• $M\in \mathcal{C}$ is an object of $\mathcal{C}$
• $\mu :M\otimes M\to M$ combines those objects using the monoidal product from $\mathcal{C}$
• $\eta :I\to M$ a map from the neutral object of the monoidal product from $\mathcal{C}$
• And the following equations hold:
  • The pentagon $\alpha ;1\otimes \mu ;\mu \cong \mu \otimes 1;\mu$
  • The left-unit $\eta \otimes 1;\mu \cong \lambda$
  • The right-unit $1\otimes \eta ;\mu \cong \rho$

We port this definition in Idris directly by providing a record with all the necessary information, parameterised over the category and its monoidal structure.

record MonoidObject {0 o : Type} {cat : Category o} (mon : Monoidal cat) where
  constructor MkMonObj
  obj : o
  η : mon.i ~> obj
  mult : obj ⊗ obj ~> obj

  0 left : let 0 η_id_μ, λ : mon.i ⊗ obj ~> obj
               0 topMorphism : mon.i ⊗ obj ~> obj ⊗ obj
               topMorphism = η -⊗- cat.id obj
               η_id_μ = topMorphism |> mult
               λ = mon.leftUnitor.nat.component obj
            in η_id_μ === λ

  0 right : let 0 id_η_μ, ρ : obj ⊗ mon.i  ~> obj
                0 topMorphism : obj ⊗ mon.i  ~> obj ⊗ obj
                topMorphism = cat.id obj -⊗- η
                id_η_μ = topMorphism |> mult
                ρ  = mon.rightUnitor.nat.component obj
             in id_η_μ === ρ

  0 assoc : let
                0 botLeft : (obj ⊗ obj) ⊗ obj ~> obj
                botLeft = mult -⊗- cat.id obj |> mult
                0 assoc : ((obj ⊗ obj) ⊗ obj) ~> obj ⊗ (obj ⊗ obj)
                assoc = mon.alpha.tan.component (obj && (obj && obj))
                0 topRight : ((obj ⊗ obj) ⊗ obj) ~> obj
                topRight = assoc |> cat.id obj -⊗- mult |> mult
            in botLeft === topRight