This module exports "record-style" wrappers around various
interfaces in this library. These may be easier to use if the
categories you're constructing are particularly complex, as
Idris's interface resolution can often break.
This module defines the functor category between two categories,
`FunCat C D`, traditionally written `[C, D]`. Its morphisms are
natural transformations between parallel functors.
This module defines a more general Kleisli category construction
that can be used to derive a premonoidal category structure from
any strong monad on any premonoidal category.
This module defines `Linear`, the category of types and linear
functions. Unlike the unrestricted function category `Typ`, this
is a non-distributive bimonoidal category.
This module defines the category of types and functions, named
`Typ`. Using this is more efficient than something like `Morphism`,
as it erases the types at runtime.
This module provides a compatibility layer between the traditional
Haskell arrow hierarchy and the categorical interfaces of this
library. These functions may be easier to write code with for users
who are already familiar with arrows.
This module defines `Wrap0`, a wrapper type containing a value
that is present at compile-time, but erased during run-time. This
wrapper is used to define categories with erased objects, such as
the category of types `Typ`.