proarrow
Safe HaskellNone
LanguageGHC2024

Proarrow.Limit.BinaryProduct

Description

Binary products: HasBinaryProducts provides a && b with projections fst/snd and pairing (&&&), and HasProducts adds the terminal object. Also Cartesian (the monoidal tensor is the product) and the PROD kind wrapper, which makes (&&) the tensor of a monoidal structure on the same objects.

Synopsis

Documentation

class CategoryOf k => HasBinaryProducts k where Source Github #

Binary products: an object a && b with projections fst and snd, universal among all pairs of arrows out of a common source. Each such pair factors through it uniquely via (&&&).

Laws:

Checked by testBinaryProducts.

Minimal complete definition

withObProd, fst, snd, (&&&)

Associated Types

type (a :: k) && (b :: k) :: k infixl 5 Source Github #

The product object.

Methods

withObProd :: 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 factors.

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

The left projection.

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

The right projection.

(&&&) :: forall (a :: k) (x :: k) (y :: k). (a ~> x) -> (a ~> y) -> a ~> (x && y) infixl 5 Source Github #

The mediating arrow: pairs two arrows out of a common source.

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

The product of two arrows, acting on each factor independently.

Instances

Instances details
HasBinaryProducts BOOL Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Associated Types

type 'FLS && (b :: BOOL) 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type 'FLS && (b :: BOOL) = 'FLS
type 'TRU && (b :: BOOL) 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type 'TRU && (b :: BOOL) = b
type (a :: BOOL) && 'FLS 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (a :: BOOL) && 'FLS = 'FLS
type (a :: BOOL) && 'TRU 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (a :: BOOL) && 'TRU = a

Methods

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

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

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

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

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

HasBinaryProducts CONSTRAINT Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Constraint

Associated Types

type ('CNSTRNT l :: CONSTRAINT) && ('CNSTRNT r :: CONSTRAINT) 
Instance details

Defined in Proarrow.Category.Instance.Constraint

type ('CNSTRNT l :: CONSTRAINT) && ('CNSTRNT r :: CONSTRAINT) = 'CNSTRNT (l, r)

Methods

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

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

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

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

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

HasBinaryProducts COST Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type ('C a :: COST) && ('C b :: COST) 
Instance details

Defined in Proarrow.Category.Instance.Cost

type ('C a :: COST) && ('C b :: COST) = 'C (Max a b)
type 'INF && (b :: COST) 
Instance details

Defined in Proarrow.Category.Instance.Cost

type 'INF && (b :: COST) = 'INF
type (a :: COST) && 'INF 
Instance details

Defined in Proarrow.Category.Instance.Cost

type (a :: COST) && 'INF = 'INF

Methods

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

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

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

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

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

HasBinaryProducts FINHASK Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Associated Types

type ('FH a :: FINHASK) && ('FH b :: FINHASK) 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type ('FH a :: FINHASK) && ('FH b :: FINHASK) = 'FH (a, b)

Methods

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

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

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

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

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

HasBinaryProducts FINREL Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinRel

Associated Types

type (a :: FINREL) && (b :: FINREL) 
Instance details

Defined in Proarrow.Category.Instance.FinRel

type (a :: FINREL) && (b :: FINREL) = 'FR (Plus (UN 'FR a) (UN 'FR b))

Methods

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

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

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

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

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

HasBinaryProducts FINSET Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type ('FS a :: FINSET) && ('FS b :: FINSET) 
Instance details

Defined in Proarrow.Category.Instance.FinSet

type ('FS a :: FINSET) && ('FS b :: FINSET) = 'FS (Mult a b)

Methods

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

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

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

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

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

HasBinaryProducts LINEAR Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type ('L a :: LINEAR) && ('L b :: LINEAR) 
Instance details

Defined in Proarrow.Category.Instance.Linear

type ('L a :: LINEAR) && ('L b :: LINEAR) = 'L (With a b)

Methods

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

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

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

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

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

HasBinaryProducts POINTED Source Github # 
Instance details

Defined in Proarrow.Category.Instance.PointedHask

Associated Types

type ('P a :: POINTED) && ('P b :: POINTED) 
Instance details

Defined in Proarrow.Category.Instance.PointedHask

type ('P a :: POINTED) && ('P b :: POINTED) = 'P (These a b)

Methods

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

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

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

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

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

HasBinaryProducts () Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Associated Types

type (_1 :: ()) && (_2 :: ()) 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (_1 :: ()) && (_2 :: ()) = '()

Methods

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

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

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

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

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

HasBinaryProducts Type Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Associated Types

type (a :: Type) && (b :: Type) 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (a :: Type) && (b :: Type) = (a, b)

Methods

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

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

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

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

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

Indexed k => HasBinaryProducts (CODISCRETE k) Source Github #

Any object works as the product of any two objects here, since every hom-set is a singleton.

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

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

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

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

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

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

HasBinaryProducts k => HasBinaryProducts (FAM k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Fam

Methods

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

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

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

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

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

Num a => HasBinaryProducts (MatK a) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

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

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

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

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

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

HasBinaryCoproducts k => HasBinaryProducts (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

Methods

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

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

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

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

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

HasBinaryProducts (ORDINAL ('S n)) => HasBinaryProducts (ORDINAL ('S ('S n))) Source Github #

Minimum

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

withObProd :: forall (a :: ORDINAL ('S ('S n))) (b :: ORDINAL ('S ('S n))) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: ORDINAL ('S ('S n))) (b :: ORDINAL ('S ('S n))). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: ORDINAL ('S ('S n))) (b :: ORDINAL ('S ('S n))). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: ORDINAL ('S ('S n))) (x :: ORDINAL ('S ('S n))) (y :: ORDINAL ('S ('S n))). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: ORDINAL ('S ('S n))) (b :: ORDINAL ('S ('S n))) (x :: ORDINAL ('S ('S n))) (y :: ORDINAL ('S ('S n))). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

HasBinaryProducts (ORDINAL ('S 'Z)) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

type ('OZ :: ORDINAL ('S 'Z)) && ('OZ :: ORDINAL ('S 'Z)) 
Instance details

Defined in Proarrow.Category.Instance.Ordinal

type ('OZ :: ORDINAL ('S 'Z)) && ('OZ :: ORDINAL ('S 'Z)) = 'OZ :: ORDINAL ('S 'Z)

Methods

withObProd :: forall (a :: ORDINAL ('S 'Z)) (b :: ORDINAL ('S 'Z)) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: ORDINAL ('S 'Z)) (b :: ORDINAL ('S 'Z)). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: ORDINAL ('S 'Z)) (b :: ORDINAL ('S 'Z)). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: ORDINAL ('S 'Z)) (x :: ORDINAL ('S 'Z)) (y :: ORDINAL ('S 'Z)). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: ORDINAL ('S 'Z)) (b :: ORDINAL ('S 'Z)) (x :: ORDINAL ('S 'Z)) (y :: ORDINAL ('S 'Z)). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

HasBinaryProducts (ORDINAL 'Z) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

type (a :: ORDINAL 'Z) && (b :: ORDINAL 'Z) 
Instance details

Defined in Proarrow.Category.Instance.Ordinal

type (a :: ORDINAL 'Z) && (b :: ORDINAL 'Z) = a

Methods

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

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

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

(&&&) :: forall (a :: ORDINAL 'Z) (x :: ORDINAL 'Z) (y :: ORDINAL 'Z). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

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

HasBinaryProducts k => HasBinaryProducts (COPROD k) Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

Methods

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

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

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

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

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

HasBinaryProducts k => HasBinaryProducts (PROD k) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

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

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

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

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

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

(Cartesian k, Comonad p, MonoidalProfunctor p) => HasBinaryProducts (KLEISLI p) Source Github #

Products lift for the same reason as the terminal object: for a Comonad p a (-) is representable, and lmap diag (f ** g) is then the canonical mediating map.

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

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

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

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

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

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

(HasBinaryProducts k, forall (a :: k) (b :: k). (ob a, ob b) => IsObProd ob a b) => HasBinaryProducts (SUBCAT ob) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

Methods

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

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

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

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

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

(CategoryOf j, CategoryOf k) => HasBinaryProducts (j +-> k) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

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

fst :: forall (a :: j +-> k) (b :: j +-> k). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: j +-> k) (b :: j +-> k). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: j +-> k) (x :: j +-> k) (y :: j +-> k). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

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

(HasBinaryProducts j, HasBinaryProducts k) => HasBinaryProducts (j, k) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

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

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

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

(&&&) :: forall (a :: (j, k)) (x :: (j, k)) (y :: (j, k)). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

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

HasBinaryProducts (k1 -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Nat

Methods

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

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

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

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

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

(HasBinaryProducts n, Adjunction adj) => HasBinaryProducts (DUPLOID adj) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Duploid

Methods

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

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

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

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

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

Elem HasBinaryProducts cs => HasBinaryProducts (FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

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

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

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

(&&&) :: forall (a :: FREE cs p) (x :: FREE cs p) (y :: FREE cs p). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

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

fst' :: forall {k} (a :: k) (a' :: k) (b :: k). HasBinaryProducts k => (a ~> a') -> Obj b -> (a && b) ~> a' Source Github #

snd' :: forall {k} (a :: k) (b :: k) (b' :: k). HasBinaryProducts k => Obj a -> (b ~> b') -> (a && b) ~> b' Source Github #

first :: forall {k} (c :: k) (a :: k) (b :: k). (HasBinaryProducts k, Ob c) => (a ~> b) -> (a && c) ~> (b && c) Source Github #

second :: forall {k} (c :: k) (a :: k) (b :: k). (HasBinaryProducts k, Ob c) => (a ~> b) -> (c && a) ~> (c && b) Source Github #

diag :: forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a) Source Github #

data family Product :: k -> k +-> k Source Github #

Instances

Instances details
(HasBinaryProducts k, Ob a) => FunctorForRep (Product a :: k +-> k) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

fmap :: forall (a0 :: k) (b :: k). (a0 ~> b) -> (Product a @ a0) ~> (Product a @ b) Source Github #

(HasBinaryProducts k, Ob s) => AffineFoldFl (Rep (Product s) :: k -> k -> Type) (Corep (Product s) :: k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic.AffineFold

Methods

previewP :: forall (s0 :: k) (a :: k). Bicartesian k => Rep (Product s) s0 a -> s0 ~> (a || (TerminalObject :: k)) Source Github #

(HasBinaryProducts k, Ob s) => FoldFl (Rep (Product s) :: k -> k -> Type) (Corep (Product s) :: k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic.Fold

Methods

foldMapP :: forall (m :: k) (s0 :: k) (a :: k). Monoid m => Rep (Product s) s0 a -> (a ~> m) -> s0 ~> m Source Github #

(HasBinaryProducts k, Ob s) => GetterFl (Rep (Product s) :: k -> k -> Type) (Corep (Product s) :: k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic.Getter

Methods

getP :: forall (s0 :: k) (a :: k). Rep (Product s) s0 a -> s0 ~> a Source Github #

(HasBinaryProducts k, Ob a) => Promonad (Corep (Product a) :: k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

id :: forall (a0 :: k). Ob a0 => Corep (Product a) a0 a0 Source Github #

(.) :: forall (b :: k) (c :: k) (a0 :: k). Corep (Product a) b c -> Corep (Product a) a0 b -> Corep (Product a) a0 c Source Github #

(HasBinaryProducts k, Ob s) => AffineTravFl (Rep (Product s) :: k -> k -> Type) (Corep (Product s) :: k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic.AffineTraversal

Methods

affineMatch :: forall (s0 :: k) (a :: k) (b :: k) (t :: k). Bicartesian k => Rep (Product s) s0 a -> Corep (Product s) b t -> s0 ~> (t || a) Source Github #

affineSet :: forall (s0 :: k) (a :: k) (b :: k) (t :: k). Bicartesian k => Rep (Product s) s0 a -> Corep (Product s) b t -> (s0 && b) ~> t Source Github #

(HasBinaryProducts k, Ob c) => GlassFl (Rep (Product c) :: k -> k -> Type) (Corep (Product c) :: k -> k -> Type) Source Github #

The product pair, a lens witness: the selector is the lens's own get, applied to the source at hand; the residual is kept.

Instance details

Defined in Proarrow.Optic.Glass

Methods

glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k). CCC k => Rep (Product c) s a -> Corep (Product c) b t -> (s && Mod s a b) ~> t Source Github #

(HasBinaryProducts k, Ob s) => LensFl (Rep (Product s) :: k -> k -> Type) (Corep (Product s) :: k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic.Lens

Methods

putP :: forall (s0 :: k) (a :: k) (b :: k) (t :: k). HasBinaryProducts k => Rep (Product s) s0 a -> Corep (Product s) b t -> (s0 && b) ~> t Source Github #

(HasBinaryProducts k, Ob s) => SetterFl (Rep (Product s) :: k -> k -> Type) (Corep (Product s) :: k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic.Setter

Methods

overP :: forall (s0 :: k) (a :: k) (b :: k) (t :: k). Rep (Product s) s0 a -> Corep (Product s) b t -> (a ~> b) -> s0 ~> t Source Github #

(HasBinaryProducts k, Ob s) => TravFl (Rep (Product s) :: k -> k -> Type) (Corep (Product s) :: k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic.Traversal

Methods

travP :: forall r (s0 :: k) (a :: k) (b :: k) (t :: k). (StrongDistributiveProfunctor r, Strong (ProdAction :: k -> (PROD k, k) -> Type) r) => Rep (Product s) s0 a -> Corep (Product s) b t -> r a b -> r s0 t Source Github #

type (Product a :: k +-> k) @ (b :: k) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (Product a :: k +-> k) @ (b :: k) = a && b

type HasProducts k = (HasTerminalObject k, HasBinaryProducts k) Source Github #

leftUnitorProd :: forall {k} (a :: k). (HasProducts k, Ob a) => ((TerminalObject :: k) && a) ~> a Source Github #

leftUnitorProdInv :: forall {k} (a :: k). (HasProducts k, Ob a) => a ~> ((TerminalObject :: k) && a) Source Github #

rightUnitorProd :: forall {k} (a :: k). (HasProducts k, Ob a) => (a && (TerminalObject :: k)) ~> a Source Github #

rightUnitorProdInv :: forall {k} (a :: k). (HasProducts k, Ob a) => a ~> (a && (TerminalObject :: k)) Source Github #

associatorProd :: forall {k} (a :: k) (b :: k) (c :: k). (HasBinaryProducts k, Ob a, Ob b, Ob c) => ((a && b) && c) ~> (a && (b && c)) Source Github #

associatorProdInv :: forall {k} (a :: k) (b :: k) (c :: k). (HasBinaryProducts k, Ob a, Ob b, Ob c) => (a && (b && c)) ~> ((a && b) && c) Source Github #

swapProd :: forall {k} (a :: k) (b :: k). (HasBinaryProducts k, Ob a, Ob b) => (a && b) ~> (b && a) Source Github #

data PROD k Source Github #

Constructors

PR k 

Instances

Instances details
CategoryOf k => Functor ('PR :: k -> PROD k) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

map :: forall (a :: k) (b :: k). (a ~> b) -> 'PR a ~> 'PR b Source Github #

HasProducts k => Monoidal (PROD k) Source Github #

Products as monoidal structure.

Instance details

Defined in Proarrow.Limit.BinaryProduct

Associated Types

type Unit 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type Unit = TerminalObject :: PROD k

Methods

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

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

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

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

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

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

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

HasProducts k => SymMonoidal (PROD k) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

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

(CategoryOf j, CategoryOf k, HasTerminalObject (SUBCAT ob), HasBinaryProducts (SUBCAT ob), forall (p :: j +-> k) (q :: j +-> k). (ob p, ob q) => IsObProd ob p q, forall (p :: j +-> k) (q :: j +-> k). (ob p, ob q) => IsObExp ob p q) => Closed (PROD (SUBCAT ob)) Source Github #

And then the subcategory is closed, with the ambient exponential and nothing of its own, just as its products are the ambient ones. FINITARY j k is one instance, SHEAVES another. For the first, a hom-set of natural transformations is finitary. For the second, an internal hom into a sheaf is a sheaf.

Instance details

Defined in Proarrow.Profunctor.Instance.Exponential

Methods

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

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

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

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

(CategoryOf j, CategoryOf k) => Closed (PROD (j +-> k)) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Exponential

Methods

withObExp :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r Source Github #

curry :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) (c :: PROD (j +-> k)). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) Source Github #

apply :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b Source Github #

(^^^) :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) (x :: PROD (j +-> k)) (y :: PROD (j +-> k)). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Github #

CategoryOf k1 => Closed (PROD (k1 -> Type)) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Nat

Methods

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

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

apply :: forall (a :: PROD (k1 -> Type)) (b :: PROD (k1 -> Type)). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b Source Github #

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

HasProducts k => CopyDiscard (PROD k) Source Github #

A category with products, viewed through PROD as a monoidal category, is cartesian.

Instance details

Defined in Proarrow.Category.Monoidal.Cartesian

Methods

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

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

BiCCC k => Distributive (PROD k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Cartesian

Methods

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

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

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

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

(StableSite t k, HasFiniteCovers t k, FiniteCat j, FiniteCat k) => ElementaryTopos (PROD (SHEAVES t j k)) Source Github #

The topos of sheaves. Finite limits and colimits, cartesian closed, a subobject classifier, and image factorization, all defined above and none of them postulated.

The exponential needs StableSite. A full subcategory is closed when it contains its internal homs, and an internal hom is a sheaf by gluing pointwise into the codomain, which needs the cover pulled back along the argument.

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Sheaf

(FiniteCat j, FiniteCat k) => ElementaryTopos (PROD (FINITARY j k)) Source Github #

Finitary profunctors between finite categories form an elementary topos: finite limits and colimits, cartesian closed, a subobject classifier, and image factorization.

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

HasEpiMonoFactorization k => HasEpiMonoFactorization (PROD k) Source Github #

Image factorization is unchanged by making the tensor the product.

Instance details

Defined in Proarrow.Category.Topos

Methods

factorize :: forall (a :: PROD k) (b :: PROD k). (a ~> b) -> (Hom (PROD k) :.: Hom (PROD k)) a b Source Github #

(StableSite t k, HasFiniteCovers t k, FiniteCat j, FiniteCat k) => HasSubobjectClassifier (PROD (SHEAVES t j k)) Source Github #

The classifier is the closed sieves, and an arrow is classified by FINITARY's graph sieve, closed. For an arrow of sheaves that sieve is already closed, since a sheaf is separated. The closedSieve call guards against a Sheaf instance that was asserted instead of decided, which would otherwise fail later in familyIndex as "not a closed sieve".

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Sheaf

Associated Types

type Omega 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Sheaf

type Omega = 'PR ('SUB (ClosedSieve t :: k -> j -> Type) :: SUBCAT ((Finitary :: (j +-> k) -> Constraint) :&&: (Sheaf t :: (j +-> k) -> Constraint)))

Methods

true :: (TerminalObject :: PROD (SHEAVES t j k)) ~> (Omega :: PROD (SHEAVES t j k)) Source Github #

classifyGraph :: forall (a :: PROD (SHEAVES t j k)) (b :: PROD (SHEAVES t j k)). (a ~> b) -> (a && b) ~> (Omega :: PROD (SHEAVES t j k)) Source Github #

(FiniteCat j, FiniteCat k) => HasSubobjectClassifier (PROD (FINITARY j k)) Source Github #

The subobject classifier is the profunctor of sieves, and an arrow classifies its graph.

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Associated Types

type Omega 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

type Omega = 'PR ('SUB (Sieve :: k -> j -> Type) :: SUBCAT (Finitary :: (j +-> k) -> Constraint))

Methods

true :: (TerminalObject :: PROD (FINITARY j k)) ~> (Omega :: PROD (FINITARY j k)) Source Github #

classifyGraph :: forall (a :: PROD (FINITARY j k)) (b :: PROD (FINITARY j k)). (a ~> b) -> (a && b) ~> (Omega :: PROD (FINITARY j k)) Source Github #

HasBinaryCoproducts k => HasBinaryCoproducts (PROD k) Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

Methods

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

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

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

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

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

HasCoequalizers k => HasCoequalizers (PROD k) Source Github #

Coequalizers are unchanged by making the tensor the product.

Instance details

Defined in Proarrow.Colimit.Coequalizer

Methods

coequalize :: forall (a :: PROD k) (b :: PROD k) r. (a ~> b) -> (a ~> b) -> (forall (c :: PROD k). (b ~> c) -> r) -> r Source Github #

factorCoequalizer :: forall (c :: PROD k) (x :: PROD k) (c' :: PROD k). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #

HasInitialObject k => HasInitialObject (PROD k) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Associated Types

type InitialObject 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type InitialObject = 'PR (InitialObject :: k)

Methods

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

HasPushouts k => HasPushouts (PROD k) Source Github #

Pushouts are unchanged by making the tensor the product.

Instance details

Defined in Proarrow.Colimit.Pushout

Methods

pushout :: forall (o :: PROD k) (a :: PROD k) (b :: PROD k) r. (o ~> a) -> (o ~> b) -> (forall (p :: PROD k). (a ~> p) -> (b ~> p) -> r) -> r Source Github #

factorPushout :: forall (a :: PROD k) (b :: PROD k) (p :: PROD k) (q :: PROD k). (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q Source Github #

CategoryOf k => CategoryOf (PROD k) Source Github #

The same category as the category of k, but with products as the tensor.

Instance details

Defined in Proarrow.Limit.BinaryProduct

Associated Types

type (~>) 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (~>) = Prod ((~>) :: CAT k)
HasBinaryProducts k => HasBinaryProducts (PROD k) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

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

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

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

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

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

HasEqualizers k => HasEqualizers (PROD k) Source Github #

Equalizers are unchanged by making the tensor the product.

Instance details

Defined in Proarrow.Limit.Equalizer

Methods

equalize :: forall (a :: PROD k) (b :: PROD k) r. (a ~> b) -> (a ~> b) -> (forall (e :: PROD k). (e ~> a) -> r) -> r Source Github #

factorEqualizer :: forall (e :: PROD k) (x :: PROD k) (e' :: PROD k). (e ~> x) -> (e' ~> x) -> e' ~> e Source Github #

HasPullbacks k => HasPullbacks (PROD k) Source Github #

Pullbacks are unchanged by making the tensor the product.

Instance details

Defined in Proarrow.Limit.Pullback

Methods

pullback :: forall (o :: PROD k) (a :: PROD k) (b :: PROD k) r. (a ~> o) -> (b ~> o) -> (forall (p :: PROD k). (p ~> a) -> (p ~> b) -> r) -> r Source Github #

factorPullback :: forall (a :: PROD k) (b :: PROD k) (p :: PROD k) (q :: PROD k). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #

HasTerminalObject k => HasTerminalObject (PROD k) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Associated Types

type TerminalObject 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type TerminalObject = 'PR (TerminalObject :: k)

Methods

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

HasProducts k => MonoidalAction (ProdAction :: k -> (PROD k, k) -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Action

Methods

unitor :: forall (x :: k). Ob x => Act (ProdAction :: k -> (PROD k, k) -> Type) (Unit :: PROD k) x ~> x Source Github #

unitorInv :: forall (x :: k). Ob x => x ~> Act (ProdAction :: k -> (PROD k, k) -> Type) (Unit :: PROD k) x Source Github #

multiplicator :: forall (a :: PROD k) (b :: PROD k) (x :: k). (Ob a, Ob b, Ob x) => Act (ProdAction :: k -> (PROD k, k) -> Type) (a ** b) x ~> Act (ProdAction :: k -> (PROD k, k) -> Type) a (Act (ProdAction :: k -> (PROD k, k) -> Type) b x) Source Github #

multiplicatorInv :: forall (a :: PROD k) (b :: PROD k) (x :: k). (Ob a, Ob b, Ob x) => Act (ProdAction :: k -> (PROD k, k) -> Type) a (Act (ProdAction :: k -> (PROD k, k) -> Type) b x) ~> Act (ProdAction :: k -> (PROD k, k) -> Type) (a ** b) x Source Github #

Cartesian k => Costrong (ProdAction :: k -> (PROD k, k) -> Type) (Fold :: k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Fold

Methods

coact :: forall (a :: PROD k) (x :: k) (y :: k). (Ob a, Ob x, Ob y) => Fold (Act (ProdAction :: k -> (PROD k, k) -> Type) a x) (Act (ProdAction :: k -> (PROD k, k) -> Type) a y) -> Fold x y Source Github #

Functor f => Strong (ProdAction :: Type -> (PROD Type, Type) -> Type) (Star (Prelude f) :: Type -> Type -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Star

Methods

act :: forall (a :: PROD Type) x y. Ob a => Star (Prelude f) x y -> Star (Prelude f) (Act (ProdAction :: Type -> (PROD Type, Type) -> Type) a x) (Act (ProdAction :: Type -> (PROD Type, Type) -> Type) a y) Source Github #

(HasProducts k, Ob a, Ob b, Flavor w, forall (s :: k). Ob s => w (Rep (Product s)) (Corep (Product s))) => Strong (ProdAction :: k -> (PROD k, k) -> Type) (ExOptic w a b :: k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic.MonoidalTraversal

Methods

act :: forall (a0 :: PROD k) (x :: k) (y :: k). Ob a0 => ExOptic w a b x y -> ExOptic w a b (Act (ProdAction :: k -> (PROD k, k) -> Type) a0 x) (Act (ProdAction :: k -> (PROD k, k) -> Type) a0 y) Source Github #

Ord k => Applicative (FromProd (FromPointed (Map k)) :: PROD POINTED -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.PointedHask

Methods

pure :: forall (a :: PROD POINTED). ((Unit :: PROD POINTED) ~> a) -> (Unit :: Type) ~> FromProd (FromPointed (Map k)) a Source Github #

liftA2 :: forall (a :: PROD POINTED) (b :: PROD POINTED) (c :: PROD POINTED). (Ob a, Ob b) => ((a ** b) ~> c) -> (FromProd (FromPointed (Map k)) a ** FromProd (FromPointed (Map k)) b) ~> FromProd (FromPointed (Map k)) c Source Github #

Applicative (FromProd (FromPointed [])) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.PointedHask

Methods

pure :: forall (a :: PROD POINTED). ((Unit :: PROD POINTED) ~> a) -> (Unit :: Type) ~> FromProd (FromPointed []) a Source Github #

liftA2 :: forall (a :: PROD POINTED) (b :: PROD POINTED) (c :: PROD POINTED). (Ob a, Ob b) => ((a ** b) ~> c) -> (FromProd (FromPointed []) a ** FromProd (FromPointed []) b) ~> FromProd (FromPointed []) c Source Github #

Functor f => Functor (FromProd f :: PROD k -> Type) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

map :: forall (a :: PROD k) (b :: PROD k). (a ~> b) -> FromProd f a ~> FromProd f b Source Github #

HasProducts k => MonoidalProfunctor (Cone :: PROD k -> LIST k -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Cone

Methods

one :: Cone (Unit :: PROD k) (Unit :: LIST k) Source Github #

(**) :: forall (x1 :: PROD k) (x2 :: LIST k) (y1 :: PROD k) (y2 :: LIST k). Cone x1 x2 -> Cone y1 y2 -> Cone (x1 ** y1) (x2 ** y2) Source Github #

CategoryOf k => Profunctor (Cone :: PROD k -> LIST k -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Cone

Methods

dimap :: forall (c :: PROD k) (a :: PROD k) (b :: LIST k) (d :: LIST k). (c ~> a) -> (b ~> d) -> Cone a b -> Cone c d Source Github #

lmap :: forall (c :: PROD k) (a :: PROD k) (b :: LIST k). (c ~> a) -> Cone a b -> Cone c b Source Github #

rmap :: forall (b :: LIST k) (d :: LIST k) (a :: PROD k). (b ~> d) -> Cone a b -> Cone a d Source Github #

(\\) :: forall (a :: PROD k) (b :: LIST k) r. ((Ob a, Ob b) => r) -> Cone a b -> r Source Github #

(CategoryOf j, CategoryOf k) => EnrichedProfunctor (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) :: PROD (j +-> k) -> PROD (j +-> k) -> Type) Source Github #

The category of profunctors is enriched in itself: the hom-object is the internal hom p :~>: q, an element of it is a natural transformation, and composition is the internal one. Cartesian closed, hence the PROD wrapper (j +-> k's own tensor is Day convolution).

This self-enrichment is written the generic way, from HomSelf and friends. Those apply to any Closed SymMonoidal kind that has no enrichment instance of its own covering its hom-profunctor.

Instance details

Defined in Proarrow.Category.Enriched

Methods

withProObj :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) r. (Ob a, Ob b) => (Ob (ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b) => r) -> r Source Github #

underlying :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)). Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) a b -> (Unit :: PROD (j +-> k)) ~> ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b Source Github #

enriched :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)). (Ob a, Ob b) => ((Unit :: PROD (j +-> k)) ~> ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b) -> Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) a b Source Github #

rmap :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) (c :: PROD (j +-> k)). (Ob a, Ob b, Ob c) => (HomObj (PROD (j +-> k)) b c ** ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b) ~> ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a c Source Github #

lmap :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) (c :: PROD (j +-> k)). (Ob a, Ob b, Ob c) => (HomObj (PROD (j +-> k)) c a ** ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b) ~> ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) c b Source Github #

(HasProducts k, cat ~ Hom k) => MonoidalProfunctor (Prod cat :: PROD k -> PROD k -> Type) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

one :: Prod cat (Unit :: PROD k) (Unit :: PROD k) Source Github #

(**) :: forall (x1 :: PROD k) (x2 :: PROD k) (y1 :: PROD k) (y2 :: PROD k). Prod cat x1 x2 -> Prod cat y1 y2 -> Prod cat (x1 ** y1) (x2 ** y2) Source Github #

Profunctor p => Profunctor (Prod p :: PROD k -> PROD j -> Type) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

dimap :: forall (c :: PROD k) (a :: PROD k) (b :: PROD j) (d :: PROD j). (c ~> a) -> (b ~> d) -> Prod p a b -> Prod p c d Source Github #

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

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

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

Representable p => Representable (Prod p :: PROD k -> PROD j -> Type) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

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

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

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

repUniv :: forall (a :: PROD j). Ob a => Prod p (Prod p % a) a Source Github #

(HasProducts k, Ob a) => CocommutativeComonoid ('PR a :: PROD k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Cartesian

(HasProducts k, Ob a) => Comonoid ('PR a :: PROD k) Source Github #

In a category with products every object is a comonoid via the diagonal and the terminal map. With this comonoid structure PROD is CopyDiscard and Cartesian.

Instance details

Defined in Proarrow.Category.Monoidal.Cartesian

Methods

counit :: 'PR a ~> (Unit :: PROD k) Source Github #

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

(CategoryOf j, CategoryOf k) => Strong (ProdAction :: (j +-> k) -> (PROD (j +-> k), j +-> k) -> Type) (Prof :: (j +-> k) -> (j +-> k) -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Strength

Methods

act :: forall (a :: PROD (j +-> k)) (x :: j +-> k) (y :: j +-> k). Ob a => Prof x y -> Prof (Act (ProdAction :: (j +-> k) -> (PROD (j +-> k), j +-> k) -> Type) a x) (Act (ProdAction :: (j +-> k) -> (PROD (j +-> k), j +-> k) -> Type) a y) Source Github #

Promonad p => Promonad (Prod p :: PROD j -> PROD j -> Type) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

id :: forall (a :: PROD j). Ob a => Prod p a a Source Github #

(.) :: forall (b :: PROD j) (c :: PROD j) (a :: PROD j). Prod p b c -> Prod p a b -> Prod p a c Source Github #

HasProducts k => FunctorForRep (ProdAction' :: (PROD k, k) +-> k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Action

Methods

fmap :: forall (a :: (PROD k, k)) (b :: (PROD k, k)). (a ~> b) -> ((ProdAction' :: (PROD k, k) +-> k) @ a) ~> ((ProdAction' :: (PROD k, k) +-> k) @ b) Source Github #

type Unit Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type Unit = TerminalObject :: PROD k
type Omega Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Sheaf

type Omega = 'PR ('SUB (ClosedSieve t :: k -> j -> Type) :: SUBCAT ((Finitary :: (j +-> k) -> Constraint) :&&: (Sheaf t :: (j +-> k) -> Constraint)))
type Omega Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

type Omega = 'PR ('SUB (Sieve :: k -> j -> Type) :: SUBCAT (Finitary :: (j +-> k) -> Constraint))
type InitialObject Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type InitialObject = 'PR (InitialObject :: k)
type (~>) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (~>) = Prod ((~>) :: CAT k)
type TerminalObject Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type TerminalObject = 'PR (TerminalObject :: k)
type Ob (a :: PROD k) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type Ob (a :: PROD k) = WrappedOb ('PR :: k -> PROD k) a
type (a :: PROD k) ** (b :: PROD k) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (a :: PROD k) ** (b :: PROD k) = a && b
type (p :: PROD (SUBCAT ob)) ~~> (q :: PROD (SUBCAT ob)) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Exponential

type (p :: PROD (SUBCAT ob)) ~~> (q :: PROD (SUBCAT ob)) = 'PR ('SUB (UN ('SUB :: (k -> j -> Type) -> SUBCAT ob) (UN ('PR :: SUBCAT ob -> PROD (SUBCAT ob)) p) :~>: UN ('SUB :: (k -> j -> Type) -> SUBCAT ob) (UN ('PR :: SUBCAT ob -> PROD (SUBCAT ob)) q)) :: SUBCAT ob)
type (p :: PROD (k -> j -> Type)) ~~> (q :: PROD (k -> j -> Type)) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Exponential

type (p :: PROD (k -> j -> Type)) ~~> (q :: PROD (k -> j -> Type)) = 'PR (UN ('PR :: (k -> j -> Type) -> PROD (k -> j -> Type)) p :~>: UN ('PR :: (k -> j -> Type) -> PROD (k -> j -> Type)) q)
type (f :: PROD (k1 -> Type)) ~~> (g :: PROD (k1 -> Type)) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Nat

type (f :: PROD (k1 -> Type)) ~~> (g :: PROD (k1 -> Type)) = 'PR (UN ('PR :: (k1 -> Type) -> PROD (k1 -> Type)) f :~>: UN ('PR :: (k1 -> Type) -> PROD (k1 -> Type)) g)
type (a :: PROD k) && (b :: PROD k) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (a :: PROD k) && (b :: PROD k) = 'PR (UN ('PR :: k -> PROD k) a && UN ('PR :: k -> PROD k) b)
type ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) :: PROD (j +-> k) -> PROD (j +-> k) -> Type) (p :: PROD (j +-> k)) (q :: PROD (j +-> k)) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched

type ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) :: PROD (j +-> k) -> PROD (j +-> k) -> Type) (p :: PROD (j +-> k)) (q :: PROD (j +-> k)) = HomSelf p q
type (Prod p :: PROD k -> PROD j -> Type) % ('PR a :: PROD j) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (Prod p :: PROD k -> PROD j -> Type) % ('PR a :: PROD j) = 'PR (p % a)
type ('PR a :: PROD k) || ('PR b :: PROD k) Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

type ('PR a :: PROD k) || ('PR b :: PROD k) = 'PR (a || b)
type (ProdAction' :: (PROD k, k) +-> k) @ ('('PR a, b) :: (PROD k, k)) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Action

type (ProdAction' :: (PROD k, k) +-> k) @ ('('PR a, b) :: (PROD k, k)) = a && b

data Prod (p :: j +-> k) (a :: PROD k) (b :: PROD j) where Source Github #

Lifts a profunctor to the PROD-wrapped kinds, where the monoidal structure is the categorical product.

Constructors

Prod 

Fields

  • :: forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j). { unProd :: p a1 b1
     
  •    } -> Prod p ('PR a1) ('PR b1)
     

Instances

Instances details
(CategoryOf j, CategoryOf k) => EnrichedProfunctor (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) :: PROD (j +-> k) -> PROD (j +-> k) -> Type) Source Github #

The category of profunctors is enriched in itself: the hom-object is the internal hom p :~>: q, an element of it is a natural transformation, and composition is the internal one. Cartesian closed, hence the PROD wrapper (j +-> k's own tensor is Day convolution).

This self-enrichment is written the generic way, from HomSelf and friends. Those apply to any Closed SymMonoidal kind that has no enrichment instance of its own covering its hom-profunctor.

Instance details

Defined in Proarrow.Category.Enriched

Methods

withProObj :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) r. (Ob a, Ob b) => (Ob (ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b) => r) -> r Source Github #

underlying :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)). Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) a b -> (Unit :: PROD (j +-> k)) ~> ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b Source Github #

enriched :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)). (Ob a, Ob b) => ((Unit :: PROD (j +-> k)) ~> ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b) -> Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) a b Source Github #

rmap :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) (c :: PROD (j +-> k)). (Ob a, Ob b, Ob c) => (HomObj (PROD (j +-> k)) b c ** ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b) ~> ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a c Source Github #

lmap :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) (c :: PROD (j +-> k)). (Ob a, Ob b, Ob c) => (HomObj (PROD (j +-> k)) c a ** ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b) ~> ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) c b Source Github #

(HasProducts k, cat ~ Hom k) => MonoidalProfunctor (Prod cat :: PROD k -> PROD k -> Type) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

one :: Prod cat (Unit :: PROD k) (Unit :: PROD k) Source Github #

(**) :: forall (x1 :: PROD k) (x2 :: PROD k) (y1 :: PROD k) (y2 :: PROD k). Prod cat x1 x2 -> Prod cat y1 y2 -> Prod cat (x1 ** y1) (x2 ** y2) Source Github #

Profunctor p => Profunctor (Prod p :: PROD k -> PROD j -> Type) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

dimap :: forall (c :: PROD k) (a :: PROD k) (b :: PROD j) (d :: PROD j). (c ~> a) -> (b ~> d) -> Prod p a b -> Prod p c d Source Github #

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

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

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

Representable p => Representable (Prod p :: PROD k -> PROD j -> Type) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

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

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

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

repUniv :: forall (a :: PROD j). Ob a => Prod p (Prod p % a) a Source Github #

Promonad p => Promonad (Prod p :: PROD j -> PROD j -> Type) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

id :: forall (a :: PROD j). Ob a => Prod p a a Source Github #

(.) :: forall (b :: PROD j) (c :: PROD j) (a :: PROD j). Prod p b c -> Prod p a b -> Prod p a c Source Github #

type ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) :: PROD (j +-> k) -> PROD (j +-> k) -> Type) (p :: PROD (j +-> k)) (q :: PROD (j +-> k)) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched

type ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) :: PROD (j +-> k) -> PROD (j +-> k) -> Type) (p :: PROD (j +-> k)) (q :: PROD (j +-> k)) = HomSelf p q
type (Prod p :: PROD k -> PROD j -> Type) % ('PR a :: PROD j) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (Prod p :: PROD k -> PROD j -> Type) % ('PR a :: PROD j) = 'PR (p % a)

data FromProd (f :: k -> Type) (a :: PROD k) where Source Github #

Constructors

FromProd 

Fields

Instances

Instances details
Ord k => Applicative (FromProd (FromPointed (Map k)) :: PROD POINTED -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.PointedHask

Methods

pure :: forall (a :: PROD POINTED). ((Unit :: PROD POINTED) ~> a) -> (Unit :: Type) ~> FromProd (FromPointed (Map k)) a Source Github #

liftA2 :: forall (a :: PROD POINTED) (b :: PROD POINTED) (c :: PROD POINTED). (Ob a, Ob b) => ((a ** b) ~> c) -> (FromProd (FromPointed (Map k)) a ** FromProd (FromPointed (Map k)) b) ~> FromProd (FromPointed (Map k)) c Source Github #

Applicative (FromProd (FromPointed [])) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.PointedHask

Methods

pure :: forall (a :: PROD POINTED). ((Unit :: PROD POINTED) ~> a) -> (Unit :: Type) ~> FromProd (FromPointed []) a Source Github #

liftA2 :: forall (a :: PROD POINTED) (b :: PROD POINTED) (c :: PROD POINTED). (Ob a, Ob b) => ((a ** b) ~> c) -> (FromProd (FromPointed []) a ** FromProd (FromPointed []) b) ~> FromProd (FromPointed []) c Source Github #

Functor f => Functor (FromProd f :: PROD k -> Type) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

map :: forall (a :: PROD k) (b :: PROD k). (a ~> b) -> FromProd f a ~> FromProd f b Source Github #

data family (a :: k) *! (b :: k) :: k Source Github #

Instances

Instances details
(IsFreeOb a, IsFreeOb b, Elem HasBinaryProducts cs) => IsFreeOb (a *! b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (a *! b)) => r) -> r Source Github #

type Lower (f :: k +-> k') (a *! b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type Lower (f :: k +-> k') (a *! b :: FREE cs p) = Lower f a && Lower f b

Orphan instances

Monoidal BOOL Source Github #

Products as monoidal structure.

Instance details

Associated Types

type Unit 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type Unit = TerminalObject :: BOOL
type (a :: BOOL) ** (b :: BOOL) 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (a :: BOOL) ** (b :: BOOL) = a && b

Methods

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

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

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

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

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

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

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

Monoidal Type Source Github #

Products as monoidal structure.

Instance details

Associated Types

type Unit 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type Unit = TerminalObject :: Type
type (a :: Type) ** (b :: Type) 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (a :: Type) ** (b :: Type) = a && b

Methods

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

leftUnitor :: Ob a => ((Unit :: Type) ** a) ~> a Source Github #

leftUnitorInv :: Ob a => a ~> ((Unit :: Type) ** a) Source Github #

rightUnitor :: Ob a => (a ** (Unit :: Type)) ~> a Source Github #

rightUnitorInv :: Ob a => a ~> (a ** (Unit :: Type)) Source Github #

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

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

SymMonoidal BOOL Source Github # 
Instance details

Methods

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

SymMonoidal Type Source Github # 
Instance details

Methods

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

MonoidalProfunctor Booleans Source Github # 
Instance details

Methods

one :: Booleans (Unit :: BOOL) (Unit :: BOOL) Source Github #

(**) :: forall (x1 :: BOOL) (x2 :: BOOL) (y1 :: BOOL) (y2 :: BOOL). Booleans x1 x2 -> Booleans y1 y2 -> Booleans (x1 ** y1) (x2 ** y2) Source Github #

MonoidalProfunctor (->) Source Github # 
Instance details

Methods

one :: (Unit :: Type) -> (Unit :: Type) Source Github #

(**) :: (x1 -> x2) -> (y1 -> y2) -> (x1 ** y1) -> (x2 ** y2) Source Github #

(DecidableProfunctor p, DecidableProfunctor q) => DecidableProfunctor (p :*: q :: k -> j -> Type) Source Github # 
Instance details

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (p :*: q) a b (Holds (p :*: q) a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. (p :*: q) a b -> ((Holds (p :*: q) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(HasBinaryProducts k, Representable p, Representable q) => Representable (p :*: q :: k -> j -> Type) Source Github # 
Instance details

Methods

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

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

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

repUniv :: forall (a :: j). Ob a => (p :*: q) ((p :*: q) % a) a Source Github #

HasBinaryProducts k => Representable (Corep (Diag :: k +-> (k, k)) :: k -> (k, k) -> Type) Source Github #

The right adjoint to the diagonal functor.

Instance details

Methods

index :: forall (a :: k) (b :: (k, k)). Corep (Diag :: k +-> (k, k)) a b -> a ~> (Corep (Diag :: k +-> (k, k)) % b) Source Github #

tabulate :: forall (b :: (k, k)) (a :: k). Ob b => (a ~> (Corep (Diag :: k +-> (k, k)) % b)) -> Corep (Diag :: k +-> (k, k)) a b Source Github #

repMap :: forall (a :: (k, k)) (b :: (k, k)). (a ~> b) -> (Corep (Diag :: k +-> (k, k)) % a) ~> (Corep (Diag :: k +-> (k, k)) % b) Source Github #

repUniv :: forall (a :: (k, k)). Ob a => Corep (Diag :: k +-> (k, k)) (Corep (Diag :: k +-> (k, k)) % a) a Source Github #

(DecidableProfunctor p, DecidableProfunctor q) => DecidableProfunctor (p :**: q :: (k1, k2) -> (j1, j2) -> Type) Source Github #

A product holds when both components do: the type-level && is BOOL's categorical product.

Instance details

Methods

decide :: forall (a :: (k1, k2)) (b :: (j1, j2)). (Ob a, Ob b) => Decision (p :**: q) a b (Holds (p :**: q) a b) Source Github #

toHolds :: forall (a :: (k1, k2)) (b :: (j1, j2)) r. (p :**: q) a b -> ((Holds (p :**: q) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #