Data.Category.Product

Documentation

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

Constructors

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

Instances

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

The product category of categories c1 and c2.

Defined in Data.Category.Product

Methods

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

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

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

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

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

Defined in Data.Category.Limit

Associated Types

type BinaryCoproduct (c1 :**: c2) x y :: Kind k

Methods

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

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

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

(+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). (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 :: Type -> Type -> Type)

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

Defined in Data.Category.Limit

Associated Types

type BinaryProduct (c1 :**: c2) x y :: Kind k

Methods

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

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

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

(***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). (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 :: Type -> Type -> Type)

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

Defined in Data.Category.Limit

Associated Types

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

Methods

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

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

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

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

Defined in Data.Category.Limit

Associated Types

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

Methods

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

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

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

Defined in Data.Category.Limit

type InitialObject (c1 :**: c2 :: Type -> Type -> Type) = (InitialObject c1, InitialObject c2)

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

Defined in Data.Category.Limit

type TerminalObject (c1 :**: c2 :: Type -> Type -> Type) = (TerminalObject c1, TerminalObject c2)

type BinaryCoproduct (c1 :**: c2 :: Type -> Type -> Type) ((x1, x2) :: Kind (c1 :**: c2)) ((y1, y2) :: Kind (c1 :**: c2))

Defined in Data.Category.Limit

type BinaryCoproduct (c1 :**: c2 :: Type -> Type -> Type) ((x1, x2) :: Kind (c1 :**: c2)) ((y1, y2) :: Kind (c1 :**: c2)) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)

type BinaryProduct (c1 :**: c2 :: Type -> Type -> Type) ((x1, x2) :: Kind (c1 :**: c2)) ((y1, y2) :: Kind (c1 :**: c2))

Defined in Data.Category.Limit

type BinaryProduct (c1 :**: c2 :: Type -> Type -> Type) ((x1, x2) :: Kind (c1 :**: c2)) ((y1, y2) :: Kind (c1 :**: c2)) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)