Data.Quiver.Bifunctor

The category of quivers forms a closed monoidal category in two ways, under ProductQ or ComposeQ. The relations between these and their adjoints can be characterized by typeclasses below.

Documentation

class (forall q. QFunctor (prod q)) => QBifunctor prod where

A endo-bifunctor on the category of quivers, covariant in both its arguments.

qbimap id id = id

qbimap (g . f) (i . h) = qbimap g i . qbimap f h

Methods

qbimap :: (forall x y. p x y -> p' x y) -> (forall x y. q x y -> q' x y) -> prod p q x y -> prod p' q' x y

Instances

QBifunctor (ProductQ :: (k1 -> k2 -> Type) -> (k1 -> k2 -> Type) -> k1 -> k2 -> Type)

Defined in Data.Quiver.Bifunctor

Methods

qbimap :: (forall (x :: k) (y :: k). p x y -> p' x y) -> (forall (x :: k) (y :: k). q x y -> q' x y) -> ProductQ p q x y -> ProductQ p' q' x y

QBifunctor (ComposeQ :: (k1 -> k3 -> Type) -> (k2 -> k1 -> Type) -> k2 -> k3 -> Type)

Defined in Data.Quiver.Bifunctor

Methods

qbimap :: (forall (x :: k) (y :: k). p x y -> p' x y) -> (forall (x :: k) (y :: k). q x y -> q' x y) -> ComposeQ p q x y -> ComposeQ p' q' x y

class (forall q. QFunctor (hom q)) => QProfunctor hom where

A endo-bifunctor on the category of quivers, contravariant in its first argument, and covariant in its second argument.

qdimap id id = id

qdimap (g . f) (i . h) = qdimap f i . qdimap g h

Methods

qdimap :: (forall x y. p' x y -> p x y) -> (forall x y. q x y -> q' x y) -> hom p q x y -> hom p' q' x y

Instances

QProfunctor (HomQ :: (k1 -> k2 -> Type) -> (k1 -> k2 -> Type) -> k1 -> k2 -> Type)

Defined in Data.Quiver.Bifunctor

Methods

qdimap :: (forall (x :: k) (y :: k). p' x y -> p x y) -> (forall (x :: k) (y :: k). q x y -> q' x y) -> HomQ p q x y -> HomQ p' q' x y

QProfunctor (RightQ :: (k3 -> k1 -> Type) -> (k2 -> k1 -> Type) -> k2 -> k3 -> Type)

Defined in Data.Quiver.Bifunctor

Methods

qdimap :: (forall (x :: k) (y :: k). p' x y -> p x y) -> (forall (x :: k) (y :: k). q x y -> q' x y) -> RightQ p q x y -> RightQ p' q' x y

QProfunctor (LeftQ :: (k1 -> k2 -> Type) -> (k1 -> k3 -> Type) -> k2 -> k3 -> Type)

Defined in Data.Quiver.Bifunctor

Methods

qdimap :: (forall (x :: k) (y :: k). p' x y -> p x y) -> (forall (x :: k) (y :: k). q x y -> q' x y) -> LeftQ p q x y -> LeftQ p' q' x y

class QBifunctor prod => QMonoidal prod unit | prod -> unit where

A monoidal category structure on the category of quivers.

This consists of a product bifunctor, a unit object and structure morphisms, an invertible associator,

qassoc . qdisassoc = id

qdisassoc . qassoc = id

and invertible left and right unitors,

qintro1 . qelim1 = id

qelim1 . qintro1 = id

qintro2 . qelim2 = id

qelim2 . qintro2 = id

that satisfy the pentagon equation,

qbimap id qassoc . qassoc . qbimap qassoc id = qassoc . qassoc

and the triangle equation,

qbimap id qelim1 . qassoc = qbimap qelim2 id

Methods

qintro1 :: p x y -> prod unit p x y

qintro2 :: p x y -> prod p unit x y

qelim1 :: prod unit p x y -> p x y

qelim2 :: prod p unit x y -> p x y

qassoc :: prod (prod p q) r x y -> prod p (prod q r) x y

qdisassoc :: prod p (prod q r) x y -> prod (prod p q) r x y

Instances

QMonoidal (ProductQ :: (k1 -> k2 -> Type) -> (k1 -> k2 -> Type) -> k1 -> k2 -> Type) (KQ () :: k1 -> k2 -> Type)

Defined in Data.Quiver.Bifunctor

Methods

qintro1 :: p x y -> ProductQ (KQ ()) p x y

qintro2 :: p x y -> ProductQ p (KQ ()) x y

qelim1 :: ProductQ (KQ ()) p x y -> p x y

qelim2 :: ProductQ p (KQ ()) x y -> p x y

qassoc :: ProductQ (ProductQ p q) r x y -> ProductQ p (ProductQ q r) x y

qdisassoc :: ProductQ p (ProductQ q r) x y -> ProductQ (ProductQ p q) r x y

QMonoidal (ComposeQ :: (k -> k -> Type) -> (k -> k -> Type) -> k -> k -> Type) (ReflQ () :: k -> k -> Type)

Defined in Data.Quiver.Bifunctor

Methods

qintro1 :: p x y -> ComposeQ (ReflQ ()) p x y

qintro2 :: p x y -> ComposeQ p (ReflQ ()) x y

qelim1 :: ComposeQ (ReflQ ()) p x y -> p x y

qelim2 :: ComposeQ p (ReflQ ()) x y -> p x y

qassoc :: ComposeQ (ComposeQ p q) r x y -> ComposeQ p (ComposeQ q r) x y

qdisassoc :: ComposeQ p (ComposeQ q r) x y -> ComposeQ (ComposeQ p q) r x y

class (QBifunctor prod, QProfunctor lhom, QProfunctor rhom) => QClosed prod lhom rhom | prod -> lhom, prod -> rhom where

A (bi-)closed monoidal category is one for which the products prod _ p and prod p _ both have right adjoint functors, the left and right residuals lhom p and rhom p. If prod is symmetric then the left and right residuals coincide as the internal hom.

qcurry  . quncurry = id

qflurry . qunflurry = id

qlev . (qcurry f `qbimap` id) = f

qcurry (qlev . (g `qbimap` id)) = g

qrev . (id `qbimap` qflurry f) = f

qflurry (qrev . (id `qbimap` g)) = g

Methods

qlev :: prod (lhom p q) p x y -> q x y

qrev :: prod p (rhom p q) x y -> q x y

qcurry :: (forall x y. prod p q x y -> r x y) -> p x y -> lhom q r x y

quncurry :: (forall x y. p x y -> lhom q r x y) -> prod p q x y -> r x y

qflurry :: (forall x y. prod p q x y -> r x y) -> q x y -> rhom p r x y

qunflurry :: (forall x y. q x y -> rhom p r x y) -> prod p q x y -> r x y

Instances

QClosed (ProductQ :: (k1 -> k2 -> Type) -> (k1 -> k2 -> Type) -> k1 -> k2 -> Type) (HomQ :: (k1 -> k2 -> Type) -> (k1 -> k2 -> Type) -> k1 -> k2 -> Type) (HomQ :: (k1 -> k2 -> Type) -> (k1 -> k2 -> Type) -> k1 -> k2 -> Type)

Defined in Data.Quiver.Bifunctor

Methods

qlev :: ProductQ (HomQ p q) p x y -> q x y

qrev :: ProductQ p (HomQ p q) x y -> q x y

qcurry :: (forall (x :: k) (y :: k). ProductQ p q x y -> r x y) -> p x y -> HomQ q r x y

quncurry :: (forall (x :: k) (y :: k). p x y -> HomQ q r x y) -> ProductQ p q x y -> r x y

qflurry :: (forall (x :: k) (y :: k). ProductQ p q x y -> r x y) -> q x y -> HomQ p r x y

qunflurry :: (forall (x :: k) (y :: k). q x y -> HomQ p r x y) -> ProductQ p q x y -> r x y

QClosed (ComposeQ :: (k3 -> k1 -> Type) -> (k2 -> k3 -> Type) -> k2 -> k1 -> Type) (LeftQ :: (k2 -> k3 -> Type) -> (k2 -> k1 -> Type) -> k3 -> k1 -> Type) (RightQ :: (k3 -> k1 -> Type) -> (k2 -> k1 -> Type) -> k2 -> k3 -> Type)

Defined in Data.Quiver.Bifunctor

Methods

qlev :: ComposeQ (LeftQ p q) p x y -> q x y

qrev :: ComposeQ p (RightQ p q) x y -> q x y

qcurry :: (forall (x :: k) (y :: k). ComposeQ p q x y -> r x y) -> p x y -> LeftQ q r x y

quncurry :: (forall (x :: k) (y :: k). p x y -> LeftQ q r x y) -> ComposeQ p q x y -> r x y

qflurry :: (forall (x :: k) (y :: k). ComposeQ p q x y -> r x y) -> q x y -> RightQ p r x y

qunflurry :: (forall (x :: k) (y :: k). q x y -> RightQ p r x y) -> ComposeQ p q x y -> r x y