Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.CatProf

Documentation

newtype KIND Source Github #

Constructors

K Kind

Instances

Instances details

Monoidal KIND Source Github #

Products as monoidal structure.

Instance details

Defined in Proarrow.Category.Instance.CatProf

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.CatProf type Unit = 'K ()
type (l :: KIND) ** (r :: KIND)
Instance details Defined in Proarrow.Category.Instance.CatProf type (l :: KIND) ** (r :: KIND) = 'K (UN 'K l, UN 'K r)

Methods

withOb2 :: forall (a :: KIND) (b :: KIND) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Github #

leftUnitor :: forall (a :: KIND). Ob a => ((Unit :: KIND) ** a) ~> a Source Github #

leftUnitorInv :: forall (a :: KIND). Ob a => a ~> ((Unit :: KIND) ** a) Source Github #

rightUnitor :: forall (a :: KIND). Ob a => (a ** (Unit :: KIND)) ~> a Source Github #

rightUnitorInv :: forall (a :: KIND). Ob a => a ~> (a ** (Unit :: KIND)) Source Github #

associator :: forall (a :: KIND) (b :: KIND) (c :: KIND). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Github #

associatorInv :: forall (a :: KIND) (b :: KIND) (c :: KIND). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Github #

SymMonoidal KIND Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Methods

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

Closed KIND Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Associated Types

type ('K a :: KIND) ~~> ('K b :: KIND)
Instance details Defined in Proarrow.Category.Instance.CatProf type ('K a :: KIND) ~~> ('K b :: KIND) = 'K (OPPOSITE a, b)

Methods

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

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

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

(^^^) :: forall (a :: KIND) (b :: KIND) (x :: KIND) (y :: KIND). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Github #

CompactClosed KIND Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Methods

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

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

CopyDiscard KIND Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Methods

copy :: forall (a :: KIND). Ob a => a ~> (a ** a) Source Github #

discard :: forall (a :: KIND). Ob a => a ~> (Unit :: KIND) Source Github #

Distributive KIND Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Methods

distL :: forall (a :: KIND) (b :: KIND) (c :: KIND). (Ob a, Ob b, Ob c) => (a ** (b || c)) ~> ((a ** b) || (a ** c)) Source Github #

distR :: forall (a :: KIND) (b :: KIND) (c :: KIND). (Ob a, Ob b, Ob c) => ((a || b) ** c) ~> ((a ** c) || (b ** c)) Source Github #

absorbL :: forall (a :: KIND). Ob a => (a ** (InitialObject :: KIND)) ~> (InitialObject :: KIND) Source Github #

absorbR :: forall (a :: KIND). Ob a => ((InitialObject :: KIND) ** a) ~> (InitialObject :: KIND) Source Github #

StarAutonomous KIND Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Associated Types

type Dual ('K a :: KIND)
Instance details Defined in Proarrow.Category.Instance.CatProf type Dual ('K a :: KIND) = 'K (OPPOSITE a)

Methods

dual :: forall (a :: KIND) (b :: KIND). (a ~> b) -> Dual b ~> Dual a Source Github #

dualInv :: forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> a Source Github #

linDist :: forall (a :: KIND) (b :: KIND) (c :: KIND). (Ob a, Ob b, Ob c) => ((a ** b) ~> Dual c) -> a ~> Dual (b ** c) Source Github #

linDistInv :: forall (a :: KIND) (b :: KIND) (c :: KIND). (Ob a, Ob b, Ob c) => (a ~> Dual (b ** c)) -> (a ** b) ~> Dual c Source Github #

HasBinaryCoproducts KIND Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Associated Types

type ('K l :: KIND) \|\| ('K r :: KIND)
Instance details Defined in Proarrow.Category.Instance.CatProf type ('K l :: KIND) \|\| ('K r :: KIND) = 'K (l, r)

Methods

withObCoprod :: forall (a :: KIND) (b :: KIND) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Github #

lft :: forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => a ~> (a || b) Source Github #

rgt :: forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => b ~> (a || b) Source Github #

(|||) :: forall (x :: KIND) (a :: KIND) (y :: KIND). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Github #

(+++) :: forall (a :: KIND) (b :: KIND) (x :: KIND) (y :: KIND). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Github #

HasBiproducts KIND Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Methods

sum :: forall (a :: KIND) (b :: KIND). (a ~> b) -> (a ~> b) -> a ~> b Source Github #

HasInitialObject KIND Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.CatProf type InitialObject = 'K ()

Methods

initiate :: forall (a :: KIND). Ob a => (InitialObject :: KIND) ~> a Source Github #

HasParamNNO KIND Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Associated Types

type NNO
Instance details Defined in Proarrow.Category.Instance.CatProf type NNO = 'K (DISCRETE Nat)

Methods

zero :: (Unit :: KIND) ~> (NNO :: KIND) Source Github #

succ :: (NNO :: KIND) ~> (NNO :: KIND) Source Github #

nnoUniv :: forall (a :: KIND) (x :: KIND). (a ~> x) -> (x ~> x) -> (a ** (NNO :: KIND)) ~> x Source Github #

CategoryOf KIND Source Github #

The category of categories and profunctors between them.

Instance details

Defined in Proarrow.Category.Instance.CatProf

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.CatProf type (~>) = Cat
type Ob (c :: KIND)
Instance details Defined in Proarrow.Category.Instance.CatProf type Ob (c :: KIND) = (Is 'K c, CategoryOf (UN 'K c))

HasBinaryProducts KIND Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Associated Types

type (l :: KIND) && (r :: KIND)
Instance details Defined in Proarrow.Category.Instance.CatProf type (l :: KIND) && (r :: KIND) = 'K (UN 'K l, UN 'K r)

Methods

withObProd :: forall (a :: KIND) (b :: KIND) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: KIND) (x :: KIND) (y :: KIND). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: KIND) (b :: KIND) (x :: KIND) (y :: KIND). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

HasTerminalObject KIND Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.CatProf type TerminalObject = 'K ()

Methods

terminate :: forall (a :: KIND). Ob a => a ~> (TerminalObject :: KIND) Source Github #

Promonad Cat Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Methods

id :: forall (a :: KIND). Ob a => Cat a a Source Github #

(.) :: forall (b :: KIND) (c :: KIND) (a :: KIND). Cat b c -> Cat a b -> Cat a c Source Github #

Ob a => Comonoid (a :: KIND) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Methods

counit :: a ~> (Unit :: KIND) Source Github #

comult :: a ~> (a ** a) Source Github #

MonoidalProfunctor Cat Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Methods

one :: Cat (Unit :: KIND) (Unit :: KIND) Source Github #

(**) :: forall (x1 :: KIND) (x2 :: KIND) (y1 :: KIND) (y2 :: KIND). Cat x1 x2 -> Cat y1 y2 -> Cat (x1 ** y1) (x2 ** y2) Source Github #

Profunctor Cat Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Methods

dimap :: forall (c :: KIND) (a :: KIND) (b :: KIND) (d :: KIND). (c ~> a) -> (b ~> d) -> Cat a b -> Cat c d Source Github #

lmap :: forall (c :: KIND) (a :: KIND) (b :: KIND). (c ~> a) -> Cat a b -> Cat c b Source Github #

rmap :: forall (b :: KIND) (d :: KIND) (a :: KIND). (b ~> d) -> Cat a b -> Cat a d Source Github #

(\\) :: forall (a :: KIND) (b :: KIND) r. ((Ob a, Ob b) => r) -> Cat a b -> r Source Github #

MonoidalAction t => Costrong (t :: (KIND, KIND) +-> KIND) Cat Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Methods

coact :: forall (a :: KIND) (x :: KIND) (y :: KIND). (Ob a, Ob x, Ob y) => Cat (Act t a x) (Act t a y) -> Cat x y Source Github #

Monoidal k => Monoid ('K [k] :: KIND) Source Github #

A strictified monoidal category as a monoid in Cat.

Instance details

Defined in Proarrow.Category.Instance.CatProf

Methods

mempty :: (Unit :: KIND) ~> 'K [k] Source Github #

mappend :: ('K [k] ** 'K [k]) ~> 'K [k] Source Github #

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

type Unit = 'K ()

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

type InitialObject = 'K ()

type NNO Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

type NNO = 'K (DISCRETE Nat)

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

type (~>) = Cat

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

type TerminalObject = 'K ()

type Ob (c :: KIND) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

type Ob (c :: KIND) = (Is 'K c, CategoryOf (UN 'K c))

type (l :: KIND) ** (r :: KIND) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

type (l :: KIND) ** (r :: KIND) = 'K (UN 'K l, UN 'K r)

type (l :: KIND) && (r :: KIND) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

type (l :: KIND) && (r :: KIND) = 'K (UN 'K l, UN 'K r)

type Dual ('K a :: KIND) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

type Dual ('K a :: KIND) = 'K (OPPOSITE a)

type ('K a :: KIND) ~~> ('K b :: KIND) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

type ('K a :: KIND) ~~> ('K b :: KIND) = 'K (OPPOSITE a, b)

type ('K l :: KIND) || ('K r :: KIND) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

type ('K l :: KIND) || ('K r :: KIND) = 'K (l, r)

data Cat (a :: KIND) (b :: KIND) where Source Github #

Constructors

Cat :: forall {j} {k} (p :: j +-> k). Profunctor p => Cat ('K j) ('K k)

Instances

Instances details

Promonad Cat Source Github #
Instance details Defined in Proarrow.Category.Instance.CatProf Methods id :: forall (a :: KIND). Ob a => Cat a a Source Github # (.) :: forall (b :: KIND) (c :: KIND) (a :: KIND). Cat b c -> Cat a b -> Cat a c Source Github #
MonoidalProfunctor Cat Source Github #
Instance details Defined in Proarrow.Category.Instance.CatProf Methods one :: Cat (Unit :: KIND) (Unit :: KIND) Source Github # () :: forall (x1 :: KIND) (x2 :: KIND) (y1 :: KIND) (y2 :: KIND). Cat x1 x2 -> Cat y1 y2 -> Cat (x1 y1) (x2 ** y2) Source Github #
Profunctor Cat Source Github #
Instance details Defined in Proarrow.Category.Instance.CatProf Methods dimap :: forall (c :: KIND) (a :: KIND) (b :: KIND) (d :: KIND). (c ~> a) -> (b ~> d) -> Cat a b -> Cat c d Source Github # lmap :: forall (c :: KIND) (a :: KIND) (b :: KIND). (c ~> a) -> Cat a b -> Cat c b Source Github # rmap :: forall (b :: KIND) (d :: KIND) (a :: KIND). (b ~> d) -> Cat a b -> Cat a d Source Github # (\\) :: forall (a :: KIND) (b :: KIND) r. ((Ob a, Ob b) => r) -> Cat a b -> r Source Github #
MonoidalAction t => Costrong (t :: (KIND, KIND) +-> KIND) Cat Source Github #
Instance details Defined in Proarrow.Category.Instance.CatProf Methods coact :: forall (a :: KIND) (x :: KIND) (y :: KIND). (Ob a, Ob x, Ob y) => Cat (Act t a x) (Act t a y) -> Cat x y Source Github #

data family Swap :: (j, k) +-> (k, j) Source Github #

Instances

Instances details

(CategoryOf j, CategoryOf k) => FunctorForRep (Swap :: (j, k) +-> (k, j)) Source Github #
Instance details Defined in Proarrow.Category.Instance.CatProf Methods fmap :: forall (a :: (j, k)) (b :: (j, k)). (a ~> b) -> ((Swap :: (j, k) +-> (k, j)) @ a) ~> ((Swap :: (j, k) +-> (k, j)) @ b) Source Github #
type (Swap :: (j, k) +-> (k, j)) @ ('(a, b) :: (j, k)) Source Github #
Instance details Defined in Proarrow.Category.Instance.CatProf type (Swap :: (j, k) +-> (k, j)) @ ('(a, b) :: (j, k)) = '(b, a)

data Curry (p :: (i, j) +-> k) (a :: (OPPOSITE j, k)) (b :: i) where Source Github #

Constructors

Curry :: forall {i} {j} {k} (p :: (i, j) +-> k) (c :: k) (b :: i) (b1 :: j). p c '(b, b1) -> Curry p '('OP b1, c) b

Instances

Instances details

(Profunctor p, CategoryOf i, CategoryOf j) => Profunctor (Curry p :: (OPPOSITE j, k) -> i -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Methods

dimap :: forall (c :: (OPPOSITE j, k)) (a :: (OPPOSITE j, k)) (b :: i) (d :: i). (c ~> a) -> (b ~> d) -> Curry p a b -> Curry p c d Source Github #

lmap :: forall (c :: (OPPOSITE j, k)) (a :: (OPPOSITE j, k)) (b :: i). (c ~> a) -> Curry p a b -> Curry p c b Source Github #

rmap :: forall (b :: i) (d :: i) (a :: (OPPOSITE j, k)). (b ~> d) -> Curry p a b -> Curry p a d Source Github #

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

data Uncurry (p :: i +-> (OPPOSITE j, k)) (a :: k) (b :: (i, j)) where Source Github #

Constructors

Uncurry :: forall {i} {j} {k} (p :: i +-> (OPPOSITE j, k)) (b1 :: j) (a :: k) (a1 :: i). p '('OP b1, a) a1 -> Uncurry p a '(a1, b1)

Instances

Instances details

(Profunctor p, CategoryOf j, CategoryOf k) => Profunctor (Uncurry p :: k -> (i, j) -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Methods

dimap :: forall (c :: k) (a :: k) (b :: (i, j)) (d :: (i, j)). (c ~> a) -> (b ~> d) -> Uncurry p a b -> Uncurry p c d Source Github #

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

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

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

data family CombineDual :: (OPPOSITE j, OPPOSITE k) +-> OPPOSITE (j, k) Source Github #

Instances

Instances details

(CategoryOf j, CategoryOf k) => FunctorForRep (CombineDual :: (OPPOSITE j, OPPOSITE k) +-> OPPOSITE (j, k)) Source Github #
Instance details Defined in Proarrow.Category.Instance.CatProf Methods fmap :: forall (a :: (OPPOSITE j, OPPOSITE k)) (b :: (OPPOSITE j, OPPOSITE k)). (a ~> b) -> ((CombineDual :: (OPPOSITE j, OPPOSITE k) +-> OPPOSITE (j, k)) @ a) ~> ((CombineDual :: (OPPOSITE j, OPPOSITE k) +-> OPPOSITE (j, k)) @ b) Source Github #
type (CombineDual :: (OPPOSITE j, OPPOSITE k) +-> OPPOSITE (j, k)) @ ('('OP a, 'OP b) :: (OPPOSITE j, OPPOSITE k)) Source Github #
Instance details Defined in Proarrow.Category.Instance.CatProf type (CombineDual :: (OPPOSITE j, OPPOSITE k) +-> OPPOSITE (j, k)) @ ('('OP a, 'OP b) :: (OPPOSITE j, OPPOSITE k)) = 'OP '(a, b)

data family DistribDual :: OPPOSITE (j, k) +-> (OPPOSITE j, OPPOSITE k) Source Github #

Instances

Instances details

(CategoryOf j, CategoryOf k) => FunctorForRep (DistribDual :: OPPOSITE (j, k) +-> (OPPOSITE j, OPPOSITE k)) Source Github #
Instance details Defined in Proarrow.Category.Instance.CatProf Methods fmap :: forall (a :: OPPOSITE (j, k)) (b :: OPPOSITE (j, k)). (a ~> b) -> ((DistribDual :: OPPOSITE (j, k) +-> (OPPOSITE j, OPPOSITE k)) @ a) ~> ((DistribDual :: OPPOSITE (j, k) +-> (OPPOSITE j, OPPOSITE k)) @ b) Source Github #
type (DistribDual :: OPPOSITE (j, k) +-> (OPPOSITE j, OPPOSITE k)) @ ('OP '(a, b) :: OPPOSITE (j, k)) Source Github #
Instance details Defined in Proarrow.Category.Instance.CatProf type (DistribDual :: OPPOSITE (j, k) +-> (OPPOSITE j, OPPOSITE k)) @ ('OP '(a, b) :: OPPOSITE (j, k)) = '('OP a, 'OP b)

data family DualUnit :: OPPOSITE () +-> () Source Github #

Instances

Instances details

FunctorForRep DualUnit Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Associated Types

type DualUnit @ ('OP '())
Instance details Defined in Proarrow.Category.Instance.CatProf type DualUnit @ ('OP '()) = '()

Methods

fmap :: forall (a :: OPPOSITE ()) (b :: OPPOSITE ()). (a ~> b) -> (DualUnit @ a) ~> (DualUnit @ b) Source Github #

type DualUnit @ ('OP '()) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

type DualUnit @ ('OP '()) = '()

data family Succ :: DISCRETE Nat +-> DISCRETE Nat Source Github #

Instances

Instances details

FunctorForRep Succ Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Associated Types

type Succ @ ('D n :: DISCRETE Nat)
Instance details Defined in Proarrow.Category.Instance.CatProf type Succ @ ('D n :: DISCRETE Nat) = 'D ('S n)

Methods

fmap :: forall (a :: DISCRETE Nat) (b :: DISCRETE Nat). (a ~> b) -> (Succ @ a) ~> (Succ @ b) Source Github #

type Succ @ ('D n :: DISCRETE Nat) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

type Succ @ ('D n :: DISCRETE Nat) = 'D ('S n)

data NNOUniv (z :: a +-> x) (s :: x +-> x) (a1 :: x) (b :: (a, DISCRETE Nat)) where Source Github #

Constructors

NNOZ :: forall {x} {a} (a1 :: x) (z :: a +-> x) (a2 :: a) (s :: x +-> x). Ob a1 => z a1 a2 -> NNOUniv z s a1 '(a2, 'D 'Z)
NNOS :: forall {x} {a} (s :: x +-> x) (z :: a +-> x) (a1 :: x) (a2 :: a) (n :: Nat). (s :.: NNOUniv z s) a1 '(a2, 'D n) -> NNOUniv z s a1 '(a2, 'D ('S n))

Instances

Instances details

(Profunctor z, Profunctor s) => Profunctor (NNOUniv z s :: k -> (a, DISCRETE Nat) -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatProf

Methods

dimap :: forall (c :: k) (a0 :: k) (b :: (a, DISCRETE Nat)) (d :: (a, DISCRETE Nat)). (c ~> a0) -> (b ~> d) -> NNOUniv z s a0 b -> NNOUniv z s c d Source Github #

lmap :: forall (c :: k) (a0 :: k) (b :: (a, DISCRETE Nat)). (c ~> a0) -> NNOUniv z s a0 b -> NNOUniv z s c b Source Github #

rmap :: forall (b :: (a, DISCRETE Nat)) (d :: (a, DISCRETE Nat)) (a0 :: k). (b ~> d) -> NNOUniv z s a0 b -> NNOUniv z s a0 d Source Github #

(\\) :: forall (a0 :: k) (b :: (a, DISCRETE Nat)) r. ((Ob a0, Ob b) => r) -> NNOUniv z s a0 b -> r Source Github #