Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Duploid

Documentation

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

Constructors

N n
P p

Instances

Instances details

(Adjunction adj, StrongMonoidalCorep adj) => Monoidal (DUPLOID adj) Source Github #

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 Github #

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

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

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

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

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

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

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

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 Github #

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

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

(HasBinaryCoproducts p, Adjunction adj) => HasBinaryCoproducts (DUPLOID adj) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Duploid

Methods

withObCoprod :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Github #

lft :: forall (a :: DUPLOID adj) (b :: DUPLOID adj). (Ob a, Ob b) => a ~> (a || b) Source Github #

rgt :: forall (a :: DUPLOID adj) (b :: DUPLOID adj). (Ob a, Ob b) => b ~> (a || b) Source Github #

(|||) :: forall (x :: DUPLOID adj) (a :: DUPLOID adj) (y :: DUPLOID adj). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Github #

(+++) :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) (x :: DUPLOID adj) (y :: DUPLOID adj). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Github #

(HasBinaryProducts n, Adjunction adj) => HasBinaryProducts (DUPLOID adj) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Duploid

Methods

withObProd :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: DUPLOID adj) (b :: DUPLOID adj). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: DUPLOID adj) (b :: DUPLOID adj). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: DUPLOID adj) (x :: DUPLOID adj) (y :: DUPLOID adj). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) (x :: DUPLOID adj) (y :: DUPLOID adj). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

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

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 Github #

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

(Adjunction adj, StrongMonoidalCorep adj) => MonoidalProfunctor (Duploid :: DUPLOID adj -> DUPLOID adj -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Duploid

Methods

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

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 Github #

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

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 Github #

lmap :: forall (c :: DUPLOID adj) (a :: DUPLOID adj) (b :: DUPLOID adj). (c ~> a) -> Duploid a b -> Duploid c b Source Github #

rmap :: forall (b :: DUPLOID adj) (d :: DUPLOID adj) (a :: DUPLOID adj). (b ~> d) -> Duploid a b -> Duploid a d Source Github #

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

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.Duploid

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

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Duploid

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

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

Instance details

Defined in Proarrow.Category.Instance.Duploid

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

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

Instance details

Defined in Proarrow.Category.Instance.Duploid

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

type (a :: DUPLOID adj) || (b :: DUPLOID adj) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Duploid

type (a :: DUPLOID adj) || (b :: DUPLOID adj) = 'P (Pos a || Pos b) :: DUPLOID adj

type (a :: DUPLOID adj) && (b :: DUPLOID adj) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Duploid

type (a :: DUPLOID adj) && (b :: DUPLOID adj) = 'N (Neg a && Neg b) :: DUPLOID adj

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

Constructors

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

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

Methods

pn :: SDuploidObj x Source Github #

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

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

Instances

Instances details

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

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

Equations

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

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

Equations

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

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

Constructors

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

Instances

Instances details

Adjunction adj => Promonad (Duploid :: DUPLOID adj -> DUPLOID adj -> Type) Source Github #	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 Github # (.) :: forall (b :: DUPLOID adj) (c :: DUPLOID adj) (a :: DUPLOID adj). Duploid b c -> Duploid a b -> Duploid a c Source Github #
(Adjunction adj, StrongMonoidalCorep adj) => MonoidalProfunctor (Duploid :: DUPLOID adj -> DUPLOID adj -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Duploid Methods par0 :: Duploid (Unit :: DUPLOID adj) (Unit :: DUPLOID adj) Source Github # 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 Github #
Adjunction adj => Profunctor (Duploid :: DUPLOID adj -> DUPLOID adj -> Type) Source Github #
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 Github # lmap :: forall (c :: DUPLOID adj) (a :: DUPLOID adj) (b :: DUPLOID adj). (c ~> a) -> Duploid a b -> Duploid c b Source Github # rmap :: forall (b :: DUPLOID adj) (d :: DUPLOID adj) (a :: DUPLOID adj). (b ~> d) -> Duploid a b -> Duploid a d Source Github # (\\) :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) r. ((Ob a, Ob b) => r) -> Duploid a b -> r Source Github #

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

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

fromThunkable :: forall {n} {k} {adj :: n +-> k} (x :: DUPLOID adj) (y :: DUPLOID adj). (Adjunction adj, Ob x, Ob y) => (Pos x ~> Pos y) -> x ~> y Source Github #

fromLinear :: forall {k} {p} {adj :: k +-> p} (x :: DUPLOID adj) (y :: DUPLOID adj). (Adjunction adj, Ob x, Ob y) => (Neg x ~> Neg y) -> x ~> y Source Github #

type Dn (x :: DUPLOID adj1) = 'P (Pos x) :: DUPLOID adj Source Github #

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

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

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

type Up (x :: DUPLOID adj1) = 'N (Neg x) :: DUPLOID adj Source Github #

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

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

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

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