Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Duploid

Documentation

data DUPLOID (adj :: p +-> n) Source Comments #

Constructors

N n
P p

Instances

Instances details

(Adjunction adj, StrongMonoidalRep adj) => Monoidal (DUPLOID adj) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Duploid

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.Duploid type Unit = 'P (Unit :: p) :: DUPLOID adj

Methods

withOb2 :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Comments #

leftUnitor :: forall (a :: DUPLOID adj). Ob a => ((Unit :: DUPLOID adj) ** a) ~> a Source Comments #

leftUnitorInv :: forall (a :: DUPLOID adj). Ob a => a ~> ((Unit :: DUPLOID adj) ** a) Source Comments #

rightUnitor :: forall (a :: DUPLOID adj). Ob a => (a ** (Unit :: DUPLOID adj)) ~> a Source Comments #

rightUnitorInv :: forall (a :: DUPLOID adj). Ob a => a ~> (a ** (Unit :: DUPLOID adj)) Source Comments #

associator :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) (c :: DUPLOID adj). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Comments #

associatorInv :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) (c :: DUPLOID adj). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Comments #

StrongSymMonAdj adj => SymMonoidal (DUPLOID adj) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Duploid

Methods

swap :: forall (a :: DUPLOID adj) (b :: DUPLOID adj). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Comments #

Adjunction adj => CategoryOf (DUPLOID adj) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Duploid

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Duploid type (~>) = Duploid :: DUPLOID adj -> DUPLOID adj -> Type

Adjunction adj => Promonad (Duploid :: DUPLOID adj -> DUPLOID adj -> Type) Source Comments #

ATTENTION: a duploid is not associative, so not really a promonad/category!

Instance details

Defined in Proarrow.Category.Instance.Duploid

Methods

id :: forall (a :: DUPLOID adj). Ob a => Duploid a a Source Comments #

(.) :: forall (b :: DUPLOID adj) (c :: DUPLOID adj) (a :: DUPLOID adj). Duploid b c -> Duploid a b -> Duploid a c Source Comments #

(Adjunction adj, StrongMonoidalRep adj) => MonoidalProfunctor (Duploid :: DUPLOID adj -> DUPLOID adj -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Duploid

Methods

par0 :: Duploid (Unit :: DUPLOID adj) (Unit :: DUPLOID adj) Source Comments #

par :: forall (x1 :: DUPLOID adj) (x2 :: DUPLOID adj) (y1 :: DUPLOID adj) (y2 :: DUPLOID adj). Duploid x1 x2 -> Duploid y1 y2 -> Duploid (x1 ** y1) (x2 ** y2) Source Comments #

Adjunction adj => Profunctor (Duploid :: DUPLOID adj -> DUPLOID adj -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Duploid

Methods

dimap :: forall (c :: DUPLOID adj) (a :: DUPLOID adj) (b :: DUPLOID adj) (d :: DUPLOID adj). (c ~> a) -> (b ~> d) -> Duploid a b -> Duploid c d Source Comments #

(\\) :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) r. ((Ob a, Ob b) => r) -> Duploid a b -> r Source Comments #

type Unit Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Duploid

type Unit = 'P (Unit :: p) :: DUPLOID adj

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Duploid

type (~>) = Duploid :: DUPLOID adj -> DUPLOID adj -> Type

type Ob (x :: DUPLOID adj) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Duploid

type Ob (x :: DUPLOID adj) = IsPN x

type (x :: DUPLOID adj) ** (y :: DUPLOID adj) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Duploid

type (x :: DUPLOID adj) ** (y :: DUPLOID adj) = 'P (Pos x ** Pos y) :: DUPLOID adj

data SDuploidObj (x :: DUPLOID adj) where Source Comments #

Constructors

SN :: forall {n} {p} {adj :: p +-> n} (x1 :: n). Ob x1 => SDuploidObj ('N x1 :: DUPLOID adj)
SP :: forall {p} {n} {adj :: p +-> n} (x1 :: p). Ob x1 => SDuploidObj ('P x1 :: DUPLOID adj)

class IsPN (x :: DUPLOID adj) where Source Comments #

Methods

pn :: SDuploidObj x Source Comments #

withPosOb :: (Ob (Pos x) => r) -> r Source Comments #

withNegOb :: (Ob (Neg x) => r) -> r Source Comments #

Instances

Instances details

(Ob x, Corepresentable adj) => IsPN ('N x :: DUPLOID adj) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Duploid Methods pn :: SDuploidObj ('N x :: DUPLOID adj) Source Comments # withPosOb :: (Ob (Pos ('N x :: DUPLOID adj)) => r) -> r Source Comments # withNegOb :: (Ob (Neg ('N x :: DUPLOID adj)) => r) -> r Source Comments #
(Ob x, Representable adj) => IsPN ('P x :: DUPLOID adj) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Duploid Methods pn :: SDuploidObj ('P x :: DUPLOID adj) Source Comments # withPosOb :: (Ob (Pos ('P x :: DUPLOID adj)) => r) -> r Source Comments # withNegOb :: (Ob (Neg ('P x :: DUPLOID adj)) => r) -> r Source Comments #

type family Pos (x :: DUPLOID adj) :: p where ... Source Comments #

Equations

Pos ('P a :: DUPLOID adj) = a
Pos ('N a :: DUPLOID adj) = adj %% a

type family Neg (x :: DUPLOID adj) :: n where ... Source Comments #

Equations

Neg ('P a :: DUPLOID adj) = adj % a
Neg ('N a :: DUPLOID adj) = a

data Duploid (x :: DUPLOID adj) (y :: DUPLOID adj) where Source Comments #

Constructors

Duploid :: forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj) (y :: DUPLOID adj). (Ob x, Ob y) => adj (Neg x) (Pos y) -> Duploid x y

Instances

Instances details

Adjunction adj => Promonad (Duploid :: DUPLOID adj -> DUPLOID adj -> Type) Source Comments #	ATTENTION: a duploid is not associative, so not really a promonad/category!
Instance details Defined in Proarrow.Category.Instance.Duploid Methods id :: forall (a :: DUPLOID adj). Ob a => Duploid a a Source Comments # (.) :: forall (b :: DUPLOID adj) (c :: DUPLOID adj) (a :: DUPLOID adj). Duploid b c -> Duploid a b -> Duploid a c Source Comments #
(Adjunction adj, StrongMonoidalRep adj) => MonoidalProfunctor (Duploid :: DUPLOID adj -> DUPLOID adj -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Duploid Methods par0 :: Duploid (Unit :: DUPLOID adj) (Unit :: DUPLOID adj) Source Comments # par :: forall (x1 :: DUPLOID adj) (x2 :: DUPLOID adj) (y1 :: DUPLOID adj) (y2 :: DUPLOID adj). Duploid x1 x2 -> Duploid y1 y2 -> Duploid (x1 y1) (x2 y2) Source Comments #
Adjunction adj => Profunctor (Duploid :: DUPLOID adj -> DUPLOID adj -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Duploid Methods dimap :: forall (c :: DUPLOID adj) (a :: DUPLOID adj) (b :: DUPLOID adj) (d :: DUPLOID adj). (c ~> a) -> (b ~> d) -> Duploid a b -> Duploid c d Source Comments # (\\) :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) r. ((Ob a, Ob b) => r) -> Duploid a b -> r Source Comments #

(•) :: forall {j} {k} {adj :: j +-> k} (x :: DUPLOID adj) (y :: k) (z :: DUPLOID adj). Corepresentable adj => (('N y :: DUPLOID adj) ~> z) -> (x ~> ('N y :: DUPLOID adj)) -> x ~> z Source Comments #

(◦) :: forall {j} {k} {adj :: j +-> k} (x :: DUPLOID adj) (y :: j) (z :: DUPLOID adj). Representable adj => (('P y :: DUPLOID adj) ~> z) -> (x ~> ('P y :: DUPLOID adj)) -> x ~> z Source Comments #

fromThunkable :: forall {p} {n} {adj :: p +-> n} (x :: p) (y :: p). Adjunction adj => (x ~> y) -> ('P x :: DUPLOID adj) ~> ('P y :: DUPLOID adj) Source Comments #

fromLinear :: forall {p} {n} {adj :: p +-> n} (x :: n) (y :: n). Adjunction adj => (x ~> y) -> ('N x :: DUPLOID adj) ~> ('N y :: DUPLOID adj) Source Comments #

type Up (x :: DUPLOID adj1) = 'P (Pos x) :: DUPLOID adj Source Comments #

shiftPosObj :: forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj). (Adjunction adj, Ob x) => x ~> (Up x :: DUPLOID adj) Source Comments #

shiftPosLift :: forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj) (y :: DUPLOID adj). Adjunction adj => (x ~> y) -> (Up x :: DUPLOID adj) ~> y Source Comments #

shiftPos :: forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj) (y :: DUPLOID adj). Adjunction adj => (x ~> y) -> (Up x :: DUPLOID adj) ~> (Up y :: DUPLOID adj) Source Comments #

type Dn (x :: DUPLOID adj1) = 'N (Neg x) :: DUPLOID adj Source Comments #

shiftNegObj :: forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj). (Adjunction adj, Ob x) => (Dn x :: DUPLOID adj) ~> x Source Comments #

shiftNegLift :: forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj) (y :: DUPLOID adj). Adjunction adj => (x ~> y) -> x ~> (Dn y :: DUPLOID adj) Source Comments #

shiftNeg :: forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj) (y :: DUPLOID adj). Adjunction adj => (x ~> y) -> (Dn x :: DUPLOID adj) ~> (Dn y :: DUPLOID adj) Source Comments #

type StrongSymMonAdj (adj :: p +-> n) = (Adjunction adj, StrongMonoidalRep adj, SymMonoidal p) Source Comments #