Safe Haskell | None |
---|---|
Language | Haskell2010 |
Documentation
class CategoryOf k => HasBinaryProducts k where Source Comments #
fst :: forall (a :: k) (b :: k). (Ob a, Ob b) => (a && b) ~> a Source Comments #
fst' :: forall (a :: k) (a' :: k) (b :: k). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments #
snd :: forall (a :: k) (b :: k). (Ob a, Ob b) => (a && b) ~> b Source Comments #
snd' :: forall (a :: k) (b :: k) (b' :: k). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments #
(&&&) :: forall (a :: k) (x :: k) (y :: k). (a ~> x) -> (a ~> y) -> a ~> (x && y) infixl 5 Source Comments #
(***) :: forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) infixl 5 Source Comments #
Instances
HasBinaryProducts BOOL Source Comments # | |||||||||||||||||
Defined in Proarrow.Category.Instance.Bool
fst :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: BOOL) (a' :: BOOL) (b :: BOOL). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: BOOL) (b :: BOOL) (b' :: BOOL). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: BOOL) (x :: BOOL) (y :: BOOL). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: BOOL) (b :: BOOL) (x :: BOOL) (y :: BOOL). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
HasBinaryProducts KIND Source Comments # | |||||||||||||||||
Defined in Proarrow.Category.Instance.Cat fst :: forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: KIND) (a' :: KIND) (b :: KIND). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: KIND) (b :: KIND) (b' :: KIND). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: KIND) (x :: KIND) (y :: KIND). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: KIND) (b :: KIND) (x :: KIND) (y :: KIND). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
HasBinaryProducts CONSTRAINT Source Comments # | |||||||||||||||||
Defined in Proarrow.Category.Instance.Constraint
fst :: forall (a :: CONSTRAINT) (b :: CONSTRAINT). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: CONSTRAINT) (a' :: CONSTRAINT) (b :: CONSTRAINT). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: CONSTRAINT) (b :: CONSTRAINT). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) (b' :: CONSTRAINT). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: CONSTRAINT) (x :: CONSTRAINT) (y :: CONSTRAINT). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) (x :: CONSTRAINT) (y :: CONSTRAINT). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
HasBinaryProducts LINEAR Source Comments # | |||||||||||||||||
Defined in Proarrow.Category.Instance.Linear fst :: forall (a :: LINEAR) (b :: LINEAR). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: LINEAR) (a' :: LINEAR) (b :: LINEAR). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: LINEAR) (b :: LINEAR). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: LINEAR) (b :: LINEAR) (b' :: LINEAR). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: LINEAR) (x :: LINEAR) (y :: LINEAR). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: LINEAR) (b :: LINEAR) (x :: LINEAR) (y :: LINEAR). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
HasBinaryProducts POINTED Source Comments # | |||||||||||||||||
Defined in Proarrow.Category.Instance.PointedHask fst :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: POINTED) (a' :: POINTED) (b :: POINTED). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: POINTED) (b :: POINTED) (b' :: POINTED). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: POINTED) (x :: POINTED) (y :: POINTED). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: POINTED) (b :: POINTED) (x :: POINTED) (y :: POINTED). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
HasBinaryProducts () Source Comments # | |||||||||||||||||
Defined in Proarrow.Object.BinaryProduct
fst :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: ()) (a' :: ()) (b :: ()). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: ()) (b :: ()) (b' :: ()). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: ()) (x :: ()) (y :: ()). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: ()) (b :: ()) (x :: ()) (y :: ()). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
HasBinaryProducts Type Source Comments # | |||||||||||||||||
Defined in Proarrow.Object.BinaryProduct
fst :: (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall a b x y. (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
HasBinaryProducts (FIN ('S n)) => HasBinaryProducts (FIN ('S ('S n))) Source Comments # | Minimum | ||||||||||||||||
Defined in Proarrow.Category.Instance.Fin fst :: forall (a :: FIN ('S ('S n))) (b :: FIN ('S ('S n))). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: FIN ('S ('S n))) (a' :: FIN ('S ('S n))) (b :: FIN ('S ('S n))). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: FIN ('S ('S n))) (b :: FIN ('S ('S n))). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: FIN ('S ('S n))) (b :: FIN ('S ('S n))) (b' :: FIN ('S ('S n))). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: FIN ('S ('S n))) (x :: FIN ('S ('S n))) (y :: FIN ('S ('S n))). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: FIN ('S ('S n))) (b :: FIN ('S ('S n))) (x :: FIN ('S ('S n))) (y :: FIN ('S ('S n))). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
HasBinaryProducts (FIN ('S 'Z)) Source Comments # | |||||||||||||||||
Defined in Proarrow.Category.Instance.Fin fst :: forall (a :: FIN ('S 'Z)) (b :: FIN ('S 'Z)). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: FIN ('S 'Z)) (a' :: FIN ('S 'Z)) (b :: FIN ('S 'Z)). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: FIN ('S 'Z)) (b :: FIN ('S 'Z)). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: FIN ('S 'Z)) (b :: FIN ('S 'Z)) (b' :: FIN ('S 'Z)). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: FIN ('S 'Z)) (x :: FIN ('S 'Z)) (y :: FIN ('S 'Z)). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: FIN ('S 'Z)) (b :: FIN ('S 'Z)) (x :: FIN ('S 'Z)) (y :: FIN ('S 'Z)). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
HasBinaryProducts (FIN 'Z) Source Comments # | |||||||||||||||||
Defined in Proarrow.Category.Instance.Fin fst :: forall (a :: FIN 'Z) (b :: FIN 'Z). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: FIN 'Z) (a' :: FIN 'Z) (b :: FIN 'Z). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: FIN 'Z) (b :: FIN 'Z). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: FIN 'Z) (b :: FIN 'Z) (b' :: FIN 'Z). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: FIN 'Z) (x :: FIN 'Z) (y :: FIN 'Z). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: FIN 'Z) (b :: FIN 'Z) (x :: FIN 'Z) (y :: FIN 'Z). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
Num a => HasBinaryProducts (MatK a) Source Comments # | |||||||||||||||||
Defined in Proarrow.Category.Instance.Mat fst :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => (a0 && b) ~> a0 Source Comments # fst' :: forall (a0 :: MatK a) (a' :: MatK a) (b :: MatK a). (a0 ~> a') -> Obj b -> (a0 && b) ~> a' Source Comments # snd :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => (a0 && b) ~> b Source Comments # snd' :: forall (a0 :: MatK a) (b :: MatK a) (b' :: MatK a). Obj a0 -> (b ~> b') -> (a0 && b) ~> b' Source Comments # (&&&) :: forall (a0 :: MatK a) (x :: MatK a) (y :: MatK a). (a0 ~> x) -> (a0 ~> y) -> a0 ~> (x && y) Source Comments # (***) :: forall (a0 :: MatK a) (b :: MatK a) (x :: MatK a) (y :: MatK a). (a0 ~> x) -> (b ~> y) -> (a0 && b) ~> (x && y) Source Comments # | |||||||||||||||||
HasBinaryProducts (POCATK Constraint) Source Comments # | |||||||||||||||||
Defined in Proarrow.Category.Instance.PreorderAsCategory
fst :: forall (a :: POCATK Constraint) (b :: POCATK Constraint). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: POCATK Constraint) (a' :: POCATK Constraint) (b :: POCATK Constraint). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: POCATK Constraint) (b :: POCATK Constraint). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: POCATK Constraint) (b :: POCATK Constraint) (b' :: POCATK Constraint). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: POCATK Constraint) (x :: POCATK Constraint) (y :: POCATK Constraint). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: POCATK Constraint) (b :: POCATK Constraint) (x :: POCATK Constraint) (y :: POCATK Constraint). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
HasBinaryCoproducts k => HasBinaryProducts (OPPOSITE k) Source Comments # | |||||||||||||||||
Defined in Proarrow.Category.Opposite fst :: forall (a :: OPPOSITE k) (b :: OPPOSITE k). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: OPPOSITE k) (a' :: OPPOSITE k) (b :: OPPOSITE k). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: OPPOSITE k) (b :: OPPOSITE k). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (b' :: OPPOSITE k). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: OPPOSITE k) (x :: OPPOSITE k) (y :: OPPOSITE k). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (x :: OPPOSITE k) (y :: OPPOSITE k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
BiCCC k => HasBinaryProducts (FK k) Source Comments # | |||||||||||||||||
Defined in Proarrow.Helper.CCC fst :: forall (a :: FK k) (b :: FK k). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: FK k) (a' :: FK k) (b :: FK k). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: FK k) (b :: FK k). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: FK k) (b :: FK k) (b' :: FK k). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: FK k) (x :: FK k) (y :: FK k). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: FK k) (b :: FK k) (x :: FK k) (y :: FK k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
HasBinaryProducts k => HasBinaryProducts (PROD k) Source Comments # | |||||||||||||||||
Defined in Proarrow.Object.BinaryProduct fst :: forall (a :: PROD k) (b :: PROD k). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: PROD k) (a' :: PROD k) (b :: PROD k). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: PROD k) (b :: PROD k). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: PROD k) (b :: PROD k) (b' :: PROD k). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: PROD k) (x :: PROD k) (y :: PROD k). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: PROD k) (b :: PROD k) (x :: PROD k) (y :: PROD k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
(CategoryOf j, CategoryOf k) => HasBinaryProducts (PRO j k) Source Comments # | |||||||||||||||||
Defined in Proarrow.Object.BinaryProduct fst :: forall (a :: PRO j k) (b :: PRO j k). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: PRO j k) (a' :: PRO j k) (b :: PRO j k). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: PRO j k) (b :: PRO j k). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: PRO j k) (b :: PRO j k) (b' :: PRO j k). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: PRO j k) (x :: PRO j k) (y :: PRO j k). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: PRO j k) (b :: PRO j k) (x :: PRO j k) (y :: PRO j k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
(HasBinaryProducts j, HasBinaryProducts k) => HasBinaryProducts (j, k) Source Comments # | |||||||||||||||||
Defined in Proarrow.Object.BinaryProduct fst :: forall (a :: (j, k)) (b :: (j, k)). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: (j, k)) (a' :: (j, k)) (b :: (j, k)). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: (j, k)) (b :: (j, k)). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: (j, k)) (b :: (j, k)) (b' :: (j, k)). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: (j, k)) (x :: (j, k)) (y :: (j, k)). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: (j, k)) (b :: (j, k)) (x :: (j, k)) (y :: (j, k)). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||||||||||||||
HasBinaryProducts (k1 -> Type) Source Comments # | |||||||||||||||||
Defined in Proarrow.Category.Instance.Nat fst :: forall (a :: k1 -> Type) (b :: k1 -> Type). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: k1 -> Type) (a' :: k1 -> Type) (b :: k1 -> Type). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: k1 -> Type) (b :: k1 -> Type). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: k1 -> Type) (b :: k1 -> Type) (b' :: k1 -> Type). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: k1 -> Type) (x :: k1 -> Type) (y :: k1 -> Type). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: k1 -> Type) (b :: k1 -> Type) (x :: k1 -> Type) (y :: k1 -> Type). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # |
first :: forall {k} (c :: k) (a :: k) (b :: k). (HasBinaryProducts k, Ob c) => (a ~> b) -> (a && c) ~> (b && c) Source Comments #
second :: forall {k} (c :: k) (a :: k) (b :: k). (HasBinaryProducts k, Ob c) => (a ~> b) -> (c && a) ~> (c && b) Source Comments #
type HasProducts k = (HasTerminalObject k, HasBinaryProducts k) Source Comments #
class (a ** b) ~ (a && b) => TensorIsProduct (a :: k) (b :: k) Source Comments #
Instances
(a ** b) ~ (a && b) => TensorIsProduct (a :: k) (b :: k) Source Comments # | |
Defined in Proarrow.Object.BinaryProduct |
class (HasProducts k, Monoidal k, (Unit :: k) ~ (TerminalObject :: k), forall (a :: k) (b :: k). TensorIsProduct a b) => Cartesian k Source Comments #
Instances
(HasProducts k, Monoidal k, (Unit :: k) ~ (TerminalObject :: k), forall (a :: k) (b :: k). TensorIsProduct a b) => Cartesian k Source Comments # | |
Defined in Proarrow.Object.BinaryProduct |
leftUnitorProd :: forall {k} (a :: k). (HasProducts k, Ob a) => ((TerminalObject :: k) && a) ~> a Source Comments #
leftUnitorProdInv :: forall {k} (a :: k). (HasProducts k, Ob a) => a ~> ((TerminalObject :: k) && a) Source Comments #
rightUnitorProd :: forall {k} (a :: k). (HasProducts k, Ob a) => (a && (TerminalObject :: k)) ~> a Source Comments #
rightUnitorProdInv :: forall {k} (a :: k). (HasProducts k, Ob a) => a ~> (a && (TerminalObject :: k)) Source Comments #
associatorProd :: forall {k} (a :: k) (b :: k) (c :: k). (HasProducts k, Ob a, Ob b, Ob c) => ((a && b) && c) ~> (a && (b && c)) Source Comments #
associatorProdInv :: forall {k} (a :: k) (b :: k) (c :: k). (HasProducts k, Ob a, Ob b, Ob c) => (a && (b && c)) ~> ((a && b) && c) Source Comments #
swapProd' :: forall k (a :: k) (a' :: k) (b :: k) (b' :: k). HasBinaryProducts k => (a ~> a') -> (b ~> b') -> (a && b) ~> (b' && a') Source Comments #
swapProd :: forall k (a :: k) (b :: k). (HasBinaryProducts k, Ob a, Ob b) => (a && b) ~> (b && a) Source Comments #
newtype PROD k Source Comments #
PR k |
Instances
HasProducts k => Monoidal (PROD k) Source Comments # | |||||
Defined in Proarrow.Object.BinaryProduct
leftUnitor :: forall (a :: PROD k). Ob a => ((Unit :: PROD k) ** a) ~> a Source Comments # leftUnitorInv :: forall (a :: PROD k). Ob a => a ~> ((Unit :: PROD k) ** a) Source Comments # rightUnitor :: forall (a :: PROD k). Ob a => (a ** (Unit :: PROD k)) ~> a Source Comments # rightUnitorInv :: forall (a :: PROD k). Ob a => a ~> (a ** (Unit :: PROD k)) Source Comments # associator :: forall (a :: PROD k) (b :: PROD k) (c :: PROD k). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Comments # associatorInv :: forall (a :: PROD k) (b :: PROD k) (c :: PROD k). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Comments # | |||||
HasProducts k => SymMonoidal (PROD k) Source Comments # | |||||
BiCCC k => Distributive (PROD k) Source Comments # | |||||
Defined in Proarrow.Category.Monoidal.Distributive 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 Comments # 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 Comments # distL0 :: forall (a :: PROD k). Ob a => (a ** (InitialObject :: PROD k)) ~> (InitialObject :: PROD k) Source Comments # distR0 :: forall (a :: PROD k). Ob a => ((InitialObject :: PROD k) ** a) ~> (InitialObject :: PROD k) Source Comments # | |||||
CategoryOf k => CategoryOf (PROD k) Source Comments # | |||||
Defined in Proarrow.Object.BinaryProduct | |||||
HasBinaryCoproducts k => HasBinaryCoproducts (PROD k) Source Comments # | |||||
Defined in Proarrow.Object.BinaryCoproduct lft :: forall (a :: PROD k) (b :: PROD k). (Ob a, Ob b) => a ~> (a || b) Source Comments # lft' :: forall (a :: PROD k) (a' :: PROD k) (b :: PROD k). (a ~> a') -> Obj b -> a ~> (a' || b) Source Comments # rgt :: forall (a :: PROD k) (b :: PROD k). (Ob a, Ob b) => b ~> (a || b) Source Comments # rgt' :: forall (a :: PROD k) (b :: PROD k) (b' :: PROD k). Obj a -> (b ~> b') -> b ~> (a || b') Source Comments # (|||) :: forall (x :: PROD k) (a :: PROD k) (y :: PROD k). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Comments # (+++) :: forall (a :: PROD k) (b :: PROD k) (x :: PROD k) (y :: PROD k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Comments # | |||||
HasBinaryProducts k => HasBinaryProducts (PROD k) Source Comments # | |||||
Defined in Proarrow.Object.BinaryProduct fst :: forall (a :: PROD k) (b :: PROD k). (Ob a, Ob b) => (a && b) ~> a Source Comments # fst' :: forall (a :: PROD k) (a' :: PROD k) (b :: PROD k). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments # snd :: forall (a :: PROD k) (b :: PROD k). (Ob a, Ob b) => (a && b) ~> b Source Comments # snd' :: forall (a :: PROD k) (b :: PROD k) (b' :: PROD k). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments # (&&&) :: forall (a :: PROD k) (x :: PROD k) (y :: PROD k). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments # (***) :: forall (a :: PROD k) (b :: PROD k) (x :: PROD k) (y :: PROD k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments # | |||||
(CategoryOf j, CategoryOf k) => Closed (PROD (PRO j k)) Source Comments # | |||||
Defined in Proarrow.Object.Exponential curry' :: forall (a :: PROD (PRO j k)) (b :: PROD (PRO j k)) (c :: PROD (PRO j k)). Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c) Source Comments # uncurry' :: forall (b :: PROD (PRO j k)) (c :: PROD (PRO j k)) (a :: PROD (PRO j k)). Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c Source Comments # (^^^) :: forall (b :: PROD (PRO j k)) (y :: PROD (PRO j k)) (x :: PROD (PRO j k)) (a :: PROD (PRO j k)). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Comments # | |||||
CategoryOf k1 => Closed (PROD (k1 -> Type)) Source Comments # | |||||
Defined in Proarrow.Category.Instance.Nat curry' :: forall (a :: PROD (k1 -> Type)) (b :: PROD (k1 -> Type)) (c :: PROD (k1 -> Type)). Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c) Source Comments # uncurry' :: forall (b :: PROD (k1 -> Type)) (c :: PROD (k1 -> Type)) (a :: PROD (k1 -> Type)). Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c Source Comments # (^^^) :: forall (b :: PROD (k1 -> Type)) (y :: PROD (k1 -> Type)) (x :: PROD (k1 -> Type)) (a :: PROD (k1 -> Type)). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Comments # | |||||
HasInitialObject k => HasInitialObject (PROD k) Source Comments # | |||||
Defined in Proarrow.Object.BinaryProduct
| |||||
HasTerminalObject k => HasTerminalObject (PROD k) Source Comments # | |||||
Defined in Proarrow.Object.BinaryProduct
| |||||
(HasProducts k, Category cat) => MonoidalProfunctor (Prod cat :: PROD k -> PROD k -> Type) Source Comments # | |||||
Profunctor p => Profunctor (Prod p :: PROD k -> PROD j -> Type) Source Comments # | |||||
(HasProducts k, Ob a) => Comonoid ('PR a :: PROD k) Source Comments # | |||||
Profunctor p => Monoid ('PR (FreeMonoid p) :: PROD (k -> k -> Type)) Source Comments # | |||||
Defined in Proarrow.Profunctor.Free | |||||
Promonad p => Promonad (Prod p :: PROD j -> PROD j -> Type) Source Comments # | |||||
type UN ('PR :: j -> PROD j) ('PR k :: PROD j) Source Comments # | |||||
type Unit Source Comments # | |||||
Defined in Proarrow.Object.BinaryProduct | |||||
type (~>) Source Comments # | |||||
Defined in Proarrow.Object.BinaryProduct | |||||
type InitialObject Source Comments # | |||||
Defined in Proarrow.Object.BinaryProduct | |||||
type TerminalObject Source Comments # | |||||
Defined in Proarrow.Object.BinaryProduct | |||||
type Ob (a :: PROD k) Source Comments # | |||||
type (a :: PROD k) ** (b :: PROD k) Source Comments # | |||||
Defined in Proarrow.Object.BinaryProduct | |||||
type (a :: PROD k) && (b :: PROD k) Source Comments # | |||||
type (p :: PROD (j -> k -> Type)) ~~> (q :: PROD (j -> k -> Type)) Source Comments # | |||||
type (f :: PROD (k1 -> Type)) ~~> (g :: PROD (k1 -> Type)) Source Comments # | |||||
type ('PR a :: PROD k) || ('PR b :: PROD k) Source Comments # | |||||
data Prod (p :: j +-> k) (a :: PROD k) (b :: PROD j) where Source Comments #
class (Strong ((~>) :: CAT k) p, HasProducts k, forall (a :: k) (b :: k). ActIsProd a b) => StrongProd (p :: CAT k) Source Comments #
Instances
(Strong ((~>) :: CAT k) p, HasProducts k, forall (a :: k) (b :: k). ActIsProd a b) => StrongProd (p :: k +-> k) Source Comments # | |
Defined in Proarrow.Object.BinaryProduct |
first' :: forall {k} p (c :: k) (a :: k) (b :: k). (StrongProd p, Ob c) => p a b -> p (a && c) (b && c) Source Comments #
second' :: forall {k} p (c :: k) (a :: k) (b :: k). (StrongProd p, Ob c) => p a b -> p (c && a) (c && b) Source Comments #