data-category-0.5.1: 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. (HasTerminalObject (Presheaves k), HasBinaryProducts (Presheaves k), Category k) => CartesianClosed (Presheaves k) The category of presheaves on a category `C` is cartesian closed for any `C`.

data ExpFunctor k Source

Constructors

 ExpFunctor

Instances

 (Category (Dom (ExpFunctor k)), Category (Cod (ExpFunctor k)), CartesianClosed k) => Functor (ExpFunctor k) The exponential as a bifunctor.

data Apply y z Source

Constructors

 Apply

Instances

 (Category (Dom (Apply y z)), Category (Cod (Apply y z)), Category y, Category z) => Functor (Apply y z) `Apply` is a bifunctor, `Apply :% (f, a)` applies `f` to `a`, i.e. `f :% a`.

data ToTuple1 y z Source

Constructors

 ToTuple1

Instances

 (Category (Dom (ToTuple1 y z)), Category (Cod (ToTuple1 y z)), Category y, Category z) => Functor (ToTuple1 y z) `ToTuple1` converts an object `a` to the functor `Tuple1` `a`.

data ToTuple2 y z Source

Constructors

 ToTuple2

Instances

 (Category (Dom (ToTuple2 y z)), Category (Cod (ToTuple2 y z)), Category y, Category z) => Functor (ToTuple2 y z) `ToTuple2` converts an object `a` to the functor `Tuple2` `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