data-category-0.4.1: Category theory




2, or the Boolean category. It contains 2 objects, one for true and one for false. It contains 3 arrows, 2 identity arrows and one from false to true.


data Fls Source

data Tru Source

data Boolean a b whereSource


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


Category Boolean

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

HasTerminalObject Boolean

True is the terminal object in the Boolean category.

HasInitialObject Boolean

False is the initial object in the Boolean category.

HasBinaryProducts Boolean

Conjunction is the binary product in the Boolean category.

HasBinaryCoproducts Boolean

Disjunction is the binary coproduct in the Boolean category.

CartesianClosed Boolean

Implication makes the Boolean category cartesian closed.

data NatAsFunctor f g whereSource


NatAsFunctor :: (Functor f, Functor g, Category c, Category d, Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d) => Nat (Dom f) (Cod f) f g -> NatAsFunctor f g 


(Category (Dom f), Category (Cod f)) => Functor (NatAsFunctor f g)

A natural transformation Nat c d is isomorphic to a functor from c :**: 2 to d.