Category operations

Interfaces for programming with categories. A category is represented by a type of objects obj, and a type of morphisms C : obj → obj → Type. The interface gives the signatures for the following operations (which may be defined independently). For any a, b, c):

• eq2 : C a b → C a b → Prop, equivalence of morphisms;
• id_ a : C a a, the identity morphism;
• cat : C a b → C b c → C a c, composition of morphisms;
• empty : C i a, the initial morphism (where i is the initial object);
• bimap : C a b → C c d → C (bif a b) (bif c d), "vertical composition" of morphisms, where bif is a bifunctor (in our case it is the coproduct bifunctor);
• assoc_l, assoc_r, unit_l, unit_l', unit_r, unit_r': natural isomorphisms of a tensor product bif, making C a monoidal category;
• case_ : C a c → C b c → C (bif a b) c, "case analysis" of a coproduct bif;
• inl_ : C a (bif a b), left injection in a coproduct bif;
• inr_ : C b (bif a b), right injection;
• iter : C a (bif a b) → C a b, loop operator.

We use typeclasses to give such "canonical names" to these operations, allowing us to define common notations and equations once and for all. This is the approach described in "Type Classes for Mathematics in Type Theory", by Bas Spitters and Eelis van der Weegen (https://arxiv.org/abs/1102.1323). The properties of these operations are given in Basics.CategoryTheory. Notations >>> and ⩯ are in the module CatNotations, under the scope cat. The common way to use them is:
  Import CatNotations.
  Local Open Scope cat.

Low-level infrastructure

Categories are parameterized by a type of objects obj.

A category will be designated by the type of its morphisms (Hom-sets), which is indexed by two objects.

Examples found in this library:

• The category of functions: obj := Type, Fun a b := a → b.
• The category of indexed functions: obj := Type → Type, IFun E F := E ~> F (where ~> is defined in Basics.Basics).
• The category of itree continuations (one category for every E : Type → Type): obj := Type, ktree E a b := a → itree E a b.
• The category of itree handlers: obj := Type → Type, Handler E F := E ~> itree F.

The latter two are Kleisli categories of the former two respectively. Bifunctors from a category to itself are designated by their object maps. They are associated to morphism maps via the Bimap class.

Scope for category notations.

Categories

The equivalence between two morphisms f and g is written eq2 f g or f ⩯ g (\hatapprox in LaTeX).

The identity morphism for the object a : obj is written id_ a.

Given two morphisms f and g with a common endpoint, their composition (or con(cat)enation) is written cat f g or f >>> g.

If there is an initial object i, its initial morphisms are written empty : C i a.

If there is a terminal object t, its terminal morphisms are written one : C a i.

Bifunctors

Bifunctors map pairs of objects to objects (bif) and pairs of morphisms to morphisms (bimap). The composition bimap f g is also called tensor product of f and g. Many of the following typeclases are derived from just three basic Coproduct constructions:

• Case (case analysis)
• Inl (left injection)
• Inr (right injection)

Coproducts

Coproducts are a generalization of sum types and case analysis. Case analysis on a sum.

Injection into the left component.

Injection into the right component.

Tensor products (monoidal categories)

cat can be seen as "horizontal composition", while bimap as "vertical composition". When this vertical composition is associative and has units (similarly to cat), we have a monoidal category. To be more precise, this associativity and unity of vertical composition is generally allowed to be witnessed up to some isomorphisms, called associators and unitors. These properties are defined formally in Basics.CategoryTheory.

Associators

Unitors

Products

Products are a generalization of product types Pairing.

Projection onto the left component.

Projection onto the right component.

Symmetry

Notations with explicit objects

Useful to annotate the above isomorphisms in cases where their types would be ambiguous.

With explicit category.

Core notations

Derived constructions

Coproduct operations

Generalization of a + a → a.

Cocartesian category

The coproduct defines a symmetric monoidal category, called a cocartesian category.

Coproducts are bifunctors.

Coproducts are symmetric.

Coproducts are associative.

The initial object is a unit for the coproduct.

Cartesian category

The product defines a symmetric monoidal category, called a cartesian category.

Products are bifunctors.

Products are symmetric.

Products are associative.

The initial object is a unit for the product.

Iteration, fixed points

Categories with a loop operator (pre-iterative categories). Abstract generalization of ITree.Basics.Basics.ALoop and ITree.Core.KTree.loop. iter is often denoted as a dagger in the relevant literature.

Trace operator (generalization of KTree.loop).

For our purposes, loop and iter are mutually derivable. loop is a definition instead of another class to prevent the interface from growing too much. We originally started with traced categories but iterative categories seem to provide more of the theory we need.

Automatic solver of reassociating sums

The instance weights on ReSum_inl (8) and ReSum_inr (9) are so that, if you have a list E +' E +' F (associated to the right: E +' (E +' F)), then the first one will be picked for the inclusion E -< E +' E +' F.