Safe Haskell	None
Language	GHC2024

Proarrow.Universal

Synopsis

class Representable r => InitUniversal (r :: j +-> k) (a :: k) where
- type L (r :: j +-> k) (a :: k) :: j
- initUnivArr :: r a (L r a)
- initUnivProp :: forall (b :: j). r a b -> L r a ~> b
class Corepresentable l => TermUniversal (l :: j +-> k) (b :: j) where
- type R (l :: j +-> k) (b :: j) :: k
- termUnivArr :: l (R l b) b
- termUnivProp :: forall (a :: k). l a b -> a ~> R l b
newtype AsRightAdjoint (p :: k -> k1 -> Type) (a :: k) (b :: k1) = AsRightAdjoint {
- unAsRightAdjoint :: p a b
}
newtype AsLeftAdjoint (p :: k -> k1 -> Type) (a :: k) (b :: k1) = AsLeftAdjoint {
- unAsLeftAdjoint :: p a b
}
newtype FromAdjunction (p :: k -> k1 -> Type) (a :: k) (b :: k1) = FromAdjunction {
- unFromAdjunction :: p a b
}

Documentation

class Representable r => InitUniversal (r :: j +-> k) (a :: k) where Source Comments #

The initial universal property of a functor r (as a representable profunctor) and an object a.

Associated Types

type L (r :: j +-> k) (a :: k) :: j Source Comments #

Methods

initUnivArr :: r a (L r a) Source Comments #

initUnivProp :: forall (b :: j). r a b -> L r a ~> b Source Comments #

Instances

Instances details

Adjunction p => InitUniversal (FromAdjunction p :: k -> j -> Type) (a :: k) Source Comments #

Instance details

Defined in Proarrow.Universal

Associated Types

type L (FromAdjunction p :: k -> j -> Type) (a :: k)
Instance details Defined in Proarrow.Universal type L (FromAdjunction p :: k -> j -> Type) (a :: k) = p %% a

Methods

initUnivArr :: FromAdjunction p a (L (FromAdjunction p) a) Source Comments #

initUnivProp :: forall (b :: j). FromAdjunction p a b -> L (FromAdjunction p) a ~> b Source Comments #

class Corepresentable l => TermUniversal (l :: j +-> k) (b :: j) where Source Comments #

The terminal universal property of a functor l (as a corepresentable profunctor) and an object b.

Associated Types

type R (l :: j +-> k) (b :: j) :: k Source Comments #

Methods

termUnivArr :: l (R l b) b Source Comments #

termUnivProp :: forall (a :: k). l a b -> a ~> R l b Source Comments #

Instances

Instances details

Adjunction p => TermUniversal (FromAdjunction p :: k -> j -> Type) (b :: j) Source Comments #

Instance details

Defined in Proarrow.Universal

Associated Types

type R (FromAdjunction p :: k -> j -> Type) (b :: j)
Instance details Defined in Proarrow.Universal type R (FromAdjunction p :: k -> j -> Type) (b :: j) = p % b

Methods

termUnivArr :: FromAdjunction p (R (FromAdjunction p) b) b Source Comments #

termUnivProp :: forall (a :: k). FromAdjunction p a b -> a ~> R (FromAdjunction p) b Source Comments #

newtype AsRightAdjoint (p :: k -> k1 -> Type) (a :: k) (b :: k1) Source Comments #

Constructors

AsRightAdjoint
Fields unAsRightAdjoint :: p a b

Instances

Instances details

Profunctor p => Profunctor (AsRightAdjoint p :: k -> j -> Type) Source Comments #
Instance details Defined in Proarrow.Universal Methods dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> AsRightAdjoint p a b -> AsRightAdjoint p c d Source Comments # (\\) :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> AsRightAdjoint p a b -> r Source Comments #
(forall (a :: k). InitUniversal r a) => Corepresentable (AsRightAdjoint r :: k -> j -> Type) Source Comments #
Instance details Defined in Proarrow.Universal Methods coindex :: forall (a :: k) (b :: j). AsRightAdjoint r a b -> (AsRightAdjoint r %% a) ~> b Source Comments # cotabulate :: forall (a :: k) (b :: j). Ob a => ((AsRightAdjoint r %% a) ~> b) -> AsRightAdjoint r a b Source Comments # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (AsRightAdjoint r %% a) ~> (AsRightAdjoint r %% b) Source Comments #
Representable p => Representable (AsRightAdjoint p :: k -> j -> Type) Source Comments #
Instance details Defined in Proarrow.Universal Methods index :: forall (a :: k) (b :: j). AsRightAdjoint p a b -> a ~> (AsRightAdjoint p % b) Source Comments # tabulate :: forall (b :: j) (a :: k). Ob b => (a ~> (AsRightAdjoint p % b)) -> AsRightAdjoint p a b Source Comments # repMap :: forall (a :: j) (b :: j). (a ~> b) -> (AsRightAdjoint p % a) ~> (AsRightAdjoint p % b) Source Comments #
type (AsRightAdjoint r :: k -> j -> Type) %% (a :: k) Source Comments #
Instance details Defined in Proarrow.Universal type (AsRightAdjoint r :: k -> j -> Type) %% (a :: k) = L r a
type (AsRightAdjoint p :: k -> j -> Type) % (a :: j) Source Comments #
Instance details Defined in Proarrow.Universal type (AsRightAdjoint p :: k -> j -> Type) % (a :: j) = p % a

newtype AsLeftAdjoint (p :: k -> k1 -> Type) (a :: k) (b :: k1) Source Comments #

Constructors

AsLeftAdjoint
Fields unAsLeftAdjoint :: p a b

Instances

Instances details

Profunctor p => Profunctor (AsLeftAdjoint p :: k -> j -> Type) Source Comments #
Instance details Defined in Proarrow.Universal Methods dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> AsLeftAdjoint p a b -> AsLeftAdjoint p c d Source Comments # (\\) :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> AsLeftAdjoint p a b -> r Source Comments #
Corepresentable p => Corepresentable (AsLeftAdjoint p :: k -> j -> Type) Source Comments #
Instance details Defined in Proarrow.Universal Methods coindex :: forall (a :: k) (b :: j). AsLeftAdjoint p a b -> (AsLeftAdjoint p %% a) ~> b Source Comments # cotabulate :: forall (a :: k) (b :: j). Ob a => ((AsLeftAdjoint p %% a) ~> b) -> AsLeftAdjoint p a b Source Comments # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (AsLeftAdjoint p %% a) ~> (AsLeftAdjoint p %% b) Source Comments #
(forall (b :: j). TermUniversal l b) => Representable (AsLeftAdjoint l :: k -> j -> Type) Source Comments #
Instance details Defined in Proarrow.Universal Methods index :: forall (a :: k) (b :: j). AsLeftAdjoint l a b -> a ~> (AsLeftAdjoint l % b) Source Comments # tabulate :: forall (b :: j) (a :: k). Ob b => (a ~> (AsLeftAdjoint l % b)) -> AsLeftAdjoint l a b Source Comments # repMap :: forall (a :: j) (b :: j). (a ~> b) -> (AsLeftAdjoint l % a) ~> (AsLeftAdjoint l % b) Source Comments #
type (AsLeftAdjoint p :: k -> j -> Type) %% (a :: k) Source Comments #
Instance details Defined in Proarrow.Universal type (AsLeftAdjoint p :: k -> j -> Type) %% (a :: k) = p %% a
type (AsLeftAdjoint l :: k -> j -> Type) % (b :: j) Source Comments #
Instance details Defined in Proarrow.Universal type (AsLeftAdjoint l :: k -> j -> Type) % (b :: j) = R l b

newtype FromAdjunction (p :: k -> k1 -> Type) (a :: k) (b :: k1) Source Comments #

Constructors

FromAdjunction
Fields unFromAdjunction :: p a b

Instances

Instances details

Profunctor p => Profunctor (FromAdjunction p :: k -> j -> Type) Source Comments #

Instance details

Defined in Proarrow.Universal

Methods

dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> FromAdjunction p a b -> FromAdjunction p c d Source Comments #

(\\) :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> FromAdjunction p a b -> r Source Comments #

Corepresentable p => Corepresentable (FromAdjunction p :: k -> j -> Type) Source Comments #

Instance details

Defined in Proarrow.Universal

Methods

coindex :: forall (a :: k) (b :: j). FromAdjunction p a b -> (FromAdjunction p %% a) ~> b Source Comments #

cotabulate :: forall (a :: k) (b :: j). Ob a => ((FromAdjunction p %% a) ~> b) -> FromAdjunction p a b Source Comments #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (FromAdjunction p %% a) ~> (FromAdjunction p %% b) Source Comments #

Representable p => Representable (FromAdjunction p :: k -> j -> Type) Source Comments #

Instance details

Defined in Proarrow.Universal

Methods

index :: forall (a :: k) (b :: j). FromAdjunction p a b -> a ~> (FromAdjunction p % b) Source Comments #

tabulate :: forall (b :: j) (a :: k). Ob b => (a ~> (FromAdjunction p % b)) -> FromAdjunction p a b Source Comments #

repMap :: forall (a :: j) (b :: j). (a ~> b) -> (FromAdjunction p % a) ~> (FromAdjunction p % b) Source Comments #

Adjunction p => InitUniversal (FromAdjunction p :: k -> j -> Type) (a :: k) Source Comments #

Instance details

Defined in Proarrow.Universal

Associated Types

type L (FromAdjunction p :: k -> j -> Type) (a :: k)
Instance details Defined in Proarrow.Universal type L (FromAdjunction p :: k -> j -> Type) (a :: k) = p %% a

Methods

initUnivArr :: FromAdjunction p a (L (FromAdjunction p) a) Source Comments #

initUnivProp :: forall (b :: j). FromAdjunction p a b -> L (FromAdjunction p) a ~> b Source Comments #

Adjunction p => TermUniversal (FromAdjunction p :: k -> j -> Type) (b :: j) Source Comments #

Instance details

Defined in Proarrow.Universal

Associated Types

type R (FromAdjunction p :: k -> j -> Type) (b :: j)
Instance details Defined in Proarrow.Universal type R (FromAdjunction p :: k -> j -> Type) (b :: j) = p % b

Methods

termUnivArr :: FromAdjunction p (R (FromAdjunction p) b) b Source Comments #

termUnivProp :: forall (a :: k). FromAdjunction p a b -> a ~> R (FromAdjunction p) b Source Comments #

type (FromAdjunction p :: k -> j -> Type) %% (a :: k) Source Comments #

Instance details

Defined in Proarrow.Universal

type (FromAdjunction p :: k -> j -> Type) %% (a :: k) = p %% a

type (FromAdjunction p :: k -> j -> Type) % (a :: j) Source Comments #

Instance details

Defined in Proarrow.Universal

type (FromAdjunction p :: k -> j -> Type) % (a :: j) = p % a

type L (FromAdjunction p :: k -> j -> Type) (a :: k) Source Comments #

Instance details

Defined in Proarrow.Universal

type L (FromAdjunction p :: k -> j -> Type) (a :: k) = p %% a

type R (FromAdjunction p :: k -> j -> Type) (b :: j) Source Comments #

Instance details

Defined in Proarrow.Universal

type R (FromAdjunction p :: k -> j -> Type) (b :: j) = p % b