Data.Category.Product

Documentation

data (:**:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where

Constructors

(:**:) :: c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)

Instances

(Category c1, Category c2) => Category ((:**:) c1 c2)

The product category of category c1 and c2.

Methods

src :: (c1 :**: c2) a b -> Obj (c1 :**: c2) a

tgt :: (c1 :**: c2) a b -> Obj (c1 :**: c2) b

(.) :: (c1 :**: c2) b c -> (c1 :**: c2) a b -> (c1 :**: c2) a c

(HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts ((:**:) c1 c2)

The binary coproduct of the product of 2 categories is the product of their binary coproducts.

Associated Types

type BinaryCoproduct ((:**:) c1 c2 :: * -> * -> *) x y :: *

Methods

inj1 :: Obj (c1 :**: c2) x -> Obj (c1 :**: c2) y -> (c1 :**: c2) x (BinaryCoproduct (c1 :**: c2) x y)

inj2 :: Obj (c1 :**: c2) x -> Obj (c1 :**: c2) y -> (c1 :**: c2) y (BinaryCoproduct (c1 :**: c2) x y)

(|||) :: (c1 :**: c2) x a -> (c1 :**: c2) y a -> (c1 :**: c2) (BinaryCoproduct (c1 :**: c2) x y) a

(+++) :: (c1 :**: c2) a1 b1 -> (c1 :**: c2) a2 b2 -> (c1 :**: c2) (BinaryCoproduct (c1 :**: c2) a1 a2) (BinaryCoproduct (c1 :**: c2) b1 b2)

(HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts ((:**:) c1 c2)

The binary product of the product of 2 categories is the product of their binary products.

Associated Types

type BinaryProduct ((:**:) c1 c2 :: * -> * -> *) x y :: *

Methods

proj1 :: Obj (c1 :**: c2) x -> Obj (c1 :**: c2) y -> (c1 :**: c2) (BinaryProduct (c1 :**: c2) x y) x

proj2 :: Obj (c1 :**: c2) x -> Obj (c1 :**: c2) y -> (c1 :**: c2) (BinaryProduct (c1 :**: c2) x y) y

(&&&) :: (c1 :**: c2) a x -> (c1 :**: c2) a y -> (c1 :**: c2) a (BinaryProduct (c1 :**: c2) x y)

(***) :: (c1 :**: c2) a1 b1 -> (c1 :**: c2) a2 b2 -> (c1 :**: c2) (BinaryProduct (c1 :**: c2) a1 a2) (BinaryProduct (c1 :**: c2) b1 b2)

(HasInitialObject c1, HasInitialObject c2) => HasInitialObject ((:**:) c1 c2)

The initial object of the product of 2 categories is the product of their initial objects.

Associated Types

type InitialObject ((:**:) c1 c2 :: * -> * -> *) :: *

Methods

initialObject :: Obj (c1 :**: c2) (InitialObject (c1 :**: c2))

initialize :: Obj (c1 :**: c2) a -> (c1 :**: c2) (InitialObject (c1 :**: c2)) a

(HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject ((:**:) c1 c2)

The terminal object of the product of 2 categories is the product of their terminal objects.

Associated Types

type TerminalObject ((:**:) c1 c2 :: * -> * -> *) :: *

Methods

terminalObject :: Obj (c1 :**: c2) (TerminalObject (c1 :**: c2))

terminate :: Obj (c1 :**: c2) a -> (c1 :**: c2) a (TerminalObject (c1 :**: c2))

type InitialObject ((:**:) c1 c2)

type InitialObject ((:**:) c1 c2) = (InitialObject c1, InitialObject c2)

type TerminalObject ((:**:) c1 c2)

type TerminalObject ((:**:) c1 c2) = (TerminalObject c1, TerminalObject c2)

type BinaryCoproduct ((:**:) c1 c2) (x1, x2) (y1, y2)

type BinaryCoproduct ((:**:) c1 c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)

type BinaryProduct ((:**:) c1 c2) (x1, x2) (y1, y2)

type BinaryProduct ((:**:) c1 c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)