Safe Haskell	None
Language	GHC2024

Proarrow.Universal

Synopsis

class (Representable r, Ob a) => 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, Ob b) => 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 (r :: k -> k1 -> Type) (a :: k) (b :: k1) = AsRightAdjoint {
- unAsRightAdjoint :: r a b
}
newtype AsLeftAdjoint (l :: k -> k1 -> Type) (a :: k) (b :: k1) = AsLeftAdjoint {
- unAsLeftAdjoint :: l a b
}
newtype FromAdjunction (p :: k -> k1 -> Type) (a :: k) (b :: k1) = FromAdjunction {
- unFromAdjunction :: p a b
}

Documentation

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

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

Methods

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

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

Instances

Instances details

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

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

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

TermUniversal l b => InitUniversal (Op l :: OPPOSITE k1 -> OPPOSITE k2 -> Type) ('OP b :: OPPOSITE k1) Source Github #

Instance details

Defined in Proarrow.Universal

Associated Types

type L (Op l :: OPPOSITE k1 -> OPPOSITE k2 -> Type) ('OP b :: OPPOSITE k1)
Instance details Defined in Proarrow.Universal type L (Op l :: OPPOSITE k1 -> OPPOSITE k2 -> Type) ('OP b :: OPPOSITE k1) = 'OP (R l b)

Methods

initUnivArr :: Op l ('OP b) (L (Op l) ('OP b)) Source Github #

initUnivProp :: forall (b0 :: OPPOSITE k2). Op l ('OP b) b0 -> L (Op l) ('OP b) ~> b0 Source Github #

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

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

Methods

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

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

Instances

Instances details

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

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

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

InitUniversal r a => TermUniversal (Op r :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE k) Source Github #

Instance details

Defined in Proarrow.Universal

Associated Types

type R (Op r :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE k)
Instance details Defined in Proarrow.Universal type R (Op r :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE k) = 'OP (L r a)

Methods

termUnivArr :: Op r (R (Op r) ('OP a)) ('OP a) Source Github #

termUnivProp :: forall (a0 :: OPPOSITE j). Op r a0 ('OP a) -> a0 ~> R (Op r) ('OP a) Source Github #

newtype AsRightAdjoint (r :: k -> k1 -> Type) (a :: k) (b :: k1) Source Github #

Constructors

AsRightAdjoint
Fields unAsRightAdjoint :: r a b

Instances

Instances details

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

newtype AsLeftAdjoint (l :: k -> k1 -> Type) (a :: k) (b :: k1) Source Github #

Constructors

AsLeftAdjoint
Fields unAsLeftAdjoint :: l a b

Instances

Instances details

Profunctor l => Profunctor (AsLeftAdjoint l :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Universal Methods dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> AsLeftAdjoint l a b -> AsLeftAdjoint l c d Source Github # lmap :: forall (c :: k) (a :: k) (b :: j). (c ~> a) -> AsLeftAdjoint l a b -> AsLeftAdjoint l c b Source Github # rmap :: forall (b :: j) (d :: j) (a :: k). (b ~> d) -> AsLeftAdjoint l a b -> AsLeftAdjoint l a d Source Github # (\\) :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> AsLeftAdjoint l a b -> r Source Github #
Corepresentable l => Corepresentable (AsLeftAdjoint l :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Universal Methods coindex :: forall (a :: k) (b :: j). AsLeftAdjoint l a b -> (AsLeftAdjoint l %% a) ~> b Source Github # cotabulate :: forall (a :: k) (b :: j). Ob a => ((AsLeftAdjoint l %% a) ~> b) -> AsLeftAdjoint l a b Source Github # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (AsLeftAdjoint l %% a) ~> (AsLeftAdjoint l %% b) Source Github # trivialCorep :: forall (a :: k). Ob a => AsLeftAdjoint l a (AsLeftAdjoint l %% a) Source Github #
(forall (b :: j). Ob b => TermUniversal l b, Corepresentable l) => Representable (AsLeftAdjoint l :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Universal Methods index :: forall (a :: k) (b :: j). AsLeftAdjoint l a b -> a ~> (AsLeftAdjoint l % b) Source Github # tabulate :: forall (b :: j) (a :: k). Ob b => (a ~> (AsLeftAdjoint l % b)) -> AsLeftAdjoint l a b Source Github # repMap :: forall (a :: j) (b :: j). (a ~> b) -> (AsLeftAdjoint l % a) ~> (AsLeftAdjoint l % b) Source Github # trivialRep :: forall (a :: j). Ob a => AsLeftAdjoint l (AsLeftAdjoint l % a) a Source Github #
type (AsLeftAdjoint l :: k -> j -> Type) %% (a :: k) Source Github #
Instance details Defined in Proarrow.Universal type (AsLeftAdjoint l :: k -> j -> Type) %% (a :: k) = l %% a
type (AsLeftAdjoint l :: k -> j -> Type) % (b :: j) Source Github #
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 Github #

Constructors

FromAdjunction
Fields unFromAdjunction :: p a b

Instances

Instances details

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

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

lmap :: forall (c :: k) (a :: k) (b :: j). (c ~> a) -> FromAdjunction p a b -> FromAdjunction p c b Source Github #

rmap :: forall (b :: j) (d :: j) (a :: k). (b ~> d) -> FromAdjunction p a b -> FromAdjunction p a d Source Github #

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

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

Instance details

Defined in Proarrow.Universal

Methods

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

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

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

trivialCorep :: forall (a :: k). Ob a => FromAdjunction p a (FromAdjunction p %% a) Source Github #

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

Instance details

Defined in Proarrow.Universal

Methods

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

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

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

trivialRep :: forall (a :: j). Ob a => FromAdjunction p (FromAdjunction p % a) a Source Github #

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

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

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

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

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

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

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

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

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

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

Instance details

Defined in Proarrow.Universal

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