data-category-0.6.0: Category theory

Portability non-portable experimental sjoerd@w3future.com Safe-Inferred

Data.Category.CartesianClosed

Description

Synopsis

Documentation

class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k whereSource

A category is cartesian closed if it has all products and exponentials for all objects.

Associated Types

type Exponential k y z :: *Source

Methods

apply :: Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) zSource

tuple :: Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))Source

(^^^) :: k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)Source

Instances

 CartesianClosed (->) Exponentials in `Hask` are functions. CartesianClosed Cat Exponentials in `Cat` are the functor categories. CartesianClosed Boolean Implication makes the Boolean category cartesian closed. Category k => CartesianClosed (Presheaves k) The category of presheaves on a category `C` is cartesian closed for any `C`. CartesianClosed (f (Fix f)) => CartesianClosed (Fix f) `Fix f` inherits its exponentials from `f (Fix f)`.

data ExpFunctor k Source

Constructors

 ExpFunctor

Instances

 CartesianClosed k => Functor (ExpFunctor k) The exponential as a bifunctor.

data Apply c1 c2 Source

Constructors

 Apply

Instances

 (Category c1, Category c2) => Functor (Apply c1 c2) `Apply` is a bifunctor, `Apply :% (f, a)` applies `f` to `a`, i.e. `f :% a`.

data Tuple c1 c2 Source

Constructors

 Tuple

Instances

 (Category c1, Category c2) => Functor (Tuple c1 c2) `Tuple` converts an object `a` to the functor `Tuple1` `a`.

curryAdj :: CartesianClosed k => Obj k y -> Adjunction k k (ProductFunctor k :.: Tuple2 k k y) (ExpFunctor k :.: Tuple1 (Op k) k y)Source

The product functor is left adjoint the the exponential functor.

curry :: CartesianClosed k => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z)Source

From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions, generalized to any cartesian closed category.

uncurry :: CartesianClosed k => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) zSource

type State k s a = Exponential k s (BinaryProduct k a s)Source