Safe Haskell	None
Language	GHC2024

Proarrow.Category.Monoidal.Coclosed

Description

Coclosed monoidal categories, dual to Proarrow.Category.Monoidal.Closed: Coclosed provides the coexponential a <~~ b, left adjoint to tensoring, with coeval and its universal property coevalUniv; CoCCC is the cocartesian coclosed case.

Synopsis

class Monoidal k => Coclosed k where
- type (a :: k) <~~ (b :: k) :: k
- withObCoExp :: forall (a :: k) (b :: k) r. (Ob a, Ob b) => (Ob (a <~~ b) => r) -> r
- coeval :: forall (a :: k) (b :: k). (Ob a, Ob b) => a ~> ((a <~~ b) ** b)
- coevalUniv :: forall (b :: k) (c :: k) (a :: k). (Ob b, Ob c) => (a ~> (c ** b)) -> (a <~~ b) ~> c
class (Cocartesian k, Coclosed k) => CoCCC k

Documentation

class Monoidal k => Coclosed k where Source Github #

A coclosed monoidal category, dual to Closed: the coexponential a <~~ b is left adjoint to tensoring with b, so coevalUniv witnesses Hom(a <~~ b, c) ≅ Hom(a, c ** b) with coeval as the unit.

Laws:

coevalUniv is a bijection, inverted by \g -> (g ** id) . coeval: (coevalUniv f ** id) . coeval = f and coevalUniv ((g ** id) . coeval) = g
and natural in all three variables, dually to curry.

Unlike those of Closed, these laws have no check in Proarrow.Testing.Laws.

Associated Types

type (a :: k) <~~ (b :: k) :: k Source Github #

The coexponential object.

Methods

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

Recovers Ob (a <~~ b) from the objecthood of the ends.

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

Co-evaluation: the unit of the adjunction.

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

Transposes an arrow into a tensor into one out of a coexponential.

Instances

Instances details

Coclosed () Source Github #

Instance details

Defined in Proarrow.Category.Monoidal.Coclosed

Associated Types

type (a :: ()) <~~ (b :: ())
Instance details Defined in Proarrow.Category.Monoidal.Coclosed type (a :: ()) <~~ (b :: ()) = '()

Methods

withObCoExp :: forall (a :: ()) (b :: ()) r. (Ob a, Ob b) => (Ob (a <~~ b) => r) -> r Source Github #

coeval :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => a ~> ((a <~~ b) ** b) Source Github #

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

Coclosed (Type -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Nat

Associated Types

type (f :: Type -> Type) <~~ (j :: Type -> Type)
Instance details Defined in Proarrow.Category.Instance.Nat type (f :: Type -> Type) <~~ (j :: Type -> Type) = Lan j f

Methods

withObCoExp :: forall (a :: Type -> Type) (b :: Type -> Type) r. (Ob a, Ob b) => (Ob (a <~~ b) => r) -> r Source Github #

coeval :: forall (a :: Type -> Type) (b :: Type -> Type). (Ob a, Ob b) => a ~> ((a <~~ b) ** b) Source Github #

coevalUniv :: forall (b :: Type -> Type) (c :: Type -> Type) (a :: Type -> Type). (Ob b, Ob c) => (a ~> (c ** b)) -> (a <~~ b) ~> c Source Github #

class (Cocartesian k, Coclosed k) => CoCCC k Source Github #

Instances

Instances details

(Cocartesian k, Coclosed k) => CoCCC k Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Coclosed