Safe Haskell	Safe-Inferred
Language	Haskell2010

Hask.Category

Contents

Category
Functors
- Regular
- (Curried) Bifunctors
Vacuous
Categories
Prelude

Synopsis

Functors

Regular

class (Category' (Dom f), Category' (Cod f)) => Functor f where Source

Associated Types

type Dom f :: i -> i -> * Source

type Cod f :: j -> j -> * Source

Methods

fmap :: Dom f a b -> Cod f (f a) (f b) Source

Instances

Functor Constraint * Dict
Functor * * ((->) a)
Functor * * (Either a)
Functor * * ((,) a)
FunctorOf * (* -> ) (->) (Nat * (->) (->)) p => Functor * * (Fix p)
Functor Constraint * ((:-) b)
(Category' k c, (~) (k -> Constraint) (Ob k c) (Vacuous k c)) => Functor k Constraint (Vacuous k c)
Identified k c => Functor k k (Id k c)
(Category k p, (~) (k -> k -> ) (Op k p) (Yoneda k p)) => Functor k (Yoneda k p a)
Functor k * (Unit k k a)
(Category k c, Ob k c r, Ob k c a) => Functor k * (Beget k c r a)
(Category k c, Ob k c r, Ob k c a) => Functor k * (Get k c r a)
((~) (k -> k -> ) (Dom k (k -> k) t) c, CopresheafOf k c f, CopresheafOf k c g) => Functor k (Day k t f g)
(Category k c, Category k2 d, Composed k1 e, Functor k2 k1 f, Functor k k2 g, (~) (k1 -> k1 -> ) e (Cod k2 k1 f), (~) (k2 -> k2 -> ) d (Cod k k2 g), (~) (k2 -> k2 -> ) d (Dom k2 k1 f), (~) (k -> k -> ) c (Dom k k2 g)) => Functor k k (Compose k k k c d e f g)
(Category k1 c, Category k2 d, Category k e, ProfunctorOf k k2 d e p, ProfunctorOf k2 k1 c d q, Ob k1 c a) => Functor k * (Procompose k k k c d e p q a)
Functor * (* -> *) (->)
Functor * (* -> *) Either
Functor * (* -> *) (,)
Functor Constraint (Constraint -> *) (:-)
(Category k p, (~) (k -> k -> ) (Op k p) (Yoneda k p)) => Functor k (k -> ) (Yoneda k p)
Category k c => Functor k (k -> k -> *) (Beget k c)
Category k c => Functor k (k -> k -> *) (Get k c)
Functor k (k -> *) (Unit k k)
(Category k c, Ob k c r) => Functor k (k -> *) (Beget k c r)
(Category k c, Ob k c r) => Functor k (k -> *) (Get k c r)
(Category k c, Category k1 d, Category k2 e, ProfunctorOf k2 k1 d e p, ProfunctorOf k1 k c d q) => Functor k (k -> *) (Procompose k k k c d e p q)
(Category' k p, Category' k1 q) => Functor (k -> k) Constraint (FunctorOf k k p q)
(Category' k p, Category k1 q) => Functor (k -> k) * (Nat k k p q a)
(Category k p, Category k1 q) => Functor (Either k k) * (Coproduct k k p q a)
(Category k p, Category k1 q, ProductOb k k1 p q a) => Functor ((,) k k) * (Product k k p q a)
Functor (* -> * -> ) ( -> *) Fix
((~) (k -> k -> ) (Dom k (k -> k) t) c, Category k c) => Functor (k -> ) ((k -> ) -> k -> ) (Day k t)
((~) (k -> k -> ) (Dom k (k -> k) t) c, CopresheafOf k c f) => Functor (k -> ) (k -> *) (Day k t f)
(Category' k p, Category k1 q) => Functor (k -> k) ((k -> k) -> *) (Nat k k p q)
(Category k p, Category k1 q) => Functor (Either k k) (Either k k -> *) (Coproduct k k p q)
(Category k p, Category k1 q) => Functor ((,) k k) ((,) k k -> *) (Product k k p q)
(Category k c, Category k1 d, Category k2 e) => Functor (k -> k -> ) ((k -> k -> ) -> k -> k -> *) (Procompose k k k c d e)
(Category k c, Category k1 d, Composed k2 e) => Functor (k -> k) ((k -> k) -> k -> k) (Compose k k k c d e)
(Category k c, Category k1 d, Category k2 e, ProfunctorOf k2 k1 d e p) => Functor (k -> k -> ) (k -> k -> ) (Procompose k k k c d e p)
(Category k c, Category k1 d, Composed k2 e, Functor k1 k2 f, (~) (k2 -> k2 -> ) e (Cod k1 k2 f), (~) (k1 -> k1 -> ) d (Dom k1 k2 f)) => Functor (k -> k) (k -> k) (Compose k k k c d e f)

class (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f Source

Instances

(Functor k k1 f, (~) (k -> k -> ) (Dom k k1 f) p, (~) (k1 -> k1 -> ) (Cod k k1 f) q) => FunctorOf k k p q f
(Category' k p, Category' k1 q) => Functor (k -> k) Constraint (FunctorOf k k p q)
type Dom (k -> k1) Constraint (FunctorOf k k1 p q) = Nat k k1 p q
type Cod (k -> k1) Constraint (FunctorOf k k1 p q) = (:-)

ob :: forall f a. Functor f => Ob (Dom f) a :- Ob (Cod f) (f a) Source

obOf :: (Category (Dom f), Category (Cod f)) => NatId f -> Endo (Dom f) a -> Dict (Ob (Nat (Dom f) (Cod f)) f, Ob (Dom f) a, Ob (Cod f) (f a)) Source

contramap :: Functor f => Opd f b a -> Cod f (f a) (f b) Source

(Curried) Bifunctors

class (Functor p, Cod p ~ Nat (Dom2 p) (Cod2 p), Category' (Dom2 p), Category' (Cod2 p)) => Bifunctor p Source

Instances

(Functor i (j -> k) p, (~) ((j -> k) -> (j -> k) -> *) (Cod i (j -> k) p) (Nat j k (Dom2 j k i p) (Cod2 k j i p)), Category' j (Dom2 j k i p), Category' k (Cod2 k j i p)) => Bifunctor i j k p

type Cod2 p = NatCod (Cod p) Source

type Dom2 p = NatDom (Cod p) Source

fmap1 :: forall p a b c. (Bifunctor p, Ob (Dom p) c) => Dom2 p a b -> Cod2 p (p c a) (p c b) Source

first :: (Functor f, Cod f ~ Nat d e, Ob d c) => Dom f a b -> e (f a c) (f b c) Source

bimap :: Bifunctor p => Dom p a b -> Dom2 p c d -> Cod2 p (p a c) (p b d) Source

dimap :: Bifunctor p => Opd p b a -> Dom2 p c d -> Cod2 p (p a c) (p b d) Source

E-Enriched profunctors f : C -/-> D are represented by a functor of the form:

C^op -> [ D, E ]

The variance here matches Haskell's order, which means that the contravariant argument comes first!

Vacuous

class Vacuous c a Source

Instances

Vacuous k c a
(Category' k c, (~) (k -> Constraint) (Ob k c) (Vacuous k c)) => Functor k Constraint (Vacuous k c)
type Dom k Constraint (Vacuous k c) = c
type Cod k Constraint (Vacuous k c) = (:-)

Categories

Constraints

data Constraint :: BOX

Instances

Category Constraint (:-)
Category' Constraint (:-)
Identified Constraint (:-)
Composed Constraint (:-)
Functor Constraint * Dict
FullyFaithful Constraint * Dict
Functor Constraint * ((:-) b)
(Category' k c, (~) (k -> Constraint) (Ob k c) (Vacuous k c)) => Functor k Constraint (Vacuous k c)
Functor Constraint (Constraint -> *) (:-)
FullyFaithful Constraint (Constraint -> *) (:-)
Category Constraint c => Class a (Id Constraint c a)
Category Constraint c => a :=> (Id Constraint c a)
(Category k c, Category k1 d, Category Constraint e) => Class (f (g a)) (Compose k k Constraint c d e f g a)
(Category k c, Category k1 d, Category Constraint e) => (f (g a)) :=> (Compose k k Constraint c d e f g a)
Typeable ((* -> *) -> Constraint) Alternative
Typeable ((* -> *) -> Constraint) Applicative
Typeable (* -> Constraint) Monoid
Typeable (Constraint -> Constraint -> *) (:-)
Typeable (Constraint -> *) Dict
(Category' k p, Category' k1 q) => Functor (k -> k) Constraint (FunctorOf k k p q)
type Ob Constraint (:-) = Vacuous Constraint (:-)
type Dom Constraint * Dict = (:-)
type Cod Constraint * Dict = (->)
type Dom Constraint * ((:-) a) = (:-)
type Cod Constraint * ((:-) a) = (->)
type Dom k Constraint (Vacuous k c) = c
type Cod k Constraint (Vacuous k c) = (:-)
type Dom Constraint (Constraint -> *) (:-) = Op Constraint (:-)
type Cod Constraint (Constraint -> ) (:-) = Nat Constraint (:-) (->)
type Dom (k -> k1) Constraint (FunctorOf k k1 p q) = Nat k k1 p q
type Cod (k -> k1) Constraint (FunctorOf k k1 p q) = (:-)

newtype a :- b :: Constraint -> Constraint -> * infixr 9

Constructors

Sub (a -> Dict b)

Instances

Category Constraint (:-)
Category' Constraint (:-)
Identified Constraint (:-)
Composed Constraint (:-)
Functor Constraint * ((:-) b)
() :=> (Eq ((:-) a b))
() :=> (Ord ((:-) a b))
() :=> (Show ((:-) a b))
Functor Constraint (Constraint -> *) (:-)
FullyFaithful Constraint (Constraint -> *) (:-)
Eq ((:-) a b)
(Typeable Constraint p, Typeable Constraint q, p, q) => Data ((:-) p q)
Ord ((:-) a b)
Show ((:-) a b)
Typeable (Constraint -> Constraint -> *) (:-)
type Ob Constraint (:-) = Vacuous Constraint (:-)
type Dom Constraint * ((:-) a) = (:-)
type Cod Constraint * ((:-) a) = (->)
type Dom Constraint (Constraint -> *) (:-) = Op Constraint (:-)
type Cod Constraint (Constraint -> ) (:-) = Nat Constraint (:-) (->)

data Dict $a :: Constraint -> * where

Capture a dictionary for a given constraint

Constructors

Dict :: a => Dict a

Instances

Functor Constraint * Dict
FullyFaithful Constraint * Dict
a :=> (Read (Dict a))
a :=> (Monoid (Dict a))
a :=> (Enum (Dict a))
a :=> (Bounded (Dict a))
() :=> (Eq (Dict a))
() :=> (Ord (Dict a))
() :=> (Show (Dict a))
a => Bounded (Dict a)
a => Enum (Dict a)
Eq (Dict a)
(Typeable Constraint p, p) => Data (Dict p)
Ord (Dict a)
a => Read (Dict a)
Show (Dict a)
a => Monoid (Dict a)
Typeable (Constraint -> *) Dict
type Dom Constraint * Dict = (:-)
type Cod Constraint * Dict = (->)

(\\) :: a => (b -> r) -> (:-) a b -> r infixl 1

Given that a :- b, derive something that needs a context b, using the context a

sub :: (a => Proxy a -> Dict b) -> a :- b Source

class Class b h | h -> b where

Reify the relationship between a class and its superclass constraints as a class

Methods

cls :: (:-) h b

Instances

Class () ()
Class () (Bounded a)
Class () (Enum a)
Class () (Eq a)
Class () (Monad f)
Class () (Functor f)
Class () (Num a)
Class () (Read a)
Class () (Show a)
Class () (Monoid a)
Class () (Class b a)
Class () ((:=>) b a)
Class b a => () :=> (Class b a)
Category Constraint c => Class a (Id Constraint c a)
Class (Eq a) (Ord a)
Class (Fractional a) (Floating a)
Class (Monad f) (MonadPlus f)
Class (Functor f) (Applicative f)
Class (Num a) (Fractional a)
Class (Applicative f) (Alternative f)
(Category k c, Category k1 d, Category Constraint e) => Class (f (g a)) (Compose k k Constraint c d e f g a)
Class (Num a, Ord a) (Real a)
Class (Real a, Fractional a) (RealFrac a)
Class (Real a, Enum a) (Integral a)
Class (RealFrac a, Floating a) (RealFloat a)

class b :=> h | h -> b where infixr 9

Reify the relationship between an instance head and its body as a class

Methods

ins :: (:-) b h

Instances

() :=> ()
a :=> (Read (Dict a))
a :=> (Monoid (Dict a))
a :=> (Enum (Dict a))
a :=> (Bounded (Dict a))
() :=> (Alternative [])
() :=> (Alternative Maybe)
() :=> (Bounded Bool)
() :=> (Bounded Char)
() :=> (Bounded Int)
() :=> (Bounded Ordering)
() :=> (Bounded ())
() :=> (Enum Bool)
() :=> (Enum Char)
() :=> (Enum Double)
() :=> (Enum Float)
() :=> (Enum Int)
() :=> (Enum Integer)
() :=> (Enum Ordering)
() :=> (Enum ())
() :=> (Eq Bool)
() :=> (Eq Double)
() :=> (Eq Float)
() :=> (Eq Int)
() :=> (Eq Integer)
() :=> (Eq ())
() :=> (Eq (Dict a))
() :=> (Eq ((:-) a b))
() :=> (Floating Double)
() :=> (Floating Float)
() :=> (Fractional Double)
() :=> (Fractional Float)
() :=> (Integral Int)
() :=> (Integral Integer)
() :=> (Monad ((->) a))
() :=> (Monad [])
() :=> (Monad IO)
() :=> (Monad (Either a))
() :=> (Functor ((->) a))
() :=> (Functor [])
() :=> (Functor IO)
() :=> (Functor (Either a))
() :=> (Functor ((,) a))
() :=> (Functor Maybe)
() :=> (Num Double)
() :=> (Num Float)
() :=> (Num Int)
() :=> (Num Integer)
() :=> (Ord Bool)
() :=> (Ord Char)
() :=> (Ord Double)
() :=> (Ord Float)
() :=> (Ord Int)
() :=> (Ord Integer)
() :=> (Ord ())
() :=> (Ord (Dict a))
() :=> (Ord ((:-) a b))
() :=> (Read Bool)
() :=> (Read Char)
() :=> (Read Ordering)
() :=> (Read ())
() :=> (Real Double)
() :=> (Real Float)
() :=> (Real Int)
() :=> (Real Integer)
() :=> (RealFloat Double)
() :=> (RealFloat Float)
() :=> (RealFrac Double)
() :=> (RealFrac Float)
() :=> (Show Bool)
() :=> (Show Char)
() :=> (Show Ordering)
() :=> (Show ())
() :=> (Show (Dict a))
() :=> (Show ((:-) a b))
() :=> (MonadPlus [])
() :=> (MonadPlus Maybe)
() :=> (Applicative ((->) a))
() :=> (Applicative [])
() :=> (Applicative IO)
() :=> (Applicative (Either a))
() :=> (Applicative Maybe)
() :=> (Monoid [a])
() :=> (Monoid Ordering)
() :=> (Monoid ())
Class () ((:=>) b a)
Class b a => () :=> (Class b a)
(:=>) b a => () :=> ((:=>) b a)
Category Constraint c => a :=> (Id Constraint c a)
(Eq a) :=> (Eq [a])
(Eq a) :=> (Eq (Maybe a))
(Eq a) :=> (Eq (Complex a))
(Eq a) :=> (Eq (Ratio a))
(Integral a) :=> (RealFrac (Ratio a))
(Integral a) :=> (Real (Ratio a))
(Integral a) :=> (Ord (Ratio a))
(Integral a) :=> (Num (Ratio a))
(Integral a) :=> (Fractional (Ratio a))
(Integral a) :=> (Enum (Ratio a))
(Monad m) :=> (Functor (WrappedMonad m))
(Monad m) :=> (Applicative (WrappedMonad m))
(Ord a) :=> (Ord (Maybe a))
(Ord a) :=> (Ord [a])
(Read a) :=> (Read (Complex a))
(Read a) :=> (Read [a])
(Read a) :=> (Read (Maybe a))
(RealFloat a) :=> (Num (Complex a))
(RealFloat a) :=> (Fractional (Complex a))
(RealFloat a) :=> (Floating (Complex a))
(Show a) :=> (Show (Complex a))
(Show a) :=> (Show [a])
(Show a) :=> (Show (Maybe a))
(MonadPlus m) :=> (Alternative (WrappedMonad m))
(Monoid a) :=> (Monoid (Maybe a))
(Monoid a) :=> (Applicative ((,) a))
(Category k c, Category k1 d, Category Constraint e) => (f (g a)) :=> (Compose k k Constraint c d e f g a)
(Bounded a, Bounded b) :=> (Bounded (a, b))
(Eq a, Eq b) :=> (Eq (a, b))
(Eq a, Eq b) :=> (Eq (Either a b))
(Integral a, Show a) :=> (Show (Ratio a))
(Integral a, Read a) :=> (Read (Ratio a))
(Ord a, Ord b) :=> (Ord (a, b))
(Ord a, Ord b) :=> (Ord (Either a b))
(Read a, Read b) :=> (Read (a, b))
(Read a, Read b) :=> (Read (Either a b))
(Show a, Show b) :=> (Show (a, b))
(Show a, Show b) :=> (Show (Either a b))
(Monoid a, Monoid b) :=> (Monoid (a, b))

Op

newtype Yoneda p a b Source

The Yoneda embedding.

Yoneda_C :: C -> [ C^op, Set ]

Constructors

Op
Fields getOp :: p b a

Instances

(Category k p, (~) (k -> k -> ) (Op k p) (Yoneda k p)) => Functor k (Yoneda k p a)
(Category k p, (~) (k -> k -> *) (Op k p) (Yoneda k p)) => Category' k (Yoneda k p)
(Category k p, (~) (k -> k -> ) (Op k p) (Yoneda k p)) => Functor k (k -> ) (Yoneda k p)
type Dom k * (Yoneda k p a) = Yoneda k p
type Cod k * (Yoneda k p a) = (->)
type Ob k (Yoneda k p) = Ob k p
type Dom k (k -> *) (Yoneda k p) = p
type Cod k (k -> ) (Yoneda k p) = Nat k (Yoneda k p) (->)

type family Op p :: i -> i -> * Source

Equations

Op (Yoneda p) = p
Op p = Yoneda p

type Opd f = Op (Dom f) Source

Nat

data Nat p q f g where Source

Constructors

Nat :: (FunctorOf p q f, FunctorOf p q g) => (forall a. Ob p a => q (f a) (g a)) -> Nat p q f g
Fields runNat :: forall a. Ob p a => q (f a) (g a)

Instances

(Category' k p, Category k1 q) => Functor (k -> k) * (Nat k k p q a)
(Category' k p, Category k1 q) => Functor (k -> k) ((k -> k) -> *) (Nat k k p q)
(Category' k p, Category' k1 q) => Category' (k -> k) (Nat k k p q)
(Category k c, Identified k1 d) => Identified (k -> k) (Nat k k c d)
(Category k c, Composed k1 d) => Composed (k -> k) (Nat k k c d)
type Dom (k -> k1) * (Nat k k1 p q f) = Nat k k1 p q
type Cod (k -> k1) * (Nat k k1 p q f) = (->)
type Dom (k -> k1) ((k -> k1) -> *) (Nat k k1 p q) = Op (k -> k1) (Nat k k1 p q)
type Cod (k -> k1) ((k -> k1) -> ) (Nat k k1 p q) = Nat (k -> k1) (Nat k k1 p q) (->)
type Ob (k -> k1) (Nat k k1 p q) = FunctorOf k k1 p q

type NatId p = Endo (Nat (Dom p) (Cod p)) p Source

type Endo p a = p a a Source

nat :: (Category p, Category q, FunctorOf p q f, FunctorOf p q g) => (forall a. Ob p a => Endo p a -> q (f a) (g a)) -> Nat p q f g Source

(!) :: Nat p q f g -> p a a -> q (f a) (g a) infixr 1 Source

type Presheaves p = Nat (Op p) (->) Source

type Copresheaves p = Nat p (->) Source

type family NatDom f :: i -> i -> * Source

Equations

NatDom (Nat p q) = p

type family NatCod f :: j -> j -> * Source

Equations

NatCod (Nat p q) = q

Prelude

($) :: (a -> b) -> a -> b infixr 0

Application operator. This operator is redundant, since ordinary application (f x) means the same as (f $ x). However, $ has low, right-associative binding precedence, so it sometimes allows parentheses to be omitted; for example:

    f $ g $ h x  =  f (g (h x))

It is also useful in higher-order situations, such as map ($ 0) xs, or zipWith ($) fs xs.

data Either a b :: * -> * -> *

The Either type represents values with two possibilities: a value of type Either a b is either Left a or Right b.

The Either type is sometimes used to represent a value which is either correct or an error; by convention, the Left constructor is used to hold an error value and the Right constructor is used to hold a correct value (mnemonic: "right" also means "correct").

Constructors

Left a
Right b

Instances

Tensor' * Either
Semitensor * Either
Comonoid' * Either Void
Cosemigroup * Either Void
Monoid' * Either Void
Semigroup * Either Void
Functor * * (Either a)
() :=> (Monad (Either a))
() :=> (Functor (Either a))
() :=> (Applicative (Either a))
Functor * (* -> *) Either
Monad (Either e)
Functor (Either a)
Applicative (Either e)
Generic1 (Either a)
(Eq a, Eq b) => Eq (Either a b)
(Ord a, Ord b) => Ord (Either a b)
(Read a, Read b) => Read (Either a b)
(Show a, Show b) => Show (Either a b)
Generic (Either a b)
Semigroup (Either a b)
Typeable (* -> * -> *) Either
(Category k p, Category k1 q) => Functor (Either k k) * (Coproduct k k p q a)
(Eq a, Eq b) :=> (Eq (Either a b))
(Ord a, Ord b) :=> (Ord (Either a b))
(Read a, Read b) :=> (Read (Either a b))
(Show a, Show b) :=> (Show (Either a b))
(Category k p, Category k1 q) => Functor (Either k k) (Either k k -> *) (Coproduct k k p q)
(Category k p, Category k1 q) => Category' (Either k k) (Coproduct k k p q)
type I * Either = Void
type Dom * * (Either a) = (->)
type Cod * * (Either a) = (->)
type Dom * (* -> *) Either = (->)
type Cod * (* -> ) Either = Nat * (->) (->)
type Rep1 (Either a) = D1 D1Either ((:+:) (C1 C1_0Either (S1 NoSelector (Rec0 a))) (C1 C1_1Either (S1 NoSelector Par1)))
type Rep (Either a b) = D1 D1Either ((:+:) (C1 C1_0Either (S1 NoSelector (Rec0 a))) (C1 C1_1Either (S1 NoSelector (Rec0 b))))
type (==) (Either k k1) a b = EqEither k k1 a b
type Dom (Either k k1) * (Coproduct k k1 p q a) = Coproduct k k1 p q
type Cod (Either k k1) * (Coproduct k k1 p q a) = (->)
type Dom (Either k k1) (Either k k1 -> *) (Coproduct k k1 p q) = Op (Either k k1) (Coproduct k k1 p q)
type Cod (Either k k1) (Either k k1 -> ) (Coproduct k k1 p q) = Nat (Either k k1) (Coproduct k k1 p q) (->)
type Ob (Either k k1) (Coproduct k k1 p q) = CoproductOb k k1 p q

newtype Fix f a Source

Constructors

In
Fields out :: f (Fix f a) a

Instances

FunctorOf * (* -> ) (->) (Nat * (->) (->)) p => Functor * * (Fix p)
Functor (* -> * -> ) ( -> *) Fix
type Dom * * (Fix f) = (->)
type Cod * * (Fix f) = (->)
type Dom (* -> * -> ) ( -> ) Fix = Nat (* -> ) (->) (Nat * (->) (->))
type Cod (* -> * -> ) ( -> ) Fix = Nat * (->) (->)

FunctorOf * (* -> ) (->) (Nat * (->) (->)) p => Functor * * (Fix p)
Functor (* -> * -> ) ( -> *) Fix
type Dom * * (Fix f) = (->)
type Cod * * (Fix f) = (->)
type Dom (* -> * -> ) ( -> ) Fix = Nat (* -> ) (->) (Nat * (->) (->))
type Cod (* -> * -> ) ( -> ) Fix = Nat * (->) (->)

Category' * (->)
Category' Constraint (:-)
(Category k p, (~) (k -> k -> *) (Op k p) (Yoneda k p)) => Category' k (Yoneda k p)
Category' k (Unit k k)
(Category' k p, Category' k1 q) => Category' (k -> k) (Nat k k p q)
(Category k p, Category k1 q) => Category' (Either k k) (Coproduct k k p q)
(Category k p, Category k1 q) => Category' ((,) k k) (Product k k p q)