Safe Haskell	None
Language	GHC2024

Proarrow.Category.Monoidal.Dialogue

Description

Dialogue categories (Melliès): symmetric monoidal categories with a tensorial negation Dual, where morphisms a ** b ~> Dual c correspond to a ~> Dual (b ** c) (linDist). Unlike in a *-autonomous category, double negation Dual (Dual a) ~> a need not exist: only its inverse doubleNegInv does, which tripleNeg undoes on a dual. Any closed category with a chosen answer object is one, with Dual a = a ~~> r, which is why the continuation passing reading of System L in Proarrow.Tools.SMC needs no more than this.

The *-autonomous categories of Proarrow.Category.Monoidal.StarAutonomous are the dialogue categories whose double negation is an isomorphism.

Synopsis

class SymMonoidal k => Dialogue k where
- type Dual (a :: k) :: k
- withObDual :: forall (a :: k) r. Ob a => (Ob (Dual a) => r) -> r
- dual :: forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
- linDist :: forall (a :: k) (b :: k) (c :: k). (Ob a, Ob b, Ob c) => ((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
- linDistInv :: forall (a :: k) (b :: k) (c :: k). (Ob a, Ob b, Ob c) => (a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
- doubleNegInv :: forall (a :: k). Ob a => a ~> Dual (Dual a)
dualObj :: forall {k} (a :: k). (Dialogue k, Ob a) => Obj (Dual a)
doubleNegInvDefault :: forall {k} (a :: k). (Dialogue k, Ob a) => a ~> Dual (Dual a)
tripleNeg :: forall {k} (a :: k). (Dialogue k, Ob a) => Dual (Dual (Dual a)) ~> Dual a
bindDual :: forall {k} (g :: k) (a :: k) (y :: k). (Dialogue k, Ob g, Ob a, Ob y) => ((g ** a) ~> Dual y) -> (Dual (Dual a) ** g) ~> Dual y
linDistS :: forall {k} (a :: k) (b :: k) (c :: k). (Dialogue k, Ob c) => ('[a, b] ~> '[Dual c]) -> '[a] ~> '[Dual (b ** c)]
linDistInvS :: forall {k} (a :: k) (b :: k) (c :: k). (Dialogue k, Ob b, Ob c) => ('[a] ~> '[Dual (b ** c)]) -> '[a, b] ~> '[Dual c]
type Par (a :: k) (b :: k) = Dual (Dual a ** Dual b)
withObPar :: forall {k} (a :: k) (b :: k) r. (Dialogue k, Ob a, Ob b) => ((Ob (Dual a), Ob (Dual b), Ob (Par a b)) => r) -> r
par :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Dialogue k => (a ~> c) -> (b ~> d) -> Par a b ~> Par c d
parSwap :: forall {k} (a :: k) (b :: k). (Dialogue k, Ob a, Ob b) => Par a b ~> Par b a
weakDistL :: forall {k} (a :: k) (b :: k) (c :: k). (Dialogue k, Ob a, Ob b, Ob c) => (a ** Par b c) ~> Par (a ** b) c
weakDistR :: forall {k} (a :: k) (b :: k) (c :: k). (Dialogue k, Ob a, Ob b, Ob c) => (Par a b ** c) ~> Par a (b ** c)
dualityUnitSA :: forall {k} (a :: k). (Dialogue k, Ob a) => (Unit :: k) ~> Dual (Dual a ** a)
dualityCounitSA :: forall {k} (a :: k). (Dialogue k, Ob a) => (Dual a ** a) ~> Dual (Unit :: k)
data family DualF (a :: k) :: k
type DialogueStructures = '[Monoidal, SymMonoidal, Dialogue]

Documentation

class SymMonoidal k => Dialogue k where Source Github #

A dialogue category: a symmetric monoidal category with a tensorial negation, so that Dual is a contravariant functor and Hom(a ** b, Dual c) ≅ Hom(a, Dual (b ** c)).

Laws:

dual is a contravariant functor: dual id = id and dual (f . g) = dual g . dual f
linDist and linDistInv are mutually inverse, giving Hom(a ** b, Dual c) ≅ Hom(a, Dual (b ** c)), natural in all three variables
doubleNegInv is doubleNegInvDefault, the one the rest of the structure gives

Stated as code by the Laws instance for DialogueStructures, and checked by Proarrow.Testing.Laws.testDialogue.

Minimal complete definition

withObDual, dual, linDist, linDistInv

Associated Types

type Dual (a :: k) :: k Source Github #

The dual of an object.

Methods

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

Recovers Ob (Dual a) from the objecthood of a.

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

Dual's contravariant action on arrows.

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

Linear distribution: transposes a tensor factor across the dual.

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

Inverse to linDist.

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

Double-negation introduction. Defaults to doubleNegInvDefault.

Instances

Instances details

Dialogue Nat Source Github #

Instance details

Defined in Proarrow.Category.Instance.ZX

Associated Types

type Dual (x :: Nat)
Instance details Defined in Proarrow.Category.Instance.ZX type Dual (x :: Nat) = x

Methods

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

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

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

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

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

Dialogue BOOL Source Github #

Instance details

Defined in Proarrow.Category.Monoidal.Dialogue

Associated Types

type Dual (a :: BOOL)
Instance details Defined in Proarrow.Category.Monoidal.Dialogue type Dual (a :: BOOL) = Not a

Methods

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

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

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

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

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

Dialogue FINREL Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinRel

Associated Types

type Dual (n :: FINREL)
Instance details Defined in Proarrow.Category.Instance.FinRel type Dual (n :: FINREL) = n

Methods

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

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

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

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

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

Dialogue LINEAR Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type Dual ('L a :: LINEAR)
Instance details Defined in Proarrow.Category.Instance.Linear type Dual ('L a :: LINEAR) = 'L (Not a)

Methods

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

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

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

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

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

Dialogue DOT Source Github #

Instance details

Defined in Proarrow.Tools.Diagrams.Dot

Associated Types

type Dual (a :: DOT)
Instance details Defined in Proarrow.Tools.Diagrams.Dot type Dual (a :: DOT) = a

Methods

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

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

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

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

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

Dialogue SVG Source Github #

The dual of a wire is its Co wire. Duals come from dualCup and dualCap, which mean a cup or cap and are drawn as a bend, so a dual wire is drawn hollow wherever it runs.

Instance details

Defined in Proarrow.Tools.Diagrams.Svg

Associated Types

type Dual (a :: SVG)
Instance details Defined in Proarrow.Tools.Diagrams.Svg type Dual (a :: SVG) = 'S (DualList (UN 'S a))

Methods

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

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

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

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

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

Dialogue () Source Github #

Instance details

Defined in Proarrow.Category.Monoidal.Dialogue

Associated Types

type Dual '()
Instance details Defined in Proarrow.Category.Monoidal.Dialogue type Dual '() = '()

Methods

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

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

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

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

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

(HasPushouts k, HasCoproducts k) => Dialogue (COSPAN k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cospan

Methods

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

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

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

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

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

TracedMonoidal k => Dialogue (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 #

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 #

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

Num a => Dialogue (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

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

dual :: forall (a0 :: MatK a) (b :: MatK a). (a0 ~> b) -> Dual b ~> Dual a0 Source Github #

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

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

doubleNegInv :: forall (a0 :: MatK a). Ob a0 => a0 ~> Dual (Dual a0) Source Github #

(HasPullbacks k, HasProducts k) => Dialogue (SPAN k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Span

Methods

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

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

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

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

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

(Closed k, SymMonoidal k, Ob r) => Dialogue (CPS r) Source Github #

The dual of a is a ~~> r, the functor Not r on objects: linear distribution is uncurrying, reassociating and currying.

Instance details

Defined in Proarrow.Category.Instance.Cps

Methods

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

dual :: forall (a :: CPS r) (b :: CPS r). (a ~> b) -> Dual b ~> Dual a Source Github #

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

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

doubleNegInv :: forall (a :: CPS r). Ob a => a ~> Dual (Dual a) Source Github #

Dialogue (KLEISLI (Cont r)) Source Github #

Instance details

Defined in Proarrow.Promonad.Cont

Methods

withObDual :: forall (a :: KLEISLI (Cont r)) r0. Ob a => (Ob (Dual a) => r0) -> r0 Source Github #

dual :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r)). (a ~> b) -> Dual b ~> Dual a Source Github #

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

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

doubleNegInv :: forall (a :: KLEISLI (Cont r)). Ob a => a ~> Dual (Dual a) Source Github #

CommutativeMonoid m => Dialogue (MONOID m) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Monoid

Methods

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

dual :: forall (a :: MONOID m) (b :: MONOID m). (a ~> b) -> Dual b ~> Dual a Source Github #

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

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

doubleNegInv :: forall (a :: MONOID m). Ob a => a ~> Dual (Dual a) Source Github #

(Dialogue j, Dialogue k) => Dialogue (j, k) Source Github #

Instance details

Defined in Proarrow.Category.Monoidal.Dialogue

Methods

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

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

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

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

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

Elems DialogueStructures cs => Dialogue (FREE cs p) Source Github #

Instance details

Defined in Proarrow.Category.Monoidal.Dialogue

Methods

withObDual :: forall (a :: FREE cs p) r. Ob a => (Ob (Dual a) => r) -> r Source Github #

dual :: forall (a :: FREE cs p) (b :: FREE cs p). (a ~> b) -> Dual b ~> Dual a Source Github #

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

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

doubleNegInv :: forall (a :: FREE cs p). Ob a => a ~> Dual (Dual a) Source Github #

dualObj :: forall {k} (a :: k). (Dialogue k, Ob a) => Obj (Dual a) Source Github #

doubleNegInvDefault :: forall {k} (a :: k). (Dialogue k, Ob a) => a ~> Dual (Dual a) Source Github #

doubleNegInv from the rest of the structure, through linDistInv and the duality unit.

tripleNeg :: forall {k} (a :: k). (Dialogue k, Ob a) => Dual (Dual (Dual a)) ~> Dual a Source Github #

Triple negation elimination: a dual is a retract of its double negation, with doubleNegInv as the section, tripleNeg . doubleNegInv = id. For the computations of Proarrow.Tools.SMC it runs a computation of a computation into one, like join. It is an isomorphism only in a *-autonomous category: in Type with answer object Bool, Dual () has two elements and Dual (Dual (Dual ())) sixteen.

bindDual :: forall {k} (g :: k) (a :: k) (y :: k). (Dialogue k, Ob g, Ob a, Ob y) => ((g ** a) ~> Dual y) -> (Dual (Dual a) ** g) ~> Dual y Source Github #

The Kleisli extension of the double negation monad at a dual: a morphism out of a into a dual, extended to double negations of a. This is the bind of the continuation reading of System L in Proarrow.Tools.SMC. It moves a to the other side of the hom, g ** y ~> Dual a, and dualizes.

linDistS :: forall {k} (a :: k) (b :: k) (c :: k). (Dialogue k, Ob c) => ('[a, b] ~> '[Dual c]) -> '[a] ~> '[Dual (b ** c)] Source Github #

linDistInvS :: forall {k} (a :: k) (b :: k) (c :: k). (Dialogue k, Ob b, Ob c) => ('[a] ~> '[Dual (b ** c)]) -> '[a, b] ~> '[Dual c] Source Github #

type Par (a :: k) (b :: k) = Dual (Dual a ** Dual b) Source Github #

Par, the dual of the tensor of the duals.

withObPar :: forall {k} (a :: k) (b :: k) r. (Dialogue k, Ob a, Ob b) => ((Ob (Dual a), Ob (Dual b), Ob (Par a b)) => r) -> r Source Github #

Recovers Ob (Par a b), and the objecthood of the duals it is made of, from the objecthood of a and b.

par :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Dialogue k => (a ~> c) -> (b ~> d) -> Par a b ~> Par c d Source Github #

Par's action on arrows.

parSwap :: forall {k} (a :: k) (b :: k). (Dialogue k, Ob a, Ob b) => Par a b ~> Par b a Source Github #

The symmetry of Par.

weakDistL :: forall {k} (a :: k) (b :: k) (c :: k). (Dialogue k, Ob a, Ob b, Ob c) => (a ** Par b c) ~> Par (a ** b) c Source Github #

Linear distributivity: the tensor distributes into the left of a Par. Given the dual of a ** b, the a turns it into the dual of b, which the Par answers with c.

weakDistR :: forall {k} (a :: k) (b :: k) (c :: k). (Dialogue k, Ob a, Ob b, Ob c) => (Par a b ** c) ~> Par a (b ** c) Source Github #

Linear distributivity on the other side, from weakDistL by symmetry.

dualityUnitSA :: forall {k} (a :: k). (Dialogue k, Ob a) => (Unit :: k) ~> Dual (Dual a ** a) Source Github #

dualityCounitSA :: forall {k} (a :: k). (Dialogue k, Ob a) => (Dual a ** a) ~> Dual (Unit :: k) Source Github #

data family DualF (a :: k) :: k Source Github #

Instances

Instances details

(IsFreeOb a, Elem Dialogue cs) => IsFreeOb (DualF a :: FREE cs p) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Dialogue Methods lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (DualF a)) => r) -> r Source Github #
type Lower (f :: k1 +-> k2) (DualF a :: FREE cs p) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Dialogue type Lower (f :: k1 +-> k2) (DualF a :: FREE cs p) = Dual (Lower f a)

type DialogueStructures = '[Monoidal, SymMonoidal, Dialogue] Source Github #

The structures the free category needs for Dialogue, and those its laws are stated for.