hask-0: Categories

Copyright(c) Edward Kmett 2014
LicenseBSD3
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Hask.Prof

Description

Prof  :: (j -> k -> *) -> (i -> j -> *) -> i -> k -> *
ProfR :: (i -> j -> *) -> (i -> k -> *) -> j -> k -> *

Documentation

data Prof :: (j -> k -> *) -> (i -> j -> *) -> i -> k -> * where Source

Constructors

Prof :: p b c -> q a b -> Prof p q a c 

Instances

(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 * 

associateProf :: Iso (Prof (Prof p q) r) (Prof (Prof p' q') r') (Prof p (Prof q r)) (Prof p' (Prof q' r')) Source

whiskerProfL :: (p ~> q) -> Prof p r ~> Prof q r Source

whiskerProfR :: (p ~> q) -> Prof l p ~> Prof l q Source

lambdaProf :: (Category k, k ~ Hom, Post Functor p) => Iso (Prof k p) (Prof k q) p q Source

rhoProf :: (Category k, k ~ Hom, Contravariant p) => Iso (Prof p k) (Prof q k) p q Source

newtype ProfR p q a b Source

Constructors

ProfR 

Fields

runProfR :: forall x. p x a -> q x b
 

Instances

Post k2 (k -> *) (Contravariant * k) q => Contravariant * k (ProfR k k k p q a) 
Post k2 (k -> *) (Functor k *) q => Functor k * (ProfR k k k p q a) 
Post k1 (k -> *) (Contravariant * k) p => Functor k (k -> *) (ProfR k k k p q) 
Post k1 (k -> *) (Functor k *) p => Contravariant (k -> *) k (ProfR k k k p q) 
Curried (k -> k -> *) (k -> k -> *) (k -> k -> *) (Prof k k k) (ProfR k k k) 
Contravariant ((k -> k -> *) -> k -> k -> *) (k -> k -> *) (ProfR k k k) 
Functor (k -> k -> *) (k -> k -> *) (ProfR k k k p) 
type I (k -> k -> *) (ProfR k k k) = (~>) k 

iotaProf :: (Category p, p ~ (~>), Contravariant q') => Iso (ProfR p q) (ProfR (~>) q') q q' Source