Safe Haskell	None
Language	GHC2024

Proarrow.Category.Monoidal.StarAutonomous

Description

Star-autonomous categories: symmetric closed categories with a dualizing functor Dual, where morphisms a ** b ~> Dual c correspond to a ~> Dual (b ** c) (linDist). This gives double-negation elimination (doubleNeg) and an internal hom ExpSA a b = Dual (a ** Dual b) Star-autonomous categories are the categorical semantics of multiplicative linear logic.

Synopsis

class (SymMonoidal k, Closed k, Ob (Unit :: k)) => StarAutonomous 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
- dualInv :: forall (a :: k) (b :: k). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> 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
- doubleNeg :: forall (a :: k). Ob a => Dual (Dual a) ~> a
- doubleNegInv :: forall (a :: k). Ob a => a ~> Dual (Dual a)
dualObj :: forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
doubleNegDefault :: forall {k} (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNegInvDefault :: forall {k} (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegIso :: forall {k} (a :: k) (a' :: k). (StarAutonomous k, Ob a, Ob a') => PIso a a' (Dual (Dual a)) (Dual (Dual a'))
linDistS :: forall {k} (a :: k) (b :: k) (c :: k). (StarAutonomous k, Ob c) => ('[a, b] ~> '[Dual c]) -> '[a] ~> '[Dual (b ** c)]
linDistInvS :: forall {k} (a :: k) (b :: k) (c :: k). (StarAutonomous k, Ob b, Ob c) => ('[a] ~> '[Dual (b ** c)]) -> '[a, b] ~> '[Dual c]
type ExpSA (a :: k) (b :: k) = Dual (a ** Dual b)
currySA :: forall {k} (a :: k) (b :: k) (c :: k). (StarAutonomous k, Ob a, Ob b) => ((a ** b) ~> c) -> a ~> ExpSA b c
applySA :: forall {k} (b :: k) (c :: k). (StarAutonomous k, Ob b, Ob c) => (ExpSA b c ** b) ~> c
expSA :: forall {k} (a :: k) (b :: k) (x :: k) (y :: k). StarAutonomous k => (b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
dualityUnitSA :: forall {k} (a :: k). (StarAutonomous k, Ob a) => (Unit :: k) ~> Dual (Dual a ** a)
dualityCounitSA :: forall {k} (a :: k). (StarAutonomous k, Ob a) => (Dual a ** a) ~> Dual (Unit :: k)
data family DualF (a :: k) :: k
type StarAutonomousStructures = '[Monoidal, SymMonoidal, Closed, StarAutonomous]

Documentation

class (SymMonoidal k, Closed k, Ob (Unit :: k)) => StarAutonomous k where Source Github #

A *-autonomous category: a symmetric monoidal closed category with a dualizing object, so that Dual is a contravariant involution and Hom(a ** b, Dual c) is symmetric in its three arguments.

Laws:

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

Stated as code by the Laws instance for StarAutonomousStructures, and checked by Proarrow.Testing.Laws.testStarAutonomous.

Minimal complete definition

withObDual, dual, dualInv, 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.

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

Inverse to dual on hom-sets: recovers the undualized arrow.

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.

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

Double-negation elimination. Defaults to doubleNegDefault; an instance whose double dual is the object itself can say so directly.

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

Double-negation introduction, inverse to doubleNeg. Defaults to doubleNegInvDefault.

Instances

Instances details

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

dualInv :: forall (a :: Nat) (b :: Nat). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> 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 #

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

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

StarAutonomous BOOL Source Github #

Instance details

Defined in Proarrow.Category.Monoidal.StarAutonomous

Associated Types

type Dual (a :: BOOL)
Instance details Defined in Proarrow.Category.Monoidal.StarAutonomous 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 #

dualInv :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> 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 #

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

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

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

dualInv :: forall (a :: FINREL) (b :: FINREL). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> 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 #

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

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

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

dualInv :: forall (a :: LINEAR) (b :: LINEAR). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> 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 #

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

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

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

dualInv :: forall (a :: DOT) (b :: DOT). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> 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 #

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

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

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

dualInv :: forall (a :: SVG) (b :: SVG). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> 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 #

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

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

StarAutonomous () Source Github #

Instance details

Defined in Proarrow.Category.Monoidal.StarAutonomous

Associated Types

type Dual '()
Instance details Defined in Proarrow.Category.Monoidal.StarAutonomous 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 #

dualInv :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> 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 #

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

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

(HasPushouts k, HasCoproducts k) => StarAutonomous (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 #

dualInv :: forall (a :: COSPAN k) (b :: COSPAN k). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> 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 #

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

doubleNegInv :: forall (a :: COSPAN k). Ob a => a ~> Dual (Dual a) 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 #

Num a => StarAutonomous (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 #

dualInv :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => (Dual a0 ~> Dual b) -> b ~> 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 #

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

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

(HasPullbacks k, HasProducts k) => StarAutonomous (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 #

dualInv :: forall (a :: SPAN k) (b :: SPAN k). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> 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 #

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

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

StarAutonomous (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 #

dualInv :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r)). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> 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 #

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

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

CommutativeMonoid m => StarAutonomous (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 #

dualInv :: forall (a :: MONOID m) (b :: MONOID m). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> 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 #

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

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

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

Instance details

Defined in Proarrow.Category.Monoidal.StarAutonomous

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 #

dualInv :: forall (a :: (j, k)) (b :: (j, k)). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> 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 #

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

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

Elems StarAutonomousStructures cs => StarAutonomous (FREE cs p) Source Github #

Instance details

Defined in Proarrow.Category.Monoidal.StarAutonomous

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 #

dualInv :: forall (a :: FREE cs p) (b :: FREE cs p). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> 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 #

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

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

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

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

doubleNeg from the rest of the structure: dualInv of doubleNegInv at the dual.

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

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

doubleNegIso :: forall {k} (a :: k) (a' :: k). (StarAutonomous k, Ob a, Ob a') => PIso a a' (Dual (Dual a)) (Dual (Dual a')) Source Github #

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

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

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

currySA :: forall {k} (a :: k) (b :: k) (c :: k). (StarAutonomous k, Ob a, Ob b) => ((a ** b) ~> c) -> a ~> ExpSA b c Source Github #

applySA :: forall {k} (b :: k) (c :: k). (StarAutonomous k, Ob b, Ob c) => (ExpSA b c ** b) ~> c Source Github #

expSA :: forall {k} (a :: k) (b :: k) (x :: k) (y :: k). StarAutonomous k => (b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y Source Github #

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

dualityCounitSA :: forall {k} (a :: k). (StarAutonomous 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 StarAutonomous cs) => IsFreeOb (DualF a :: FREE cs p) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.StarAutonomous 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.StarAutonomous type Lower (f :: k1 +-> k2) (DualF a :: FREE cs p) = Dual (Lower f a)

type StarAutonomousStructures = '[Monoidal, SymMonoidal, Closed, StarAutonomous] Source Github #

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