GoKawiilPreviously: Kan Extensions in Double Categories.
In programming, actegories play a central role in optics: lenses, prisms, traversals, etc. To understand actegories, let’s start with the definition of a monoidal category.
Monoidal Category
A monoidal category is a category equipped with a tensor product. A tensor product is a functor . We assume that this product is associative and unital– up to isomorphism. It means that there is an invertible associator:
natural in all three arguments. We also have a unit object and two (invertible, natural) unitors:
To get a better feel for it, we can try to model a monoidal category in Haskell. We parameterize it by the type of the tensor product, ten , which we want to be a Bifunctor :
class (Bifunctor ten) => MonoidalCategory ten where ...
The standard way to define a subcategory of Hask is to restrict the types of objects by imposing a constraint. Such a restriction has a special kind, Constraint :
class Bifunctor ten => MonoidalCategory (obj :: Type -> Constraint) ten where ...
A common example of such a constraint is a typeclass. For instance Monoid will restrict the objects of the category to be monoids. (In principle, we should also restrict the type of arrows, here to monoid morphisms.)
... continue reading