data-category-0.4.1: Category theory

Portability non-portable experimental sjoerd@w3future.com

Data.Category.CartesianClosed

Description

Synopsis

# Documentation

type family Exponential (~>) y z :: *Source

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

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

Methods

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

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

(^^^) :: (z1 ~> z2) -> (y2 ~> y1) -> Exponential ~> y1 z1 ~> Exponential ~> y2 z2Source

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 ~> => CartesianClosed (Presheaves ~>) The category of presheaves on a category `C` is cartesian closed for any `C`.

data ExpFunctor (~>) Source

Constructors

 ExpFunctor

Instances

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

data Apply y z Source

Constructors

 Apply

Instances

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

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

The product functor is left adjoint the the exponential functor.

curry :: CartesianClosed ~> => Obj ~> x -> Obj ~> y -> Obj ~> z -> (BinaryProduct ~> x y ~> z) -> x ~> Exponential ~> y zSource

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 ~> => Obj ~> x -> Obj ~> y -> Obj ~> z -> (x ~> Exponential ~> y z) -> BinaryProduct ~> x y ~> zSource

type State (~>) s a = Exponential ~> s (BinaryProduct ~> a s)Source