data-category-0.11: Category theory
LicenseBSD-style (see the file LICENSE)
Maintainersjoerd@w3future.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Category.Boolean

Description

2 a.k.a. the Boolean category a.k.a. the walking arrow. It contains 2 objects, one for false and one for true. It contains 3 arrows, 2 identity arrows and one from false to true.

Synopsis

Documentation

data Fls Source #

Instances

Instances details
type Exponential Boolean Fls Fls Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Fls Fls = Tru
type Exponential Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Fls Tru = Tru
type Exponential Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Tru Fls = Fls
type BinaryCoproduct Boolean Fls Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Fls Fls = Fls
type BinaryCoproduct Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Fls Tru = Tru
type BinaryCoproduct Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Tru Fls = Tru
type BinaryProduct Boolean Fls Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Fls Fls = Fls
type BinaryProduct Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Fls Tru = Fls
type BinaryProduct Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Tru Fls = Fls
type (Arrow k a b) :% Fls Source # 
Instance details

Defined in Data.Category.Boolean

type (Arrow k a b) :% Fls = a

data Tru Source #

Instances

Instances details
type Exponential Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Fls Tru = Tru
type Exponential Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Tru Fls = Fls
type Exponential Boolean Tru Tru Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Tru Tru = Tru
type BinaryCoproduct Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Fls Tru = Tru
type BinaryCoproduct Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Tru Fls = Tru
type BinaryCoproduct Boolean Tru Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Tru Tru = Tru
type BinaryProduct Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Fls Tru = Fls
type BinaryProduct Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Tru Fls = Fls
type BinaryProduct Boolean Tru Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Tru Tru = Tru
type (Arrow k a b) :% Tru Source # 
Instance details

Defined in Data.Category.Boolean

type (Arrow k a b) :% Tru = b

data Boolean a b where Source #

Constructors

Fls :: Boolean Fls Fls 
F2T :: Boolean Fls Tru 
Tru :: Boolean Tru Tru 

Instances

Instances details
Category Boolean Source #

Boolean is the category with true and false as objects, and an arrow from false to true.

Instance details

Defined in Data.Category.Boolean

Methods

src :: forall (a :: k) (b :: k). Boolean a b -> Obj Boolean a Source #

tgt :: forall (a :: k) (b :: k). Boolean a b -> Obj Boolean b Source #

(.) :: forall (b :: k) (c :: k) (a :: k). Boolean b c -> Boolean a b -> Boolean a c Source #

CartesianClosed Boolean Source #

Implication makes the Boolean category cartesian closed.

Instance details

Defined in Data.Category.Boolean

Associated Types

type Exponential Boolean y z :: Kind k Source #

Methods

apply :: forall (y :: k) (z :: k). Obj Boolean y -> Obj Boolean z -> Boolean (BinaryProduct Boolean (Exponential Boolean y z) y) z Source #

tuple :: forall (y :: k) (z :: k). Obj Boolean y -> Obj Boolean z -> Boolean z (Exponential Boolean y (BinaryProduct Boolean z y)) Source #

(^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). Boolean z1 z2 -> Boolean y2 y1 -> Boolean (Exponential Boolean y1 z1) (Exponential Boolean y2 z2) Source #

HasBinaryCoproducts Boolean Source #

Disjunction is the binary coproduct in the Boolean category.

Instance details

Defined in Data.Category.Boolean

Associated Types

type BinaryCoproduct Boolean x y :: Kind k Source #

Methods

inj1 :: forall (x :: k) (y :: k). Obj Boolean x -> Obj Boolean y -> Boolean x (BinaryCoproduct Boolean x y) Source #

inj2 :: forall (x :: k) (y :: k). Obj Boolean x -> Obj Boolean y -> Boolean y (BinaryCoproduct Boolean x y) Source #

(|||) :: forall (x :: k) (a :: k) (y :: k). Boolean x a -> Boolean y a -> Boolean (BinaryCoproduct Boolean x y) a Source #

(+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Boolean a1 b1 -> Boolean a2 b2 -> Boolean (BinaryCoproduct Boolean a1 a2) (BinaryCoproduct Boolean b1 b2) Source #

HasBinaryProducts Boolean Source #

Conjunction is the binary product in the Boolean category.

Instance details

Defined in Data.Category.Boolean

Associated Types

type BinaryProduct Boolean x y :: Kind k Source #

Methods

proj1 :: forall (x :: k) (y :: k). Obj Boolean x -> Obj Boolean y -> Boolean (BinaryProduct Boolean x y) x Source #

proj2 :: forall (x :: k) (y :: k). Obj Boolean x -> Obj Boolean y -> Boolean (BinaryProduct Boolean x y) y Source #

(&&&) :: forall (a :: k) (x :: k) (y :: k). Boolean a x -> Boolean a y -> Boolean a (BinaryProduct Boolean x y) Source #

(***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Boolean a1 b1 -> Boolean a2 b2 -> Boolean (BinaryProduct Boolean a1 a2) (BinaryProduct Boolean b1 b2) Source #

Category k => HasColimits Boolean k Source #

The colimit of a functor from the Boolean category is the target of the arrow it points to.

Instance details

Defined in Data.Category.Boolean

Associated Types

type ColimitFam Boolean k f Source #

Methods

colimit :: Obj (Nat Boolean k) f -> Cocone Boolean k f (ColimitFam Boolean k f) Source #

colimitFactorizer :: Cocone Boolean k f n -> k (ColimitFam Boolean k f) n Source #

HasInitialObject Boolean Source #

False is the initial object in the Boolean category.

Instance details

Defined in Data.Category.Boolean

Associated Types

type InitialObject Boolean :: Kind k Source #

Methods

initialObject :: Obj Boolean (InitialObject Boolean) Source #

initialize :: forall (a :: k). Obj Boolean a -> Boolean (InitialObject Boolean) a Source #

Category k => HasLimits Boolean k Source #

The limit of a functor from the Boolean category is the source of the arrow it points to.

Instance details

Defined in Data.Category.Boolean

Associated Types

type LimitFam Boolean k f Source #

Methods

limit :: Obj (Nat Boolean k) f -> Cone Boolean k f (LimitFam Boolean k f) Source #

limitFactorizer :: Cone Boolean k f n -> k n (LimitFam Boolean k f) Source #

HasTerminalObject Boolean Source #

True is the terminal object in the Boolean category.

Instance details

Defined in Data.Category.Boolean

Associated Types

type TerminalObject Boolean :: Kind k Source #

Methods

terminalObject :: Obj Boolean (TerminalObject Boolean) Source #

terminate :: forall (a :: k). Obj Boolean a -> Boolean a (TerminalObject Boolean) Source #

type InitialObject Boolean Source # 
Instance details

Defined in Data.Category.Boolean

type InitialObject Boolean = Fls
type TerminalObject Boolean Source # 
Instance details

Defined in Data.Category.Boolean

type TerminalObject Boolean = Tru
type ColimitFam Boolean k f Source # 
Instance details

Defined in Data.Category.Boolean

type ColimitFam Boolean k f = f :% Tru
type LimitFam Boolean k f Source # 
Instance details

Defined in Data.Category.Boolean

type LimitFam Boolean k f = f :% Fls
type Exponential Boolean Fls Fls Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Fls Fls = Tru
type Exponential Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Fls Tru = Tru
type Exponential Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Tru Fls = Fls
type Exponential Boolean Tru Tru Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Tru Tru = Tru
type BinaryCoproduct Boolean Fls Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Fls Fls = Fls
type BinaryCoproduct Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Fls Tru = Tru
type BinaryCoproduct Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Tru Fls = Tru
type BinaryCoproduct Boolean Tru Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Tru Tru = Tru
type BinaryProduct Boolean Fls Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Fls Fls = Fls
type BinaryProduct Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Fls Tru = Fls
type BinaryProduct Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Tru Fls = Fls
type BinaryProduct Boolean Tru Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Tru Tru = Tru

trueProductMonoid :: MonoidObject (ProductFunctor Boolean) Tru Source #

falseCoproductComonoid :: ComonoidObject (CoproductFunctor Boolean) Fls Source #

trueProductComonoid :: ComonoidObject (ProductFunctor Boolean) Tru Source #

falseCoproductMonoid :: MonoidObject (CoproductFunctor Boolean) Fls Source #

trueCoproductMonoid :: MonoidObject (CoproductFunctor Boolean) Tru Source #

falseProductComonoid :: ComonoidObject (ProductFunctor Boolean) Fls Source #

newtype Arrow k a b Source #

Constructors

Arrow (k a b) 

Instances

Instances details
Category k => Functor (Arrow k a b) Source #

Any functor from the Boolean category points to an arrow in its target category.

Instance details

Defined in Data.Category.Boolean

Associated Types

type Dom (Arrow k a b) :: Type -> Type -> Type Source #

type Cod (Arrow k a b) :: Type -> Type -> Type Source #

type (Arrow k a b) :% a Source #

Methods

(%) :: Arrow k a b -> Dom (Arrow k a b) a0 b0 -> Cod (Arrow k a b) (Arrow k a b :% a0) (Arrow k a b :% b0) Source #

type Cod (Arrow k a b) Source # 
Instance details

Defined in Data.Category.Boolean

type Cod (Arrow k a b) = k
type Dom (Arrow k a b) Source # 
Instance details

Defined in Data.Category.Boolean

type Dom (Arrow k a b) = Boolean
type (Arrow k a b) :% Fls Source # 
Instance details

Defined in Data.Category.Boolean

type (Arrow k a b) :% Fls = a
type (Arrow k a b) :% Tru Source # 
Instance details

Defined in Data.Category.Boolean

type (Arrow k a b) :% Tru = b

type SrcFunctor = LimitFunctor Boolean Source #

The source functor sends arrows (as functors from the Boolean category) to their source.

type TgtFunctor = ColimitFunctor Boolean Source #

The target functor sends arrows (as functors from the Boolean category) to their target.

data Terminator (k :: Type -> Type -> Type) Source #

Constructors

Terminator 

Instances

Instances details
HasTerminalObject k => Functor (Terminator k) Source #

Terminator k is the functor that sends an object to its terminating arrow.

Instance details

Defined in Data.Category.Boolean

Associated Types

type Dom (Terminator k) :: Type -> Type -> Type Source #

type Cod (Terminator k) :: Type -> Type -> Type Source #

type (Terminator k) :% a Source #

Methods

(%) :: Terminator k -> Dom (Terminator k) a b -> Cod (Terminator k) (Terminator k :% a) (Terminator k :% b) Source #

type Cod (Terminator k) Source # 
Instance details

Defined in Data.Category.Boolean

type Cod (Terminator k) = Nat Boolean k
type Dom (Terminator k) Source # 
Instance details

Defined in Data.Category.Boolean

type Dom (Terminator k) = k
type (Terminator k) :% a Source # 
Instance details

Defined in Data.Category.Boolean

type (Terminator k) :% a = Arrow k a (TerminalObject k)

terminatorLimitAdj :: HasTerminalObject k => Adjunction k (Nat Boolean k) (SrcFunctor k) (Terminator k) Source #

Terminator is right adjoint to the source functor.

data Initializer (k :: Type -> Type -> Type) Source #

Constructors

Initializer 

Instances

Instances details
HasInitialObject k => Functor (Initializer k) Source #

Initializer k is the functor that sends an object to its initializing arrow.

Instance details

Defined in Data.Category.Boolean

Associated Types

type Dom (Initializer k) :: Type -> Type -> Type Source #

type Cod (Initializer k) :: Type -> Type -> Type Source #

type (Initializer k) :% a Source #

Methods

(%) :: Initializer k -> Dom (Initializer k) a b -> Cod (Initializer k) (Initializer k :% a) (Initializer k :% b) Source #

type Cod (Initializer k) Source # 
Instance details

Defined in Data.Category.Boolean

type Cod (Initializer k) = Nat Boolean k
type Dom (Initializer k) Source # 
Instance details

Defined in Data.Category.Boolean

type Dom (Initializer k) = k
type (Initializer k) :% a Source # 
Instance details

Defined in Data.Category.Boolean

type (Initializer k) :% a = Arrow k (InitialObject k) a

initializerColimitAdj :: HasInitialObject k => Adjunction (Nat Boolean k) k (Initializer k) (TgtFunctor k) Source #

Initializer is left adjoint to the target functor.