Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.IntConstruction

Description

The Int construction (Joyal-Street-Verity) on a traced monoidal category k: objects are formal differences I plus minus of k-objects, and morphisms are k-morphisms between the appropriately tensored halves, composed by tracing out the middle. The result is compact closed (the free such over k) with duals given by swapping the two halves.

Documentation

data INT k Source Github #

Constructors

I k k

Instances

Instances details

TracedMonoidal k => Monoidal (INT k) Source Github #

The monoidal tensor is pointwise, tensoring of the plus and minus parts.

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.IntConstruction type Unit = 'I (Unit :: k) (Unit :: k)

Methods

withOb2 :: forall (a :: INT k) (b :: INT k) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Github #

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

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

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

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

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

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

TracedMonoidal k => SymMonoidal (INT k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

swap :: forall (a :: INT k) (b :: INT k). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Github #

TracedMonoidal k => Closed (INT k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

withObExp :: forall (a :: INT k) (b :: INT k) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r Source Github #

curry :: forall (a :: INT k) (b :: INT k) (c :: INT k). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) Source Github #

apply :: forall (a :: INT k) (b :: INT k). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b Source Github #

(^^^) :: forall (a :: INT k) (b :: INT k) (x :: INT k) (y :: INT k). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Github #

TracedMonoidal k => CompactClosed (INT k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

distribDual :: forall (a :: INT k) (b :: INT k). (Ob a, Ob b) => Dual (a ** b) ~> (Dual a ** Dual b) Source Github #

dualUnit :: Dual (Unit :: INT k) ~> (Unit :: INT k) Source Github #

dualityUnit :: forall (a :: INT k). Ob a => (Unit :: INT k) ~> (a ** Dual a) Source Github #

dualityCounit :: forall (a :: INT k). Ob a => (Dual a ** a) ~> (Unit :: INT k) Source Github #

TracedMonoidal k => StarAutonomous (INT k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

withObDual :: forall (a :: INT k) r. Ob a => (Ob (Dual a) => r) -> r Source Github #

dual :: forall (a :: INT k) (b :: INT k). (a ~> b) -> Dual b ~> Dual a Source Github #

dualInv :: forall (a :: INT k) (b :: INT k). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> a Source Github #

linDist :: forall (a :: INT k) (b :: INT k) (c :: INT k). (Ob a, Ob b, Ob c) => ((a ** b) ~> Dual c) -> a ~> Dual (b ** c) Source Github #

linDistInv :: forall (a :: INT k) (b :: INT k) (c :: INT k). (Ob a, Ob b, Ob c) => (a ~> Dual (b ** c)) -> (a ** b) ~> Dual c Source Github #

doubleNeg :: forall (a :: INT k). Ob a => Dual (Dual a) ~> a Source Github #

doubleNegInv :: forall (a :: INT k). Ob a => a ~> Dual (Dual a) Source Github #

TracedMonoidal k => CategoryOf (INT k) Source Github #

The Int construction, a.k.a. the geometry of interaction, the free compact closed category on a traced monoidal category.

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.IntConstruction type (~>) = IntConstruction :: INT k -> INT k -> Type

TracedMonoidal k => Promonad (IntConstruction :: INT k -> INT k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

id :: forall (a :: INT k). Ob a => IntConstruction a a Source Github #

(.) :: forall (b :: INT k) (c :: INT k) (a :: INT k). IntConstruction b c -> IntConstruction a b -> IntConstruction a c Source Github #

TracedMonoidal k => MonoidalProfunctor (IntConstruction :: INT k -> INT k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

one :: IntConstruction (Unit :: INT k) (Unit :: INT k) Source Github #

(**) :: forall (x1 :: INT k) (x2 :: INT k) (y1 :: INT k) (y2 :: INT k). IntConstruction x1 x2 -> IntConstruction y1 y2 -> IntConstruction (x1 ** y1) (x2 ** y2) Source Github #

TracedMonoidal k => Profunctor (IntConstruction :: INT k -> INT k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

dimap :: forall (c :: INT k) (a :: INT k) (b :: INT k) (d :: INT k). (c ~> a) -> (b ~> d) -> IntConstruction a b -> IntConstruction c d Source Github #

lmap :: forall (c :: INT k) (a :: INT k) (b :: INT k). (c ~> a) -> IntConstruction a b -> IntConstruction c b Source Github #

rmap :: forall (b :: INT k) (d :: INT k) (a :: INT k). (b ~> d) -> IntConstruction a b -> IntConstruction a d Source Github #

(\\) :: forall (a :: INT k) (b :: INT k) r. ((Ob a, Ob b) => r) -> IntConstruction a b -> r Source Github #

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

type Unit = 'I (Unit :: k) (Unit :: k)

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

type (~>) = IntConstruction :: INT k -> INT k -> Type

type Ob (a :: INT k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

type Ob (a :: INT k) = (a ~ 'I (IntPlus a) (IntMinus a), Ob (IntPlus a), Ob (IntMinus a))

type (a :: INT k) ** (b :: INT k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

type (a :: INT k) ** (b :: INT k) = 'I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)

type (a :: INT k) ~~> (b :: INT k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

type (a :: INT k) ~~> (b :: INT k) = ExpSA a b

type Dual ('I p n :: INT k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

type Dual ('I p n :: INT k) = 'I n p

type family IntPlus (i :: INT k) :: k where ... Source Github #

Equations

IntPlus ('I a b :: INT k) = a

type family IntMinus (i :: INT k) :: k where ... Source Github #

Equations

IntMinus ('I a b :: INT k) = b

data IntConstruction (a :: INT k) (b :: INT k) where Source Github #

Constructors

Int :: forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k). (Ob ap, Ob am, Ob bp, Ob bm) => ((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)

Instances

Instances details

TracedMonoidal k => Promonad (IntConstruction :: INT k -> INT k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.IntConstruction Methods id :: forall (a :: INT k). Ob a => IntConstruction a a Source Github # (.) :: forall (b :: INT k) (c :: INT k) (a :: INT k). IntConstruction b c -> IntConstruction a b -> IntConstruction a c Source Github #
TracedMonoidal k => MonoidalProfunctor (IntConstruction :: INT k -> INT k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.IntConstruction Methods one :: IntConstruction (Unit :: INT k) (Unit :: INT k) Source Github # () :: forall (x1 :: INT k) (x2 :: INT k) (y1 :: INT k) (y2 :: INT k). IntConstruction x1 x2 -> IntConstruction y1 y2 -> IntConstruction (x1 y1) (x2 ** y2) Source Github #
TracedMonoidal k => Profunctor (IntConstruction :: INT k -> INT k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.IntConstruction Methods dimap :: forall (c :: INT k) (a :: INT k) (b :: INT k) (d :: INT k). (c ~> a) -> (b ~> d) -> IntConstruction a b -> IntConstruction c d Source Github # lmap :: forall (c :: INT k) (a :: INT k) (b :: INT k). (c ~> a) -> IntConstruction a b -> IntConstruction c b Source Github # rmap :: forall (b :: INT k) (d :: INT k) (a :: INT k). (b ~> d) -> IntConstruction a b -> IntConstruction a d Source Github # (\\) :: forall (a :: INT k) (b :: INT k) r. ((Ob a, Ob b) => r) -> IntConstruction a b -> r Source Github #

toInt :: forall {k} (a :: k) (b :: k) (m :: k). (TracedMonoidal k, Ob m) => (a ~> b) -> 'I a m ~> 'I b m Source Github #

isoToInt :: forall {k} (a :: k) (b :: k). TracedMonoidal k => (a ~> b) -> (b ~> a) -> 'I a a ~> 'I b b Source Github #

fromInt :: forall {k} (a :: k) (b :: k) (m :: k). TracedMonoidal k => ('I a m ~> 'I b m) -> a ~> b Source Github #