Safe Haskell	None
Language	GHC2024

Proarrow.Category.Monoidal.CompactClosed

Description

Compact closed categories: star-autonomous categories whose dual distributes over the tensor (distribDual, dualUnit), so that every object has a duality unit and counit (dualityUnit, dualityCounit) and every morphism x ** u ~> y ** u has a trace (traceCC).

Synopsis

class (StarAutonomous k, SymMonoidal k) => CompactClosed k where
- distribDual :: forall (a :: k) (b :: k). (Ob a, Ob b) => Dual (a ** b) ~> (Dual a ** Dual b)
- dualUnit :: Dual (Unit :: k) ~> (Unit :: k)
- dualityUnit :: forall (a :: k). Ob a => (Unit :: k) ~> (a ** Dual a)
- dualityCounit :: forall (a :: k). Ob a => (Dual a ** a) ~> (Unit :: k)
dualUnitInv :: CompactClosed k => (Unit :: k) ~> Dual (Unit :: k)
dualityUnitDefault :: forall {k} (a :: k). (CompactClosed k, Ob a) => (Unit :: k) ~> (a ** Dual a)
dualityUnitS :: forall {k} (a :: k). (CompactClosed k, Ob a) => ('[] :: [k]) ~> '[a, Dual a]
dualityCounitDefault :: forall {k} (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> (Unit :: k)
dualityCounitS :: forall {k} (a :: k). (CompactClosed k, Ob a) => '[Dual a, a] ~> ('[] :: [k])
combineDual :: forall {k} (a :: k) (b :: k). (CompactClosed k, Ob a, Ob b) => (Dual a ** Dual b) ~> Dual (a ** b)
combineDualS :: forall {k} (a :: k) (b :: k). (CompactClosed k, Ob a, Ob b) => '[Dual a, Dual b] ~> '[Dual (a ** b)]
dimension :: forall {k} (a :: k). (CompactClosed k, Ob a) => (Unit :: k) ~> (Unit :: k)
traceCCS :: forall {k} (u :: k) (x :: k) (y :: k). (CompactClosed k, Ob x, Ob y, Ob u) => ('[x, u] ~> '[y, u]) -> '[x] ~> '[y]
traceCC :: forall {k} (u :: k) (x :: k) (y :: k). (CompactClosed k, Ob x, Ob y, Ob u) => ((x ** u) ~> (y ** u)) -> x ~> y
coactCC :: forall {m} {k} (t :: (m, k) +-> k) (u :: m) (x :: k) (y :: k). (CompactClosed m, MonoidalAction t, Ob x, Ob y, Ob u) => (Act t u x ~> Act t u y) -> x ~> y
type CompactClosedStructures = '[Monoidal, SymMonoidal, Closed, StarAutonomous, CompactClosed]

Documentation

class (StarAutonomous k, SymMonoidal k) => CompactClosed k where Source Github #

Methods

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

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

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

The unit of the duality between a and its dual. dualityUnitDefault gives it from the *-autonomous structure; an instance with cups of its own can use them. (There is no default method: a occurs only under type families, so GHC could not instantiate one.)

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

The counit of the duality between a and its dual; see dualityCounitDefault.

Instances

Instances details

CompactClosed Nat Source Github #
Instance details Defined in Proarrow.Category.Instance.ZX Methods distribDual :: forall (a :: Nat) (b :: Nat). (Ob a, Ob b) => Dual (a b) ~> (Dual a Dual b) Source Github # dualUnit :: Dual (Unit :: Nat) ~> (Unit :: Nat) Source Github # dualityUnit :: forall (a :: Nat). Ob a => (Unit :: Nat) ~> (a Dual a) Source Github # dualityCounit :: forall (a :: Nat). Ob a => (Dual a a) ~> (Unit :: Nat) Source Github #
CompactClosed FINREL Source Github #
Instance details Defined in Proarrow.Category.Instance.FinRel Methods distribDual :: forall (a :: FINREL) (b :: FINREL). (Ob a, Ob b) => Dual (a b) ~> (Dual a Dual b) Source Github # dualUnit :: Dual (Unit :: FINREL) ~> (Unit :: FINREL) Source Github # dualityUnit :: forall (a :: FINREL). Ob a => (Unit :: FINREL) ~> (a Dual a) Source Github # dualityCounit :: forall (a :: FINREL). Ob a => (Dual a a) ~> (Unit :: FINREL) Source Github #
CompactClosed DOT Source Github #
Instance details Defined in Proarrow.Tools.Diagrams.Dot Methods distribDual :: forall (a :: DOT) (b :: DOT). (Ob a, Ob b) => Dual (a b) ~> (Dual a Dual b) Source Github # dualUnit :: Dual (Unit :: DOT) ~> (Unit :: DOT) Source Github # dualityUnit :: forall (a :: DOT). Ob a => (Unit :: DOT) ~> (a Dual a) Source Github # dualityCounit :: forall (a :: DOT). Ob a => (Dual a a) ~> (Unit :: DOT) Source Github #
CompactClosed SVG Source Github #
Instance details Defined in Proarrow.Tools.Diagrams.Svg Methods distribDual :: forall (a :: SVG) (b :: SVG). (Ob a, Ob b) => Dual (a b) ~> (Dual a Dual b) Source Github # dualUnit :: Dual (Unit :: SVG) ~> (Unit :: SVG) Source Github # dualityUnit :: forall (a :: SVG). Ob a => (Unit :: SVG) ~> (a Dual a) Source Github # dualityCounit :: forall (a :: SVG). Ob a => (Dual a a) ~> (Unit :: SVG) Source Github #
CompactClosed () Source Github #
Instance details Defined in Proarrow.Category.Monoidal.CompactClosed Methods distribDual :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => Dual (a b) ~> (Dual a Dual b) Source Github # dualUnit :: Dual (Unit :: ()) ~> (Unit :: ()) Source Github # dualityUnit :: forall (a :: ()). Ob a => (Unit :: ()) ~> (a Dual a) Source Github # dualityCounit :: forall (a :: ()). Ob a => (Dual a a) ~> (Unit :: ()) Source Github #
(HasPushouts k, HasCoproducts k) => CompactClosed (COSPAN k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Cospan Methods distribDual :: forall (a :: COSPAN k) (b :: COSPAN k). (Ob a, Ob b) => Dual (a b) ~> (Dual a Dual b) Source Github # dualUnit :: Dual (Unit :: COSPAN k) ~> (Unit :: COSPAN k) Source Github # dualityUnit :: forall (a :: COSPAN k). Ob a => (Unit :: COSPAN k) ~> (a Dual a) Source Github # dualityCounit :: forall (a :: COSPAN k). Ob a => (Dual a a) ~> (Unit :: COSPAN k) 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 #
Num a => CompactClosed (MatK a) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods distribDual :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => Dual (a0 b) ~> (Dual a0 Dual b) Source Github # dualUnit :: Dual (Unit :: MatK a) ~> (Unit :: MatK a) Source Github # dualityUnit :: forall (a0 :: MatK a). Ob a0 => (Unit :: MatK a) ~> (a0 Dual a0) Source Github # dualityCounit :: forall (a0 :: MatK a). Ob a0 => (Dual a0 a0) ~> (Unit :: MatK a) Source Github #
(HasPullbacks k, HasProducts k) => CompactClosed (SPAN k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Span Methods distribDual :: forall (a :: SPAN k) (b :: SPAN k). (Ob a, Ob b) => Dual (a b) ~> (Dual a Dual b) Source Github # dualUnit :: Dual (Unit :: SPAN k) ~> (Unit :: SPAN k) Source Github # dualityUnit :: forall (a :: SPAN k). Ob a => (Unit :: SPAN k) ~> (a Dual a) Source Github # dualityCounit :: forall (a :: SPAN k). Ob a => (Dual a a) ~> (Unit :: SPAN k) Source Github #
CommutativeMonoid m => CompactClosed (MONOID m) Source Github #
Instance details Defined in Proarrow.Category.Instance.Monoid Methods distribDual :: forall (a :: MONOID m) (b :: MONOID m). (Ob a, Ob b) => Dual (a b) ~> (Dual a Dual b) Source Github # dualUnit :: Dual (Unit :: MONOID m) ~> (Unit :: MONOID m) Source Github # dualityUnit :: forall (a :: MONOID m). Ob a => (Unit :: MONOID m) ~> (a Dual a) Source Github # dualityCounit :: forall (a :: MONOID m). Ob a => (Dual a a) ~> (Unit :: MONOID m) Source Github #
(CompactClosed j, CompactClosed k) => CompactClosed (j, k) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.CompactClosed Methods distribDual :: forall (a :: (j, k)) (b :: (j, k)). (Ob a, Ob b) => Dual (a b) ~> (Dual a Dual b) Source Github # dualUnit :: Dual (Unit :: (j, k)) ~> (Unit :: (j, k)) Source Github # dualityUnit :: forall (a :: (j, k)). Ob a => (Unit :: (j, k)) ~> (a Dual a) Source Github # dualityCounit :: forall (a :: (j, k)). Ob a => (Dual a a) ~> (Unit :: (j, k)) Source Github #
Elems CompactClosedStructures cs => CompactClosed (FREE cs p) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.CompactClosed Methods distribDual :: forall (a :: FREE cs p) (b :: FREE cs p). (Ob a, Ob b) => Dual (a b) ~> (Dual a Dual b) Source Github # dualUnit :: Dual (Unit :: FREE cs p) ~> (Unit :: FREE cs p) Source Github # dualityUnit :: forall (a :: FREE cs p). Ob a => (Unit :: FREE cs p) ~> (a Dual a) Source Github # dualityCounit :: forall (a :: FREE cs p). Ob a => (Dual a a) ~> (Unit :: FREE cs p) Source Github #

dualUnitInv :: CompactClosed k => (Unit :: k) ~> Dual (Unit :: k) Source Github #

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

dualityUnit from the *-autonomous structure.

dualityUnitS :: forall {k} (a :: k). (CompactClosed k, Ob a) => ('[] :: [k]) ~> '[a, Dual a] Source Github #

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

dualityCounit from the *-autonomous structure.

dualityCounitS :: forall {k} (a :: k). (CompactClosed k, Ob a) => '[Dual a, a] ~> ('[] :: [k]) Source Github #

combineDual :: forall {k} (a :: k) (b :: k). (CompactClosed k, Ob a, Ob b) => (Dual a ** Dual b) ~> Dual (a ** b) Source Github #

combineDualS :: forall {k} (a :: k) (b :: k). (CompactClosed k, Ob a, Ob b) => '[Dual a, Dual b] ~> '[Dual (a ** b)] Source Github #

dimension :: forall {k} (a :: k). (CompactClosed k, Ob a) => (Unit :: k) ~> (Unit :: k) Source Github #

The dimension of a: the trace of its identity, as a scalar.

traceCCS :: forall {k} (u :: k) (x :: k) (y :: k). (CompactClosed k, Ob x, Ob y, Ob u) => ('[x, u] ~> '[y, u]) -> '[x] ~> '[y] Source Github #

traceCC :: forall {k} (u :: k) (x :: k) (y :: k). (CompactClosed k, Ob x, Ob y, Ob u) => ((x ** u) ~> (y ** u)) -> x ~> y Source Github #

coactCC :: forall {m} {k} (t :: (m, k) +-> k) (u :: m) (x :: k) (y :: k). (CompactClosed m, MonoidalAction t, Ob x, Ob y, Ob u) => (Act t u x ~> Act t u y) -> x ~> y Source Github #

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

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