(Corepresentable j * k p, Corepresentable i * j q, Composed k (Hom k *), Functor j k (Corep j * k p), Category j (Hom j *), Category k (Hom k *)) => Corepresentable i * k (Prof j k i p q) | |
(Representable k * j p, Representable j * i q, Composed i (Hom i *), Functor j i (Rep j * i q), Category i (Hom i *), Category j (Hom j *)) => Representable k * i (Prof j k i p q) | |
Post k1 (k -> *) (Contravariant * k) p => Contravariant * k (Prof k k k p q a) | |
Post k1 (k -> *) (Functor k *) p => Functor k * (Prof k k k p q a) | |
Functor k (k1 -> *) q => Functor k (k -> *) (Prof k k k p q) | |
Contravariant (k1 -> *) k q => Contravariant (k -> *) k (Prof k k k p q) | |
Curried (k -> k -> *) (k -> k -> *) (k -> k -> *) (Prof k k k) (ProfR k k k) | |
Functor (k -> k -> *) ((k -> k -> *) -> k -> k -> *) (Prof k k k) | |
Functor (k -> k -> *) (k -> k -> *) (Prof k k k p) | |
Category i ((~>) i) => Tensor (i -> i -> *) (Prof i i i) | |
Category i ((~>) i) => Semitensor (i -> i -> *) (Prof i i i) | |
type Corep i * k (Prof j k i p q) = · k j i (Corep j * k p) (Corep i * j q) | |
type Rep k * i (Prof j k i p q) = · i j k (Rep j * i q) (Rep k * j p) | |
type Curryable (k2 -> k1 -> *) (k2 -> k -> *) (k -> k1 -> *) (Prof k k1 k2) = Const (k -> k1 -> *) Constraint () | |
type I (k -> k -> *) (Prof k k k) = (~>) k | |
type Tensorable (k -> k -> *) (Prof k k k) = Profunctor k k * | |