## Vitalii Guzeev

# Platonic Hask overview: representable functors and monoidal category structures

*Feb 23, 2023*

In the previous post, I promised to justify the change of signature of `fmap`

from `(a -> b) -> f a -> f b`

from `Prelude`

to `(a -> b) -> (f a -> f b)`

. And occasionally explain the former notation. There is a categorical notion to help, it is called Cartesian closedness.

Here we leave indices of \(\operatorname{Hom}\)-sets to context, same for definitions of objects — each subsection operates a fixed category.

#### Cartesian closedness

##### Definitions

Category \(\mathrm{C}\) is called **cartesian closed** if it has terminal object, for all \(A,B \in \operatorname{Ob}(\mathrm{C})\) there exists a product \(A \times B\) and exponential object \(B^A\).

To define all relevant notions it is convenient (following lectures in Russian by A. Gorodentsev) to define **representable functor**.

Functor \(F : \mathrm{C}^{op} \to Set\) is said to be **representable** if is it naturally isomorphic to \(\operatorname{Hom}(\_,A)\) for some \(A\). We call \(A\) the **representing object** of functor \(F\). Representing object is unique up to canonical isomorphism.

Any representing object has associated **universal property**. Let’s see it by example.

Consider objects \(A,B \in \mathrm{C}\). If functor \(\operatorname{Hom}(\_,A) \times \operatorname{Hom}(\_,B)\) is representable, its representing object \(A \times B\) is called the **product** of \(A\) and \(B\).

Write this definition: \(\forall Y\; Hom(Y, A \times B) \cong \operatorname{Hom}(Y,A) \times \operatorname{Hom}(Y,B)\).

By setting \(Y = A \times B\), we obtain via this isomorphism the pair of maps \(\pi_A : A \times B \to A\) and \(\pi_B : A \times B \to B\) which are the image of \(Id_{A \times B}\) under isomorphism. They are called **canonical projections**. For arbitrary \(Y\) this isomorphism guarantees existence and uniqueness of map \(\phi : Y \to A \times B\) for any pair of maps \(\psi_A : Y \to A\) and \(\psi_B : Y \to B\). There are maps \(\pi_A \circ \phi\) and \(\pi_B \circ \phi\), since isomorphism is natural, \(\pi_A \circ \phi = \psi_A\), \(\pi_B \circ \phi = \psi_B\).

Thus we obtain the universal property of a product:

For any \(Y\), \(f : Y \to A\) and \(g : Y \to B\) there exists map \(\phi : Y \to A \times B\) such that the following diagram commutes:

Consider constant functor \(\overline{\{0\}}\) moving all objects to a fixed singleton set and all morphisms to identity. We call representing object of \(\overline{\{0\}}\) **terminal object** of category \(\mathrm{C}\). By evaluating its universal property we have that it is the object \(T\) with exactly one morphism \(Y \to T\) for any \(Y\).

Assume \(\mathrm{C}\) has all binary products. Consider functor \(\operatorname{Hom}(\_ \times A, B)\). Its representing object \(B^A\) is called **exponential object**. Actually, we defined it via isomorphism \(\operatorname{Hom}(Y, B^A) \cong \operatorname{Hom}(Y \times A, B)\) which may look familiar.

By taking \(Y = B^A\) we obtain map \(eval : B^A \times A \to B\). We can draw the universal property:

Usually, terminal objects and products are defined in terms of limits. But limits are examples of representing objects and are not really important here. We will turn back to them later.

##### Hask is cartesian closed

To prove the statement in the header we have to demonstrate the terminal object, exponentials, and products.

Since morphisms in \(Hask\) do not have to preserve any structure the only candidates for the terminal object are types with a single term. These are types isomorphic to `()`

. They are all isomorphic (admit invertible bijections between each other), hence there is no need to check universality.

The evaluation map of the exponential object suggests an object satisfying universal property for types `a, b`

— it is `a -> b`

. Products are given by type with two natural projections — `(a,b)`

. Since universal objects are defined up to natural isomorphisms, product types `data Cons = Cons B C`

are also products, same for newtypes over arrow types, etc.

Definition of exponential object gives us a natural isomorphism `(a,b) -> c`

\(\cong\) `a -> (b -> c)`

for any types `a, b, c`

. This isomorphism is called currying. In Haskell it is common and is reflected in both implementation and notation — type `a -> b -> c`

is literally equivalent to `a -> (b -> c)`

(which is known as partial evaluation) and is isomorphic to `(a,b) -> c`

via inverse functions `curry`

and `uncurry`

.

There is an important proposition that any cartesian closed category is a closed symmetric monoidal category with the tensor product given by the product in the sense of given universal property.

Closedness (informally) means that hom-sets can be considered objects of the category. Again informally we can see it from the existence of exponentials — their elements are functions from `a`

to `b`

, and elements of \(Hom\)-sets are morphisms from `a`

to `b`

. The term `closed monoidal category`

encapsulates some compatibility conditions between the tensor product and exponentials. Rigorous definitions and proof of the claimed proposition are worth a separate post to be written.

So let’s proceed to the definition of the symmetric monoidal category.

#### Monoidal category structure

##### Definitions

Category \(\mathrm{C}\) is called **monoidal** if

- It is equipped with
**tensor product**bifunctor \(\otimes : \mathrm{C} \times \mathrm{C} \to \mathrm{C}\) and associator functor \(\alpha : \mathrm{C} \to \mathrm{C}\) satisfying associative law. - There exists unit object \(I\) and unitor functors \(\lambda\), \(\rho\) satisfying identity law.
- Both associator and unitor maps are natural isomorphisms where defined.

Associativity law is the commutativity of the following diagram:

Identity law is the commutativity of the following diagram:

Monoidal category is called **symmetric** if \(\forall A,B\) there exists isomorphism \(s_{AB} : A \otimes B \to B \otimes A\) such that the following diagram commutes:

##### Hask

From cartesian closedness there automatically follows that \(Hask\) is symmetric monoidal with \(\otimes =\)`(,)`

and unit — `()`

. Associator and unitor functors are obvious. Denote this structure as \((Hask, (,), ())\).

Consider \(End(Hask)\). It is a monoidal category with tensor product given by composition, unit — by `Identity`

functor, and with identical unitors and associator. Denote this structure as \((End(Hask),\circ,Id)\).

These two statements will be central in the next several posts.

#### Dual counterparts

Universal properties allow us to construct dual objects by formally reversing all arrows.

While doing it with already defined representing objects we obtain the following definitions:

- Initial object is defined as an object \(I\) such that it has unique morphism to any other object
- Coproduct is defined by the following diagram:

- Coexponential object is defined by the following diagram:

Category with an initial object, all coexponentials, and all binary coproducts is called **cocartesian coclosed**.

\(Hask\) does not have all coexponentials and is not cocartesian coclosed.

But it has all coproducts given by `Either a b`

and it has the initial object `Void`

. This data is enough to equip \(Hask\) with another structure of symmetric (since coproducts are symmetric) monoidal category. The tensor product is given by the coproduct and the unit is given by the initial object. Denote this structure as \((Hask, Either, Void)\).

#### Note on corepresentable functors

These universal objects with reversed arrows can be defined via duals to representable functors.

Functor \(F : \mathrm{C} \to Set\) is said to be **corepresentable** if is it naturally isomorphic to \(\operatorname{Hom}(A,\_)\) for some \(A\). \(A\) is called **corepresenting object** of functor \(F\). Representing object is unique up to canonical isomorphism.

Initial object corepresents \(\operatorname{Hom}(\emptyset, \_)\), \(A \coprod B\) corepresents \(\operatorname{Hom}(A,\_) \otimes \operatorname{Hom}(B,\_)\), coexponential corepresents \(\operatorname{Hom}(B, \_ \coprod A)\).

In \(Hask\) \(\operatorname{Hom}(A,\_)\) is written as `(->) A`

. We can restrict functors to instances of the `Functor`

type class and obtain the following definition of representable functor: functor `F`

is said to be representable if there exists a natural isomorphism between `F a`

and `(->) A a`

for every type `a`

. `A`

is the corepresenting object of `F`

. But `F`

must be considered as a functor to Set with values — sets of terms of resulting types of `Functor`

we started with instead of types.

This definition is captured in package representable-functors. Isomorphism `Cons a ~ A -> a`

in terms of this library is written as `f a ~ Key a -> a`

, to the left it is given by `tabulate`

, to the right by `index`

.