Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Instance.Lifted

Synopsis

newtype LIFTED (p :: j +-> k) (q :: k +-> j) = LIFT j
data Lift (a :: LIFTED p q) (b :: LIFTED p1 q1) where
- Lift :: forall {j} {i} {k} {p1 :: i +-> k} {q1 :: k +-> i} (q :: j +-> i) (p :: i +-> j) (a1 :: i) (b1 :: i). (q :.: p) a1 b1 -> Lift ('LIFT a1 :: LIFTED p q) ('LIFT b1 :: LIFTED p1 q1)
type LIFTEDF (f :: j -> k) = LIFTED (Star f) (Costar f)
pattern LiftF :: forall {j1} {j2} {k} {p} {q} (f :: j1 -> j2) (a :: j1) (b :: j1). Functor f => (Ob a, Ob b) => (f a ~> f b) -> Lift ('LIFT a :: LIFTED (Star f) (Costar f)) ('LIFT b :: LIFTED p q)

Documentation

newtype LIFTED (p :: j +-> k) (q :: k +-> j) Source Comments #

Constructors

LIFT j

Instances

Instances details

Adjunction p q => CategoryOf (LIFTED p q) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Lifted

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Lifted type (~>) = Lift :: LIFTED p q -> LIFTED p q -> Type

(Adjunction p q, MonoidalProfunctor (Coprod p), MonoidalProfunctor (Coprod q), HasBinaryCoproducts j) => HasBinaryCoproducts (LIFTED p q) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Lifted

Methods

withObCoprod :: forall (a :: LIFTED p q) (b :: LIFTED p q) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Comments #

lft :: forall (a :: LIFTED p q) (b :: LIFTED p q). (Ob a, Ob b) => a ~> (a || b) Source Comments #

rgt :: forall (a :: LIFTED p q) (b :: LIFTED p q). (Ob a, Ob b) => b ~> (a || b) Source Comments #

(|||) :: forall (x :: LIFTED p q) (a :: LIFTED p q) (y :: LIFTED p q). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Comments #

(+++) :: forall (a :: LIFTED p q) (b :: LIFTED p q) (x :: LIFTED p q) (y :: LIFTED p q). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Comments #

(Adjunction p q, MonoidalProfunctor p, MonoidalProfunctor q, Cartesian j) => HasBinaryProducts (LIFTED p q) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Lifted

Methods

withObProd :: forall (a :: LIFTED p q) (b :: LIFTED p q) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Comments #

fst :: forall (a :: LIFTED p q) (b :: LIFTED p q). (Ob a, Ob b) => (a && b) ~> a Source Comments #

snd :: forall (a :: LIFTED p q) (b :: LIFTED p q). (Ob a, Ob b) => (a && b) ~> b Source Comments #

(&&&) :: forall (a :: LIFTED p q) (x :: LIFTED p q) (y :: LIFTED p q). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments #

(***) :: forall (a :: LIFTED p q) (b :: LIFTED p q) (x :: LIFTED p q) (y :: LIFTED p q). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments #

(Adjunction p q, HasInitialObject j) => HasInitialObject (LIFTED p q) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Lifted

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Lifted type InitialObject = 'LIFT (InitialObject :: j) :: LIFTED p q

Methods

initiate :: forall (a :: LIFTED p q). Ob a => (InitialObject :: LIFTED p q) ~> a Source Comments #

initiate' :: forall (a' :: LIFTED p q) (a :: LIFTED p q). (a' ~> a) -> (InitialObject :: LIFTED p q) ~> a Source Comments #

(Adjunction p q, HasTerminalObject j) => HasTerminalObject (LIFTED p q) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Lifted

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Lifted type TerminalObject = 'LIFT (TerminalObject :: j) :: LIFTED p q

Methods

terminate :: forall (a :: LIFTED p q). Ob a => a ~> (TerminalObject :: LIFTED p q) Source Comments #

terminate' :: forall (a :: LIFTED p q) (a' :: LIFTED p q). (a ~> a') -> a ~> (TerminalObject :: LIFTED p q) Source Comments #

Adjunction p q => Profunctor (Lift :: LIFTED p q -> LIFTED p q -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Lifted

Methods

dimap :: forall (c :: LIFTED p q) (a :: LIFTED p q) (b :: LIFTED p q) (d :: LIFTED p q). (c ~> a) -> (b ~> d) -> Lift a b -> Lift c d Source Comments #

(\\) :: forall (a :: LIFTED p q) (b :: LIFTED p q) r. ((Ob a, Ob b) => r) -> Lift a b -> r Source Comments #

Adjunction p q => Promonad (Lift :: LIFTED p q -> LIFTED p q -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Lifted

Methods

id :: forall (a :: LIFTED p q). Ob a => Lift a a Source Comments #

(.) :: forall (b :: LIFTED p q) (c :: LIFTED p q) (a :: LIFTED p q). Lift b c -> Lift a b -> Lift a c Source Comments #

type UN ('LIFT :: j1 -> LIFTED p q) ('LIFT j2 :: LIFTED p q) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Lifted

type UN ('LIFT :: j1 -> LIFTED p q) ('LIFT j2 :: LIFTED p q) = j2

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Lifted

type (~>) = Lift :: LIFTED p q -> LIFTED p q -> Type

type InitialObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Lifted

type InitialObject = 'LIFT (InitialObject :: j) :: LIFTED p q

type TerminalObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Lifted

type TerminalObject = 'LIFT (TerminalObject :: j) :: LIFTED p q

type Ob (a :: LIFTED p q) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Lifted

type Ob (a :: LIFTED p q) = (Is ('LIFT :: j -> LIFTED p q) a, Ob (UN ('LIFT :: j -> LIFTED p q) a))

type ('LIFT a :: LIFTED p q) || ('LIFT b :: LIFTED p q) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Lifted

type ('LIFT a :: LIFTED p q) || ('LIFT b :: LIFTED p q) = 'LIFT (a || b) :: LIFTED p q

type ('LIFT a :: LIFTED p q) && ('LIFT b :: LIFTED p q) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Lifted

type ('LIFT a :: LIFTED p q) && ('LIFT b :: LIFTED p q) = 'LIFT (a && b) :: LIFTED p q

data Lift (a :: LIFTED p q) (b :: LIFTED p1 q1) where Source Comments #

A category lifted by an adjunction.

Constructors

Lift :: forall {j} {i} {k} {p1 :: i +-> k} {q1 :: k +-> i} (q :: j +-> i) (p :: i +-> j) (a1 :: i) (b1 :: i). (q :.: p) a1 b1 -> Lift ('LIFT a1 :: LIFTED p q) ('LIFT b1 :: LIFTED p1 q1)

Instances

Instances details

Adjunction p q => Profunctor (Lift :: LIFTED p q -> LIFTED p q -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Lifted Methods dimap :: forall (c :: LIFTED p q) (a :: LIFTED p q) (b :: LIFTED p q) (d :: LIFTED p q). (c ~> a) -> (b ~> d) -> Lift a b -> Lift c d Source Comments # (\\) :: forall (a :: LIFTED p q) (b :: LIFTED p q) r. ((Ob a, Ob b) => r) -> Lift a b -> r Source Comments #
Adjunction p q => Promonad (Lift :: LIFTED p q -> LIFTED p q -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Lifted Methods id :: forall (a :: LIFTED p q). Ob a => Lift a a Source Comments # (.) :: forall (b :: LIFTED p q) (c :: LIFTED p q) (a :: LIFTED p q). Lift b c -> Lift a b -> Lift a c Source Comments #

type LIFTEDF (f :: j -> k) = LIFTED (Star f) (Costar f) Source Comments #

Categories lifted by a functor: f a ~> f b.

pattern LiftF :: forall {j1} {j2} {k} {p} {q} (f :: j1 -> j2) (a :: j1) (b :: j1). Functor f => (Ob a, Ob b) => (f a ~> f b) -> Lift ('LIFT a :: LIFTED (Star f) (Costar f)) ('LIFT b :: LIFTED p q) Source Comments #