data-category-0.10: Category theory

LicenseBSD-style (see the file LICENSE)
Maintainersjoerd@w3future.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
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
type BinaryCoproduct Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Fls Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Fls Fls Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Fls Fls Source # 
Instance details

Defined in Data.Category.Boolean

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
type BinaryCoproduct Boolean Tru Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Tru Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Tru Tru Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

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
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 :: Type 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 :: Type 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 #

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 :: Boolean a b -> Obj Boolean a Source #

tgt :: Boolean a b -> Obj Boolean b Source #

(.) :: Boolean b c -> Boolean a b -> Boolean a c 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 #

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 #

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 #

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 #

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 #

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 InitialObject Boolean Source # 
Instance details

Defined in Data.Category.Boolean

type TerminalObject Boolean Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Tru Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryCoproduct Boolean Fls Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Tru Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type BinaryProduct Boolean Fls Fls Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Tru Tru Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Tru Fls Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Fls Tru Source # 
Instance details

Defined in Data.Category.Boolean

type Exponential Boolean Fls Fls Source # 
Instance details

Defined in Data.Category.Boolean

data Arrow k a b Source #

Constructors

Arrow (k a b) 
Instances
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 :: Type 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 Dom (Arrow k a b) Source # 
Instance details

Defined in Data.Category.Boolean

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

Defined in Data.Category.Boolean

type Cod (Arrow k a b) = k
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 :: * -> * -> *) Source #

Constructors

Terminator 
Instances
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 :: Type Source #

Methods

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

type Dom (Terminator k) Source # 
Instance details

Defined in Data.Category.Boolean

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

Defined in Data.Category.Boolean

type Cod (Terminator k) = Nat Boolean 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 :: * -> * -> *) Source #

Constructors

Initializer 
Instances
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 :: Type Source #

Methods

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

type Dom (Initializer k) Source # 
Instance details

Defined in Data.Category.Boolean

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

Defined in Data.Category.Boolean

type Cod (Initializer k) = Nat Boolean 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.