Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- type O2 k a b = (Obj k a, Obj k b)
- type O3 k a b c = (Obj k a, Obj k b, Obj k c)
- type O4 k a b c d = (Obj k a, Obj k b, Obj k c, Obj k d)
- class Category (cat :: k -> k -> Type) where
- class Category cat => Dagger cat where
- (∘) :: forall {k} (cat :: k -> k -> Type) a b c con. (Category cat, con ~ Obj cat, con a, con b, con c) => cat b c -> cat a b -> cat a c
- class Category cat => Monoidal x i (cat :: k -> k -> Type) | x -> i, i -> x where
- (⊗) :: (Obj cat a, Obj cat b, Obj cat c, Obj cat d) => (a `cat` b) -> (c `cat` d) -> (a `x` c) `cat` (b `x` d)
- assoc :: (Obj cat a, Obj cat b, Obj cat c) => ((a `x` b) `x` c) `cat` (a `x` (b `x` c))
- assoc_ :: (Obj cat a, Obj cat b, Obj cat c) => (a `x` (b `x` c)) `cat` ((a `x` b) `x` c)
- unitorR :: (Obj cat a, Obj cat i) => a `cat` (a `x` i)
- unitorR_ :: (Obj cat a, Obj cat i) => (a `x` i) `cat` a
- unitorL :: (Obj cat a, Obj cat i) => a `cat` (i `x` a)
- unitorL_ :: (Obj cat a, Obj cat i) => (i `x` a) `cat` a
- monoidalRec :: forall x cat i. Monoidal x i cat => MonoidalRec x i (Obj cat) cat
- class Monoidal x i cat => Braided x i cat where
- braidedRec :: forall x cat i. Braided x i cat => BraidedRec x i (Obj cat) cat
- class Braided x i cat => Symmetric x i cat
- class Symmetric x i cat => Cartesian x i cat where
- cartesianRec :: forall x cat i. Cartesian x i cat => CartesianRec x i (Obj cat) cat
- cartesianCross :: (Obj k (b1 `x` b2), Obj k b3, Obj k c, Obj k b1, Obj k b2, Cartesian x i k) => k b1 b3 -> k b2 c -> k (b1 `x` b2) (b3 `x` c)
- cartesianUnitor :: forall a k x i. (Obj k a, Obj k i, Cartesian x i k) => a `k` (a `x` i)
- cartesianUnitor_ :: forall a k x i. (Obj k a, Obj k i, Cartesian x i k) => (a `x` i) `k` a
- cartesianSwap :: forall a b k x i con. (Obj k a, Obj k b, Cartesian x i k, Con' x con, con ~ Obj k) => (a `x` b) `k` (b `x` a)
- cartesianAssoc :: forall a b x i c k con. (Obj k a, Obj k b, Obj k c, Cartesian x i k, Con' x con, con ~ Obj k) => ((a `x` b) `x` c) `k` (a `x` (b `x` c))
- cartesianAssoc_ :: forall a b x i c k con. (Obj k a, Obj k b, Obj k c, Cartesian x i k, Con' x con, con ~ Obj k) => (a `x` (b `x` c)) `k` ((a `x` b) `x` c)
- coCartesianExl :: (O2 cat a b, CoCartesian x i cat, Additive (cat b a)) => (a `x` b) `cat` a
- coCartesianExr :: (O2 cat a b, CoCartesian x i cat, Additive (cat a b)) => (a `x` b) `cat` b
- class Symmetric x i cat => CoCartesian x i cat where
- type BiCartesian x i cat = (Cartesian x i cat, CoCartesian x i cat)
- class Monoidal x i cat => Autonomous x i l r cat | x -> l, x -> r where
- class (Symmetric x i cat, Autonomous x i d d cat) => Compact x i d cat
Documentation
class Category (cat :: k -> k -> Type) where Source #
A class for categories. Instances should satisfy the laws
f.
id
= f -- (right identity)id
.
f = f -- (left identity) f.
(g.
h) = (f.
g).
h -- (associativity)
type Obj cat :: k -> Constraint Source #
(.) :: (Obj cat a, Obj cat b, Obj cat c) => (b `cat` c) -> (a `cat` b) -> a `cat` c infixr 9 Source #
Instances
Ring s => Category (M s :: Type -> Type -> Type) Source # | |
Ring s => Category (Rel s :: Type -> Type -> Type) Source # | |
Category (->) Source # | |
Category k2 => Category (Op k2 :: k1 -> k1 -> Type) Source # | |
Category NatTrans Source # | |
Ring s => Category (Mat s :: (Type -> Type) -> (Type -> Type) -> Type) Source # | |
(∘) :: forall {k} (cat :: k -> k -> Type) a b c con. (Category cat, con ~ Obj cat, con a, con b, con c) => cat b c -> cat a b -> cat a c Source #
class Category cat => Monoidal x i (cat :: k -> k -> Type) | x -> i, i -> x where Source #
(⊗) :: (Obj cat a, Obj cat b, Obj cat c, Obj cat d) => (a `cat` b) -> (c `cat` d) -> (a `x` c) `cat` (b `x` d) Source #
assoc :: (Obj cat a, Obj cat b, Obj cat c) => ((a `x` b) `x` c) `cat` (a `x` (b `x` c)) Source #
assoc_ :: (Obj cat a, Obj cat b, Obj cat c) => (a `x` (b `x` c)) `cat` ((a `x` b) `x` c) Source #
unitorR :: (Obj cat a, Obj cat i) => a `cat` (a `x` i) Source #
unitorR_ :: (Obj cat a, Obj cat i) => (a `x` i) `cat` a Source #
unitorL :: (Obj cat a, Obj cat i) => a `cat` (i `x` a) Source #
default unitorL :: forall a con. (con ~ Obj cat, con i, con (x a i), con (x i a), Symmetric x i cat, Obj cat a) => a `cat` (i `x` a) Source #
unitorL_ :: (Obj cat a, Obj cat i) => (i `x` a) `cat` a Source #
Instances
Monoidal (,) () (->) Source # | |
Defined in Algebra.Category (⊗) :: forall (a :: k) (b :: k) (c :: k) (d :: k). (Obj (->) a, Obj (->) b, Obj (->) c, Obj (->) d) => (a -> b) -> (c -> d) -> (a, c) -> (b, d) Source # assoc :: forall (a :: k) (b :: k) (c :: k). (Obj (->) a, Obj (->) b, Obj (->) c) => ((a, b), c) -> (a, (b, c)) Source # assoc_ :: forall (a :: k) (b :: k) (c :: k). (Obj (->) a, Obj (->) b, Obj (->) c) => (a, (b, c)) -> ((a, b), c) Source # unitorR :: forall (a :: k). (Obj (->) a, Obj (->) ()) => a -> (a, ()) Source # unitorR_ :: forall (a :: k). (Obj (->) a, Obj (->) ()) => (a, ()) -> a Source # unitorL :: forall (a :: k). (Obj (->) a, Obj (->) ()) => a -> ((), a) Source # unitorL_ :: forall (a :: k). (Obj (->) a, Obj (->) ()) => ((), a) -> a Source # | |
Monoidal x i k2 => Monoidal (x :: k1 -> k1 -> k1) (i :: k1) (Op k2 :: k1 -> k1 -> Type) Source # | |
Defined in Algebra.Category.Op (⊗) :: forall (a :: k) (b :: k) (c :: k) (d :: k). (Obj (Op k2) a, Obj (Op k2) b, Obj (Op k2) c, Obj (Op k2) d) => Op k2 a b -> Op k2 c d -> Op k2 (x a c) (x b d) Source # assoc :: forall (a :: k) (b :: k) (c :: k). (Obj (Op k2) a, Obj (Op k2) b, Obj (Op k2) c) => Op k2 (x (x a b) c) (x a (x b c)) Source # assoc_ :: forall (a :: k) (b :: k) (c :: k). (Obj (Op k2) a, Obj (Op k2) b, Obj (Op k2) c) => Op k2 (x a (x b c)) (x (x a b) c) Source # unitorR :: forall (a :: k). (Obj (Op k2) a, Obj (Op k2) i) => Op k2 a (x a i) Source # unitorR_ :: forall (a :: k). (Obj (Op k2) a, Obj (Op k2) i) => Op k2 (x a i) a Source # unitorL :: forall (a :: k). (Obj (Op k2) a, Obj (Op k2) i) => Op k2 a (x i a) Source # unitorL_ :: forall (a :: k). (Obj (Op k2) a, Obj (Op k2) i) => Op k2 (x i a) a Source # | |
Ring s => Monoidal ((⊕) :: Type -> Type -> Type) (Zero :: Type) (M s :: Type -> Type -> Type) Source # | |
Defined in Algebra.Category.BlockMatrix (⊗) :: forall (a :: k) (b :: k) (c :: k) (d :: k). (Obj (M s) a, Obj (M s) b, Obj (M s) c, Obj (M s) d) => M s a b -> M s c d -> M s (a ⊕ c) (b ⊕ d) Source # assoc :: forall (a :: k) (b :: k) (c :: k). (Obj (M s) a, Obj (M s) b, Obj (M s) c) => M s ((a ⊕ b) ⊕ c) (a ⊕ (b ⊕ c)) Source # assoc_ :: forall (a :: k) (b :: k) (c :: k). (Obj (M s) a, Obj (M s) b, Obj (M s) c) => M s (a ⊕ (b ⊕ c)) ((a ⊕ b) ⊕ c) Source # unitorR :: forall (a :: k). (Obj (M s) a, Obj (M s) Zero) => M s a (a ⊕ Zero) Source # unitorR_ :: forall (a :: k). (Obj (M s) a, Obj (M s) Zero) => M s (a ⊕ Zero) a Source # unitorL :: forall (a :: k). (Obj (M s) a, Obj (M s) Zero) => M s a (Zero ⊕ a) Source # unitorL_ :: forall (a :: k). (Obj (M s) a, Obj (M s) Zero) => M s (Zero ⊕ a) a Source # | |
Ring s => Monoidal ((⊕) :: Type -> Type -> Type) (Zero :: Type) (Rel s :: Type -> Type -> Type) Source # | |
Defined in Algebra.Category.Relation (⊗) :: forall (a :: k) (b :: k) (c :: k) (d :: k). (Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c, Obj (Rel s) d) => Rel s a b -> Rel s c d -> Rel s (a ⊕ c) (b ⊕ d) Source # assoc :: forall (a :: k) (b :: k) (c :: k). (Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) => Rel s ((a ⊕ b) ⊕ c) (a ⊕ (b ⊕ c)) Source # assoc_ :: forall (a :: k) (b :: k) (c :: k). (Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) => Rel s (a ⊕ (b ⊕ c)) ((a ⊕ b) ⊕ c) Source # unitorR :: forall (a :: k). (Obj (Rel s) a, Obj (Rel s) Zero) => Rel s a (a ⊕ Zero) Source # unitorR_ :: forall (a :: k). (Obj (Rel s) a, Obj (Rel s) Zero) => Rel s (a ⊕ Zero) a Source # unitorL :: forall (a :: k). (Obj (Rel s) a, Obj (Rel s) Zero) => Rel s a (Zero ⊕ a) Source # unitorL_ :: forall (a :: k). (Obj (Rel s) a, Obj (Rel s) Zero) => Rel s (Zero ⊕ a) a Source # | |
Ring s => Monoidal ((⊗) :: Type -> Type -> Type) (One :: Type) (Rel s :: Type -> Type -> Type) Source # | |
Defined in Algebra.Category.Relation (⊗) :: forall (a :: k) (b :: k) (c :: k) (d :: k). (Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c, Obj (Rel s) d) => Rel s a b -> Rel s c d -> Rel s (a ⊗ c) (b ⊗ d) Source # assoc :: forall (a :: k) (b :: k) (c :: k). (Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) => Rel s ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c)) Source # assoc_ :: forall (a :: k) (b :: k) (c :: k). (Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) => Rel s (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c) Source # unitorR :: forall (a :: k). (Obj (Rel s) a, Obj (Rel s) One) => Rel s a (a ⊗ One) Source # unitorR_ :: forall (a :: k). (Obj (Rel s) a, Obj (Rel s) One) => Rel s (a ⊗ One) a Source # unitorL :: forall (a :: k). (Obj (Rel s) a, Obj (Rel s) One) => Rel s a (One ⊗ a) Source # unitorL_ :: forall (a :: k). (Obj (Rel s) a, Obj (Rel s) One) => Rel s (One ⊗ a) a Source # | |
Monoidal ((⊕) :: Type -> Type -> Type) (Zero :: Type) (->) Source # | |
Defined in Algebra.Category (⊗) :: forall (a :: k) (b :: k) (c :: k) (d :: k). (Obj (->) a, Obj (->) b, Obj (->) c, Obj (->) d) => (a -> b) -> (c -> d) -> (a ⊕ c) -> (b ⊕ d) Source # assoc :: forall (a :: k) (b :: k) (c :: k). (Obj (->) a, Obj (->) b, Obj (->) c) => ((a ⊕ b) ⊕ c) -> (a ⊕ (b ⊕ c)) Source # assoc_ :: forall (a :: k) (b :: k) (c :: k). (Obj (->) a, Obj (->) b, Obj (->) c) => (a ⊕ (b ⊕ c)) -> ((a ⊕ b) ⊕ c) Source # unitorR :: forall (a :: k). (Obj (->) a, Obj (->) Zero) => a -> (a ⊕ Zero) Source # unitorR_ :: forall (a :: k). (Obj (->) a, Obj (->) Zero) => (a ⊕ Zero) -> a Source # unitorL :: forall (a :: k). (Obj (->) a, Obj (->) Zero) => a -> (Zero ⊕ a) Source # unitorL_ :: forall (a :: k). (Obj (->) a, Obj (->) Zero) => (Zero ⊕ a) -> a Source # | |
Monoidal ((⊗) :: Type -> Type -> Type) (One :: Type) (->) Source # | |
Defined in Algebra.Category (⊗) :: forall (a :: k) (b :: k) (c :: k) (d :: k). (Obj (->) a, Obj (->) b, Obj (->) c, Obj (->) d) => (a -> b) -> (c -> d) -> (a ⊗ c) -> (b ⊗ d) Source # assoc :: forall (a :: k) (b :: k) (c :: k). (Obj (->) a, Obj (->) b, Obj (->) c) => ((a ⊗ b) ⊗ c) -> (a ⊗ (b ⊗ c)) Source # assoc_ :: forall (a :: k) (b :: k) (c :: k). (Obj (->) a, Obj (->) b, Obj (->) c) => (a ⊗ (b ⊗ c)) -> ((a ⊗ b) ⊗ c) Source # unitorR :: forall (a :: k). (Obj (->) a, Obj (->) One) => a -> (a ⊗ One) Source # unitorR_ :: forall (a :: k). (Obj (->) a, Obj (->) One) => (a ⊗ One) -> a Source # unitorL :: forall (a :: k). (Obj (->) a, Obj (->) One) => a -> (One ⊗ a) Source # unitorL_ :: forall (a :: k). (Obj (->) a, Obj (->) One) => (One ⊗ a) -> a Source # | |
Monoidal ((⊗) :: (Type -> Type) -> (Type -> Type) -> Type -> Type) (One :: Type -> Type) NatTrans Source # | |
Defined in Algebra.Category.NatTrans (⊗) :: forall (a :: k) (b :: k) (c :: k) (d :: k). (Obj NatTrans a, Obj NatTrans b, Obj NatTrans c, Obj NatTrans d) => NatTrans a b -> NatTrans c d -> NatTrans (a ⊗ c) (b ⊗ d) Source # assoc :: forall (a :: k) (b :: k) (c :: k). (Obj NatTrans a, Obj NatTrans b, Obj NatTrans c) => NatTrans ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c)) Source # assoc_ :: forall (a :: k) (b :: k) (c :: k). (Obj NatTrans a, Obj NatTrans b, Obj NatTrans c) => NatTrans (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c) Source # unitorR :: forall (a :: k). (Obj NatTrans a, Obj NatTrans One) => NatTrans a (a ⊗ One) Source # unitorR_ :: forall (a :: k). (Obj NatTrans a, Obj NatTrans One) => NatTrans (a ⊗ One) a Source # unitorL :: forall (a :: k). (Obj NatTrans a, Obj NatTrans One) => NatTrans a (One ⊗ a) Source # unitorL_ :: forall (a :: k). (Obj NatTrans a, Obj NatTrans One) => NatTrans (One ⊗ a) a Source # | |
Ring s => Monoidal ((⊗) :: (Type -> Type) -> (Type -> Type) -> Type -> Type) (One :: Type -> Type) (Mat s :: (Type -> Type) -> (Type -> Type) -> Type) Source # | |
Defined in Algebra.Linear (⊗) :: forall (a :: k) (b :: k) (c :: k) (d :: k). (Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c, Obj (Mat s) d) => Mat s a b -> Mat s c d -> Mat s (a ⊗ c) (b ⊗ d) Source # assoc :: forall (a :: k) (b :: k) (c :: k). (Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c) => Mat s ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c)) Source # assoc_ :: forall (a :: k) (b :: k) (c :: k). (Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c) => Mat s (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c) Source # unitorR :: forall (a :: k). (Obj (Mat s) a, Obj (Mat s) One) => Mat s a (a ⊗ One) Source # unitorR_ :: forall (a :: k). (Obj (Mat s) a, Obj (Mat s) One) => Mat s (a ⊗ One) a Source # unitorL :: forall (a :: k). (Obj (Mat s) a, Obj (Mat s) One) => Mat s a (One ⊗ a) Source # unitorL_ :: forall (a :: k). (Obj (Mat s) a, Obj (Mat s) One) => Mat s (One ⊗ a) a Source # | |
Monoidal ((∘) :: (Type -> Type) -> (Type -> Type) -> Type -> Type) Id NatTrans Source # | |
Defined in Algebra.Category.NatTrans (⊗) :: forall (a :: k) (b :: k) (c :: k) (d :: k). (Obj NatTrans a, Obj NatTrans b, Obj NatTrans c, Obj NatTrans d) => NatTrans a b -> NatTrans c d -> NatTrans (a ∘ c) (b ∘ d) Source # assoc :: forall (a :: k) (b :: k) (c :: k). (Obj NatTrans a, Obj NatTrans b, Obj NatTrans c) => NatTrans ((a ∘ b) ∘ c) (a ∘ (b ∘ c)) Source # assoc_ :: forall (a :: k) (b :: k) (c :: k). (Obj NatTrans a, Obj NatTrans b, Obj NatTrans c) => NatTrans (a ∘ (b ∘ c)) ((a ∘ b) ∘ c) Source # unitorR :: forall (a :: k). (Obj NatTrans a, Obj NatTrans Id) => NatTrans a (a ∘ Id) Source # unitorR_ :: forall (a :: k). (Obj NatTrans a, Obj NatTrans Id) => NatTrans (a ∘ Id) a Source # unitorL :: forall (a :: k). (Obj NatTrans a, Obj NatTrans Id) => NatTrans a (Id ∘ a) Source # unitorL_ :: forall (a :: k). (Obj NatTrans a, Obj NatTrans Id) => NatTrans (Id ∘ a) a Source # | |
Ring s => Monoidal ((∘) :: (Type -> Type) -> (Type -> Type) -> Type -> Type) Id (Mat s :: (Type -> Type) -> (Type -> Type) -> Type) Source # | |
Defined in Algebra.Linear (⊗) :: forall (a :: k) (b :: k) (c :: k) (d :: k). (Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c, Obj (Mat s) d) => Mat s a b -> Mat s c d -> Mat s (a ∘ c) (b ∘ d) Source # assoc :: forall (a :: k) (b :: k) (c :: k). (Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c) => Mat s ((a ∘ b) ∘ c) (a ∘ (b ∘ c)) Source # assoc_ :: forall (a :: k) (b :: k) (c :: k). (Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c) => Mat s (a ∘ (b ∘ c)) ((a ∘ b) ∘ c) Source # unitorR :: forall (a :: k). (Obj (Mat s) a, Obj (Mat s) Id) => Mat s a (a ∘ Id) Source # unitorR_ :: forall (a :: k). (Obj (Mat s) a, Obj (Mat s) Id) => Mat s (a ∘ Id) a Source # unitorL :: forall (a :: k). (Obj (Mat s) a, Obj (Mat s) Id) => Mat s a (Id ∘ a) Source # unitorL_ :: forall (a :: k). (Obj (Mat s) a, Obj (Mat s) Id) => Mat s (Id ∘ a) a Source # |
monoidalRec :: forall x cat i. Monoidal x i cat => MonoidalRec x i (Obj cat) cat Source #
class Monoidal x i cat => Braided x i cat where Source #
swap :: (Obj cat a, Obj cat b) => (a `x` b) `cat` (b `x` a) Source #
swap_ :: (Obj cat a, Obj cat b) => (a `x` b) `cat` (b `x` a) Source #
Instances
Braided (,) () (->) Source # | |
Braided x i k2 => Braided (x :: k1 -> k1 -> k1) (i :: k1) (Op k2 :: k1 -> k1 -> Type) Source # | |
Ring s => Braided ((⊕) :: Type -> Type -> Type) (Zero :: Type) (M s :: Type -> Type -> Type) Source # | |
Ring s => Braided ((⊕) :: Type -> Type -> Type) (Zero :: Type) (Rel s :: Type -> Type -> Type) Source # | |
Ring s => Braided ((⊗) :: Type -> Type -> Type) (One :: Type) (Rel s :: Type -> Type -> Type) Source # | |
Braided ((⊕) :: Type -> Type -> Type) (Zero :: Type) (->) Source # | |
Braided ((⊗) :: Type -> Type -> Type) (One :: Type) (->) Source # | |
Ring s => Braided ((⊗) :: (Type -> Type) -> (Type -> Type) -> Type -> Type) (One :: Type -> Type) (Mat s :: (Type -> Type) -> (Type -> Type) -> Type) Source # | |
Ring s => Braided ((∘) :: (Type -> Type) -> (Type -> Type) -> Type -> Type) Id (Mat s :: (Type -> Type) -> (Type -> Type) -> Type) Source # | |
braidedRec :: forall x cat i. Braided x i cat => BraidedRec x i (Obj cat) cat Source #
class Braided x i cat => Symmetric x i cat Source #
Instances
class Symmetric x i cat => Cartesian x i cat where Source #
exl :: forall a b. O2 cat a b => (a `x` b) `cat` a Source #
default exl :: forall a b con. (con ~ Obj cat, con i, Con' x con, con a, con b) => (a `x` b) `cat` a Source #
exr :: forall a b. O2 cat a b => (a `x` b) `cat` b Source #
default exr :: forall a b con. (con ~ Obj cat, con i, Con' x con, con a, con b) => (a `x` b) `cat` b Source #
dis :: forall a. Obj cat a => a `cat` i Source #
dup :: forall a. Obj cat a => a `cat` (a `x` a) Source #
default dup :: forall a con. (con ~ Obj cat, con i, Con' x con, Obj cat a) => a `cat` (a `x` a) Source #
(▵) :: forall a b c. (Obj cat a, Obj cat b, Obj cat c) => (a `cat` b) -> (a `cat` c) -> a `cat` (b `x` c) Source #
Instances
Cartesian (,) () (->) Source # | |
Defined in Algebra.Category exl :: forall (a :: k) (b :: k). O2 (->) a b => (a, b) -> a Source # exr :: forall (a :: k) (b :: k). O2 (->) a b => (a, b) -> b Source # dis :: forall (a :: k). Obj (->) a => a -> () Source # dup :: forall (a :: k). Obj (->) a => a -> (a, a) Source # (▵) :: forall (a :: k) (b :: k) (c :: k). (Obj (->) a, Obj (->) b, Obj (->) c) => (a -> b) -> (a -> c) -> a -> (b, c) Source # | |
CoCartesian x i k2 => Cartesian (x :: k1 -> k1 -> k1) (i :: k1) (Op k2 :: k1 -> k1 -> Type) Source # | |
Defined in Algebra.Category.Op exl :: forall (a :: k) (b :: k). O2 (Op k2) a b => Op k2 (x a b) a Source # exr :: forall (a :: k) (b :: k). O2 (Op k2) a b => Op k2 (x a b) b Source # dis :: forall (a :: k). Obj (Op k2) a => Op k2 a i Source # dup :: forall (a :: k). Obj (Op k2) a => Op k2 a (x a a) Source # (▵) :: forall (a :: k) (b :: k) (c :: k). (Obj (Op k2) a, Obj (Op k2) b, Obj (Op k2) c) => Op k2 a b -> Op k2 a c -> Op k2 a (x b c) Source # | |
Ring s => Cartesian ((⊕) :: Type -> Type -> Type) (Zero :: Type) (M s :: Type -> Type -> Type) Source # | |
Defined in Algebra.Category.BlockMatrix exl :: forall (a :: k) (b :: k). O2 (M s) a b => M s (a ⊕ b) a Source # exr :: forall (a :: k) (b :: k). O2 (M s) a b => M s (a ⊕ b) b Source # dis :: forall (a :: k). Obj (M s) a => M s a Zero Source # dup :: forall (a :: k). Obj (M s) a => M s a (a ⊕ a) Source # (▵) :: forall (a :: k) (b :: k) (c :: k). (Obj (M s) a, Obj (M s) b, Obj (M s) c) => M s a b -> M s a c -> M s a (b ⊕ c) Source # | |
Ring s => Cartesian ((⊕) :: Type -> Type -> Type) (Zero :: Type) (Rel s :: Type -> Type -> Type) Source # | |
Defined in Algebra.Category.Relation exl :: forall (a :: k) (b :: k). O2 (Rel s) a b => Rel s (a ⊕ b) a Source # exr :: forall (a :: k) (b :: k). O2 (Rel s) a b => Rel s (a ⊕ b) b Source # dis :: forall (a :: k). Obj (Rel s) a => Rel s a Zero Source # dup :: forall (a :: k). Obj (Rel s) a => Rel s a (a ⊕ a) Source # (▵) :: forall (a :: k) (b :: k) (c :: k). (Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) => Rel s a b -> Rel s a c -> Rel s a (b ⊕ c) Source # | |
Ring s => Cartesian ((⊗) :: Type -> Type -> Type) (One :: Type) (Rel s :: Type -> Type -> Type) Source # | |
Defined in Algebra.Category.Relation exl :: forall (a :: k) (b :: k). O2 (Rel s) a b => Rel s (a ⊗ b) a Source # exr :: forall (a :: k) (b :: k). O2 (Rel s) a b => Rel s (a ⊗ b) b Source # dis :: forall (a :: k). Obj (Rel s) a => Rel s a One Source # dup :: forall (a :: k). Obj (Rel s) a => Rel s a (a ⊗ a) Source # (▵) :: forall (a :: k) (b :: k) (c :: k). (Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) => Rel s a b -> Rel s a c -> Rel s a (b ⊗ c) Source # | |
Cartesian ((⊗) :: Type -> Type -> Type) (One :: Type) (->) Source # | |
Defined in Algebra.Category exl :: forall (a :: k) (b :: k). O2 (->) a b => (a ⊗ b) -> a Source # exr :: forall (a :: k) (b :: k). O2 (->) a b => (a ⊗ b) -> b Source # dis :: forall (a :: k). Obj (->) a => a -> One Source # dup :: forall (a :: k). Obj (->) a => a -> (a ⊗ a) Source # (▵) :: forall (a :: k) (b :: k) (c :: k). (Obj (->) a, Obj (->) b, Obj (->) c) => (a -> b) -> (a -> c) -> a -> (b ⊗ c) Source # | |
Ring s => Cartesian ((⊗) :: (Type -> Type) -> (Type -> Type) -> Type -> Type) (One :: Type -> Type) (Mat s :: (Type -> Type) -> (Type -> Type) -> Type) Source # | |
Defined in Algebra.Linear exl :: forall (a :: k) (b :: k). O2 (Mat s) a b => Mat s (a ⊗ b) a Source # exr :: forall (a :: k) (b :: k). O2 (Mat s) a b => Mat s (a ⊗ b) b Source # dis :: forall (a :: k). Obj (Mat s) a => Mat s a One Source # dup :: forall (a :: k). Obj (Mat s) a => Mat s a (a ⊗ a) Source # (▵) :: forall (a :: k) (b :: k) (c :: k). (Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c) => Mat s a b -> Mat s a c -> Mat s a (b ⊗ c) Source # |
cartesianRec :: forall x cat i. Cartesian x i cat => CartesianRec x i (Obj cat) cat Source #
cartesianCross :: (Obj k (b1 `x` b2), Obj k b3, Obj k c, Obj k b1, Obj k b2, Cartesian x i k) => k b1 b3 -> k b2 c -> k (b1 `x` b2) (b3 `x` c) Source #
cartesianSwap :: forall a b k x i con. (Obj k a, Obj k b, Cartesian x i k, Con' x con, con ~ Obj k) => (a `x` b) `k` (b `x` a) Source #
cartesianAssoc :: forall a b x i c k con. (Obj k a, Obj k b, Obj k c, Cartesian x i k, Con' x con, con ~ Obj k) => ((a `x` b) `x` c) `k` (a `x` (b `x` c)) Source #
cartesianAssoc_ :: forall a b x i c k con. (Obj k a, Obj k b, Obj k c, Cartesian x i k, Con' x con, con ~ Obj k) => (a `x` (b `x` c)) `k` ((a `x` b) `x` c) Source #
coCartesianExl :: (O2 cat a b, CoCartesian x i cat, Additive (cat b a)) => (a `x` b) `cat` a Source #
coCartesianExr :: (O2 cat a b, CoCartesian x i cat, Additive (cat a b)) => (a `x` b) `cat` b Source #
class Symmetric x i cat => CoCartesian x i cat where Source #
inl :: O2 cat a b => a `cat` (a `x` b) Source #
default inl :: forall a b con. (con ~ Obj cat, con i, Con' x con, con a, con b) => a `cat` (a `x` b) Source #
inr :: O2 cat a b => b `cat` (a `x` b) Source #
default inr :: forall a b con. (con ~ Obj cat, con i, Con' x con, con a, con b) => b `cat` (a `x` b) Source #
new :: forall a. Obj cat a => i `cat` a Source #
jam :: Obj cat a => (a `x` a) `cat` a Source #
default jam :: forall a con. (con ~ Obj cat, con i, Con' x con, Obj cat a) => (a `x` a) `cat` a Source #
(▿) :: forall a b c. (Obj cat a, Obj cat b, Obj cat c) => (b `cat` a) -> (c `cat` a) -> (b `x` c) `cat` a Source #
Instances
Cartesian x i k2 => CoCartesian (x :: k1 -> k1 -> k1) (i :: k1) (Op k2 :: k1 -> k1 -> Type) Source # | |
Defined in Algebra.Category.Op inl :: forall (a :: k) (b :: k). O2 (Op k2) a b => Op k2 a (x a b) Source # inr :: forall (a :: k) (b :: k). O2 (Op k2) a b => Op k2 b (x a b) Source # new :: forall (a :: k). Obj (Op k2) a => Op k2 i a Source # jam :: forall (a :: k). Obj (Op k2) a => Op k2 (x a a) a Source # (▿) :: forall (a :: k) (b :: k) (c :: k). (Obj (Op k2) a, Obj (Op k2) b, Obj (Op k2) c) => Op k2 b a -> Op k2 c a -> Op k2 (x b c) a Source # | |
Ring s => CoCartesian ((⊕) :: Type -> Type -> Type) (Zero :: Type) (M s :: Type -> Type -> Type) Source # | |
Defined in Algebra.Category.BlockMatrix inl :: forall (a :: k) (b :: k). O2 (M s) a b => M s a (a ⊕ b) Source # inr :: forall (a :: k) (b :: k). O2 (M s) a b => M s b (a ⊕ b) Source # new :: forall (a :: k). Obj (M s) a => M s Zero a Source # jam :: forall (a :: k). Obj (M s) a => M s (a ⊕ a) a Source # (▿) :: forall (a :: k) (b :: k) (c :: k). (Obj (M s) a, Obj (M s) b, Obj (M s) c) => M s b a -> M s c a -> M s (b ⊕ c) a Source # | |
Ring s => CoCartesian ((⊕) :: Type -> Type -> Type) (Zero :: Type) (Rel s :: Type -> Type -> Type) Source # | |
Defined in Algebra.Category.Relation inl :: forall (a :: k) (b :: k). O2 (Rel s) a b => Rel s a (a ⊕ b) Source # inr :: forall (a :: k) (b :: k). O2 (Rel s) a b => Rel s b (a ⊕ b) Source # new :: forall (a :: k). Obj (Rel s) a => Rel s Zero a Source # jam :: forall (a :: k). Obj (Rel s) a => Rel s (a ⊕ a) a Source # (▿) :: forall (a :: k) (b :: k) (c :: k). (Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) => Rel s b a -> Rel s c a -> Rel s (b ⊕ c) a Source # | |
Ring s => CoCartesian ((⊗) :: Type -> Type -> Type) (One :: Type) (Rel s :: Type -> Type -> Type) Source # | |
Defined in Algebra.Category.Relation inl :: forall (a :: k) (b :: k). O2 (Rel s) a b => Rel s a (a ⊗ b) Source # inr :: forall (a :: k) (b :: k). O2 (Rel s) a b => Rel s b (a ⊗ b) Source # new :: forall (a :: k). Obj (Rel s) a => Rel s One a Source # jam :: forall (a :: k). Obj (Rel s) a => Rel s (a ⊗ a) a Source # (▿) :: forall (a :: k) (b :: k) (c :: k). (Obj (Rel s) a, Obj (Rel s) b, Obj (Rel s) c) => Rel s b a -> Rel s c a -> Rel s (b ⊗ c) a Source # | |
CoCartesian ((⊕) :: Type -> Type -> Type) (Zero :: Type) (->) Source # | |
Defined in Algebra.Category inl :: forall (a :: k) (b :: k). O2 (->) a b => a -> (a ⊕ b) Source # inr :: forall (a :: k) (b :: k). O2 (->) a b => b -> (a ⊕ b) Source # new :: forall (a :: k). Obj (->) a => Zero -> a Source # jam :: forall (a :: k). Obj (->) a => (a ⊕ a) -> a Source # (▿) :: forall (a :: k) (b :: k) (c :: k). (Obj (->) a, Obj (->) b, Obj (->) c) => (b -> a) -> (c -> a) -> (b ⊕ c) -> a Source # | |
Ring s => CoCartesian ((⊗) :: (Type -> Type) -> (Type -> Type) -> Type -> Type) (One :: Type -> Type) (Mat s :: (Type -> Type) -> (Type -> Type) -> Type) Source # | |
Defined in Algebra.Linear inl :: forall (a :: k) (b :: k). O2 (Mat s) a b => Mat s a (a ⊗ b) Source # inr :: forall (a :: k) (b :: k). O2 (Mat s) a b => Mat s b (a ⊗ b) Source # new :: forall (a :: k). Obj (Mat s) a => Mat s One a Source # jam :: forall (a :: k). Obj (Mat s) a => Mat s (a ⊗ a) a Source # (▿) :: forall (a :: k) (b :: k) (c :: k). (Obj (Mat s) a, Obj (Mat s) b, Obj (Mat s) c) => Mat s b a -> Mat s c a -> Mat s (b ⊗ c) a Source # |
type BiCartesian x i cat = (Cartesian x i cat, CoCartesian x i cat) Source #
class Monoidal x i cat => Autonomous x i l r cat | x -> l, x -> r where Source #
Instances
(con ~ Obj k2, Con' x con, UnCon r con, UnCon l con, con i, Autonomous x i r l k2, Braided x i k2) => Autonomous (x :: k1 -> k1 -> k1) (i :: k1) (l :: k1 -> k1) (r :: k1 -> k1) (Op k2 :: k1 -> k1 -> Type) Source # | |
Ring s => Autonomous ((⊗) :: Type -> Type -> Type) (One :: Type) (Dual :: Type -> Type) (Dual :: Type -> Type) (Rel s :: Type -> Type -> Type) Source # | |
class (Symmetric x i cat, Autonomous x i d d cat) => Compact x i d cat Source #
Instances
(con ~ Obj k2, Con' x con, UnCon d con, con i, Compact x i d k2, Braided x i k2) => Compact (x :: k1 -> k1 -> k1) (i :: k1) (d :: k1 -> k1) (Op k2 :: k1 -> k1 -> Type) Source # | |
Defined in Algebra.Category.Op | |
Ring s => Compact ((⊗) :: Type -> Type -> Type) (One :: Type) (Dual :: Type -> Type) (Rel s :: Type -> Type -> Type) Source # | |
Defined in Algebra.Category.Relation |