Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Bicategory.Prof

Documentation

data ProfCl Source Comments #

Constructors

ProfC
ProfRepC
ProfCorepC

type family ProfConstraint (cl :: ProfCl) :: PRO j k -> Constraint Source Comments #

Instances

Instances details

type ProfConstraint 'ProfC Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof type ProfConstraint 'ProfC = Profunctor :: PRO j k -> Constraint
type ProfConstraint 'ProfCorepC Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof type ProfConstraint 'ProfCorepC = Corepresentable :: PRO j k -> Constraint
type ProfConstraint 'ProfRepC Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof type ProfConstraint 'ProfRepC = Representable :: PRO j k -> Constraint

data ProfK (cl :: ProfCl) j k Source Comments #

Constructors

PK (PRO j k)

Instances

Instances details

(forall i j k (p :: PRO i j) (q :: PRO j k). (ProfConstraint cl p, ProfConstraint cl q) => ComposeConstraint cl i j k p q) => Bicategory (ProfK cl :: Type -> Type -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

o :: forall {k1} i j (a :: ProfK cl i j) (b :: ProfK cl i j) (c :: ProfK cl j k1) (d :: ProfK cl j k1). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Comments #

(\\\) :: forall i j (ps :: ProfK cl i j) (qs :: ProfK cl i j) r. ((Ob0 (ProfK cl) i, Ob0 (ProfK cl) j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r Source Comments #

leftUnitor :: forall i j (a :: ProfK cl i j). Obj a -> O (I :: ProfK cl i i) a ~> a Source Comments #

leftUnitorInv :: forall i j (a :: ProfK cl i j). Obj a -> a ~> O (I :: ProfK cl i i) a Source Comments #

rightUnitor :: forall i j (a :: ProfK cl i j). Obj a -> O a (I :: ProfK cl j j) ~> a Source Comments #

rightUnitorInv :: forall i j (a :: ProfK cl i j). Obj a -> a ~> O a (I :: ProfK cl j j) Source Comments #

associator :: forall {j1} {k1} i j2 (a :: ProfK cl i j2) (b :: ProfK cl j2 j1) (c :: ProfK cl j1 k1). Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c) Source Comments #

associatorInv :: forall {j1} {k1} i j2 (a :: ProfK cl i j2) (b :: ProfK cl j2 j1) (c :: ProfK cl j1 k1). Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c Source Comments #

(Profunctor f, Profunctor j) => RightKanExtension ('PK j :: ProfK 'ProfC c d) ('PK f :: ProfK 'ProfC c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Ran ('PK j :: ProfK 'ProfC c d) ('PK f :: ProfK 'ProfC c e)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Ran ('PK j :: ProfK 'ProfC c d) ('PK f :: ProfK 'ProfC c e) = 'PK (Ran ('OP j) f) :: ProfK 'ProfC d e

Methods

ran :: O ('PK j :: ProfK 'ProfC c d) (Ran ('PK j :: ProfK 'ProfC c d) ('PK f :: ProfK 'ProfC c e)) ~> ('PK f :: ProfK 'ProfC c e) Source Comments #

ranUniv :: forall (g :: ProfK 'ProfC d e). Ob g => (O ('PK j :: ProfK 'ProfC c d) g ~> ('PK f :: ProfK 'ProfC c e)) -> g ~> Ran ('PK j :: ProfK 'ProfC c d) ('PK f :: ProfK 'ProfC c e) Source Comments #

(Profunctor f, Profunctor j) => RightKanLift ('PK j :: ProfK 'ProfC d c) ('PK f :: ProfK 'ProfC e c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Rift ('PK j :: ProfK 'ProfC d c) ('PK f :: ProfK 'ProfC e c)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Rift ('PK j :: ProfK 'ProfC d c) ('PK f :: ProfK 'ProfC e c) = 'PK (Rift ('OP j) f) :: ProfK 'ProfC e d

Methods

rift :: O (Rift ('PK j :: ProfK 'ProfC d c) ('PK f :: ProfK 'ProfC e c)) ('PK j :: ProfK 'ProfC d c) ~> ('PK f :: ProfK 'ProfC e c) Source Comments #

riftUniv :: forall (g :: ProfK 'ProfC e d). Ob g => (O g ('PK j :: ProfK 'ProfC d c) ~> ('PK f :: ProfK 'ProfC e c)) -> g ~> Rift ('PK j :: ProfK 'ProfC d c) ('PK f :: ProfK 'ProfC e c) Source Comments #

Adjunction l r => Adjunction ('PK l :: ProfK 'ProfC c d) ('PK r :: ProfK 'ProfC d c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

unit :: (I :: ProfK 'ProfC d d) ~> O ('PK r :: ProfK 'ProfC d c) ('PK l :: ProfK 'ProfC c d) Source Comments #

counit :: O ('PK l :: ProfK 'ProfC c d) ('PK r :: ProfK 'ProfC d c) ~> (I :: ProfK 'ProfC c c) Source Comments #

(IsCategoryOf j cj, IsCategoryOf k ck, Profunctor p) => Bimodule ('PK cj :: ProfK 'ProfC j j) ('PK ck :: ProfK 'ProfC k k) ('PK p :: ProfK 'ProfC j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

leftAction :: O ('PK cj :: ProfK 'ProfC j j) ('PK p :: ProfK 'ProfC j k) ~> ('PK p :: ProfK 'ProfC j k) Source Comments #

rightAction :: O ('PK p :: ProfK 'ProfC j k) ('PK ck :: ProfK 'ProfC k k) ~> ('PK p :: ProfK 'ProfC j k) Source Comments #

Promonad p => Monad ('PK p :: ProfK 'ProfC k k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

eta :: (I :: ProfK 'ProfC k k) ~> ('PK p :: ProfK 'ProfC k k) Source Comments #

mu :: O ('PK p :: ProfK 'ProfC k k) ('PK p :: ProfK 'ProfC k k) ~> ('PK p :: ProfK 'ProfC k k) Source Comments #

CategoryOf (ProfK cl j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Bicategory.Prof type (~>) = Prof :: ProfK cl j k -> ProfK cl j k -> Type

Promonad (Prof :: ProfK cl j k -> ProfK cl j k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

id :: forall (a :: ProfK cl j k). Ob a => Prof a a Source Comments #

(.) :: forall (b :: ProfK cl j k) (c :: ProfK cl j k) (a :: ProfK cl j k). Prof b c -> Prof a b -> Prof a c Source Comments #

Profunctor (Prof :: ProfK cl j k -> ProfK cl j k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

dimap :: forall (c :: ProfK cl j k) (a :: ProfK cl j k) (b :: ProfK cl j k) (d :: ProfK cl j k). (c ~> a) -> (b ~> d) -> Prof a b -> Prof c d Source Comments #

(\\) :: forall (a :: ProfK cl j k) (b :: ProfK cl j k) r. ((Ob a, Ob b) => r) -> Prof a b -> r Source Comments #

type Ob0 (ProfK cl :: Type -> Type -> Type) (k :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Ob0 (ProfK cl :: Type -> Type -> Type) (k :: Type) = (CategoryOf k, ProfConstraint cl ((~>) :: CAT k))

type Ran ('PK j :: ProfK 'ProfC c d) ('PK f :: ProfK 'ProfC c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Ran ('PK j :: ProfK 'ProfC c d) ('PK f :: ProfK 'ProfC c e) = 'PK (Ran ('OP j) f) :: ProfK 'ProfC d e

type Rift ('PK j :: ProfK 'ProfC d c) ('PK f :: ProfK 'ProfC e c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Rift ('PK j :: ProfK 'ProfC d c) ('PK f :: ProfK 'ProfC e c) = 'PK (Rift ('OP j) f) :: ProfK 'ProfC e d

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type I = 'PK ((~>) :: CAT i) :: ProfK cl i i

type O (p :: ProfK cl j1 j2) (q :: ProfK cl j2 k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type O (p :: ProfK cl j1 j2) (q :: ProfK cl j2 k) = 'PK (UN ('PK :: PRO j1 j2 -> ProfK cl j1 j2) p :.: UN ('PK :: PRO j2 k -> ProfK cl j2 k) q) :: ProfK cl j1 k

type UN ('PK :: PRO j k -> ProfK cl j k) ('PK p :: ProfK cl j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type UN ('PK :: PRO j k -> ProfK cl j k) ('PK p :: ProfK cl j k) = p

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type (~>) = Prof :: ProfK cl j k -> ProfK cl j k -> Type

type Ob (p :: ProfK cl j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Ob (p :: ProfK cl j k) = (Is ('PK :: PRO j k -> ProfK cl j k) p, Profunctor (UN ('PK :: PRO j k -> ProfK cl j k) p), ProfConstraint cl (UN ('PK :: PRO j k -> ProfK cl j k) p), ProfConstraint cl ((~>) :: CAT j), ProfConstraint cl ((~>) :: CAT k))

type PROFK = ProfK 'ProfC Source Comments #

data Prof (p :: ProfK cl j k) (q :: ProfK cl j k) where Source Comments #

Constructors

Prof :: forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k) (q :: ProfK cl j k). (Ob p, Ob q) => (UN ('PK :: PRO j k -> ProfK cl j k) p :~> UN ('PK :: PRO j k -> ProfK cl j k) q) -> Prof p q

Instances

Instances details

Promonad (Prof :: ProfK cl j k -> ProfK cl j k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods id :: forall (a :: ProfK cl j k). Ob a => Prof a a Source Comments # (.) :: forall (b :: ProfK cl j k) (c :: ProfK cl j k) (a :: ProfK cl j k). Prof b c -> Prof a b -> Prof a c Source Comments #
Profunctor (Prof :: ProfK cl j k -> ProfK cl j k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods dimap :: forall (c :: ProfK cl j k) (a :: ProfK cl j k) (b :: ProfK cl j k) (d :: ProfK cl j k). (c ~> a) -> (b ~> d) -> Prof a b -> Prof c d Source Comments # (\\) :: forall (a :: ProfK cl j k) (b :: ProfK cl j k) r. ((Ob a, Ob b) => r) -> Prof a b -> r Source Comments #

class ProfConstraint cl (p :.: q) => ComposeConstraint (cl :: ProfCl) i j k (p :: PRO i j) (q :: PRO j k) Source Comments #

Instances

Instances details

ProfConstraint cl (p :.: q) => ComposeConstraint cl i j k (p :: PRO i j) (q :: PRO j k) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof