Safe Haskell	Safe-Inferred
Language	Haskell2010

ConCat.Category

Description

Another go at constrained categories. This time without Prod, Coprod, Exp.

Synopsis

data U2 a b = U2
data (p :**: q) a b = (p a b) :**: (q a b)
prod :: (p a b :* q a b) -> (p :**: q) a b
unProd :: (p :**: q) a b -> p a b :* q a b
exl2 :: (p :**: q) a b -> p a b
exr2 :: (p :**: q) a b -> q a b
newtype Monoid2 m a b = Monoid2 m
class HasCon a where
- type Con a :: Constraint
- toDict :: a -> Dict (Con a)
- unDict :: Con a => a
newtype Sat kon a = Sat (Dict (kon a))
newtype a |- b = Entail (Con a :- Con b)
(<+) :: Con a => (Con b => r) -> (a |- b) -> r
type (&&) = (:*)
class OpCon op con where
- inOp :: (con a && con b) |- con (a `op` b)
yes1 :: c |- Sat Yes1 a
forkCon :: forall con con' a. Sat (con &+& con') a |- (Sat con a :* Sat con' a)
joinCon :: forall con con' a. (Sat con a :* Sat con' a) |- Sat (con &+& con') a
inForkCon :: ((Sat con1 a :* Sat con2 a) |- (Sat con1' b :* Sat con2' b)) -> Sat (con1 &+& con2) a |- Sat (con1' &+& con2') b
type Yes1' = Sat Yes1
type Ok' k = Sat (Ok k)
type OpSat op kon = OpCon op (Sat kon)
inSat :: OpCon op (Sat con) => (Sat con a && Sat con b) |- Sat con (a `op` b)
inOpL :: OpCon op con => ((con a && con b) && con c) |- con ((a `op` b) `op` c)
inOpR :: OpCon op con => (con a && (con b && con c)) |- con (a `op` (b `op` c))
inOpL' :: OpCon op con => ((con a && con b) && con c) |- (con (a `op` b) && con ((a `op` b) `op` c))
inOpR' :: OpCon op con => (con a && (con b && con c)) |- (con (a `op` (b `op` c)) && con (b `op` c))
inOpLR :: forall op con a b c. OpCon op con => (((con a && con b) && con c) && (con a && (con b && con c))) |- (con ((a `op` b) `op` c) && con (a `op` (b `op` c)))
class OkAdd k where
- okAdd :: Ok' k a |- Sat Additive a
type Ok2 k a b = C2 (Ok k) a b
type Ok3 k a b c = C3 (Ok k) a b c
type Ok4 k a b c d = C4 (Ok k) a b c d
type Ok5 k a b c d e = C5 (Ok k) a b c d e
type Ok6 k a b c d e f = C6 (Ok k) a b c d e f
type Oks k as = AllC (Ok k) as
class Show2 k where
- show2 :: (a `k` b) -> String
class Category k where
- type Ok k :: Type -> Constraint
- id :: Ok k a => a `k` a
- (.) :: forall b c a. Ok3 k a b c => (b `k` c) -> (a `k` b) -> a `k` c
(<~) :: (Category k, Oks k [a, b, a', b']) => (b `k` b') -> (a' `k` a) -> (a `k` b) -> a' `k` b'
(~>) :: (Category k, Oks k [a, b, a', b']) => (a' `k` a) -> (b `k` b') -> (a `k` b) -> a' `k` b'
type Prod k = (:*)
type OkProd k = OpCon (Prod k) (Ok' k)
okProd :: forall k a b. OkProd k => (Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
class (Category k, OkProd k) => AssociativePCat k where
- lassocP :: forall a b c. Ok3 k a b c => Prod k a (Prod k b c) `k` Prod k (Prod k a b) c
- rassocP :: forall a b c. Ok3 k a b c => Prod k (Prod k a b) c `k` Prod k a (Prod k b c)
class (Category k, OkProd k) => MonoidalPCat k where
- (***) :: forall a b c d. Ok4 k a b c d => (a `k` c) -> (b `k` d) -> Prod k a b `k` Prod k c d
- first :: forall a a' b. Ok3 k a b a' => (a `k` a') -> Prod k a b `k` Prod k a' b
- second :: forall a b b'. Ok3 k a b b' => (b `k` b') -> Prod k a b `k` Prod k a b'
class (Category k, OkProd k) => BraidedPCat k where
- swapP :: forall a b. Ok2 k a b => Prod k a b `k` Prod k b a
type MBraidedPCat k = (BraidedPCat k, MonoidalPCat k)
class (Category k, OkProd k) => ProductCat k where
- exl :: Ok2 k a b => Prod k a b `k` a
- exr :: Ok2 k a b => Prod k a b `k` b
- dup :: Ok k a => a `k` Prod k a a
(&&&) :: forall k a c d. (MProductCat k, Ok3 k a c d) => (a `k` c) -> (a `k` d) -> a `k` Prod k c d
type MProductCat k = (ProductCat k, MonoidalPCat k)
type Coprod k = (:+)
type OkCoprod k = OpCon (Coprod k) (Ok' k)
okCoprod :: forall k a b. OkCoprod k => (Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
class (Category k, OkCoprod k) => AssociativeSCat k where
- lassocS :: forall a b c. Oks k [a, b, c] => Coprod k a (Coprod k b c) `k` Coprod k (Coprod k a b) c
- rassocS :: forall a b c. Oks k [a, b, c] => Coprod k (Coprod k a b) c `k` Coprod k a (Coprod k b c)
class (Category k, OkCoprod k) => BraidedSCat k where
- swapS :: forall a b. Ok2 k a b => Coprod k a b `k` Coprod k b a
class (OkCoprod k, Category k) => MonoidalSCat k where
- (+++) :: forall a b c d. Ok4 k a b c d => (c `k` a) -> (d `k` b) -> Coprod k c d `k` Coprod k a b
- left :: forall a a' b. Oks k [a, b, a'] => (a `k` a') -> Coprod k a b `k` Coprod k a' b
- right :: forall a b b'. Oks k [a, b, b'] => (b `k` b') -> Coprod k a b `k` Coprod k a b'
class (Category k, OkCoprod k) => CoproductCat k where
- inl :: Ok2 k a b => a `k` Coprod k a b
- inr :: Ok2 k a b => b `k` Coprod k a b
- jam :: Ok k a => Coprod k a a `k` a
type MCoproductCat k = (CoproductCat k, MonoidalSCat k)
(|||) :: forall k a c d. (MCoproductCat k, Ok3 k a c d) => (c `k` a) -> (d `k` a) -> Coprod k c d `k` a
type AbelianCat k = (MProductCat k, CoproductPCat k, TerminalCat k, CoterminalCat k, OkAdd k)
zeroC :: (AbelianCat k, Ok2 k a b) => a `k` b
plusC :: forall k a b. (AbelianCat k, Ok2 k a b) => Binop (a `k` b)
type CoprodP k = Prod k
type OkCoprodP k = OkProd k
okCoprodP :: forall k a b. OkCoprodP k => (Ok' k a && Ok' k b) |- Ok' k (CoprodP k a b)
class BraidedPCat k => CoproductPCat k where
- inlP :: Ok2 k a b => a `k` CoprodP k a b
- inrP :: Ok2 k a b => b `k` CoprodP k a b
- jamP :: Ok k a => CoprodP k a a `k` a
type MCoproductPCat k = (CoproductPCat k, MonoidalPCat k)
(||||) :: forall k a c d. (MCoproductPCat k, Ok3 k a c d) => (c `k` a) -> (d `k` a) -> CoprodP k c d `k` a
class ScalarCat k a where
- scale :: a -> a `k` a
type LinearCat k a = (MProductCat k, CoproductPCat k, ScalarCat k a, Ok k a)
class DistribCat k where
- distl :: forall a u v. Ok3 k a u v => Prod k a (Coprod k u v) `k` Coprod k (Prod k a u) (Prod k a v)
- distr :: forall u v b. Ok3 k u v b => Prod k (Coprod k u v) b `k` Coprod k (Prod k u b) (Prod k v b)
type OkExp k = OpCon (Exp k) (Ok' k)
okExp :: forall k a b. OkExp k => (Ok' k a && Ok' k b) |- Ok' k (Exp k a b)
type Exp k = (->)
class (OkExp k, ProductCat k) => ClosedCat k where
- apply :: forall a b. Ok2 k a b => Prod k (Exp k a b) a `k` b
- curry :: Ok3 k a b c => (Prod k a b `k` c) -> a `k` Exp k b c
- uncurry :: forall a b c. Ok3 k a b c => (a `k` Exp k b c) -> Prod k a b `k` c
applyK :: Kleisli m (Kleisli m a b :* a) b
curryK :: Monad m => Kleisli m (a :* b) c -> Kleisli m a (Kleisli m b c)
uncurryK :: Monad m => Kleisli m a (Kleisli m b c) -> Kleisli m (a :* b) c
class OkExp k => FlipCat k where
- flipC :: Ok3 k a b c => (a `k` (b -> c)) -> b -> a `k` c
- flipC' :: Ok3 k a b c => (b -> a `k` c) -> a `k` (b -> c)
type Unit k = ()
type OkUnit k = Ok k (Unit k)
class OkUnit k => TerminalCat k where
- it :: Ok k a => a `k` Unit k
class OkUnit k => UnitCat k where
- lunit :: Ok k a => a `k` Prod k (Unit k) a
- lcounit :: Ok k a => Prod k (Unit k) a `k` a
- runit :: Ok k a => a `k` Prod k a (Unit k)
- rcounit :: Ok k a => Prod k a (Unit k) `k` a
type Counit k = ()
class Ok k (Counit k) => CoterminalCat k where
- ti :: Ok k a => Counit k `k` a
constFun :: forall k p a b. (ClosedCat k, Ok3 k p a b) => (a `k` b) -> p `k` Exp k a b
constFun2 :: forall k p a b c. (ClosedCat k, Oks k [p, a, b, c]) => (Prod k a b `k` c) -> p `k` Exp k a (Exp k b c)
unitFun :: forall k a b. (ClosedCat k, TerminalCat k, Ok2 k a b) => (a `k` b) -> Unit k `k` Exp k a b
unUnitFun :: forall k p a. (ClosedCat k, MonoidalPCat k, TerminalCat k, Oks k [p, a]) => (Unit k `k` Exp k p a) -> p `k` a
type ConstObj k b = b
class (Category k, Ok k (ConstObj k b)) => ConstCat k b where
- const :: Ok k a => b -> a `k` ConstObj k b
- unitArrow :: OkUnit k => b -> Unit k `k` ConstObj k b
repConst :: (HasRep b, r ~ Rep b, RepCat k b (ConstObj k r), ConstCat k r, Ok k a, Ok k (ConstObj k b)) => b -> a `k` ConstObj k b
pairConst :: (MProductCat k, ConstCat k b, ConstCat k c, Ok k a) => (b :* c) -> a `k` (b :* c)
lconst :: forall k a b. (MProductCat k, ConstCat k a, Ok2 k a b) => a -> b `k` (a :* b)
rconst :: forall k a b. (MProductCat k, ConstCat k b, Ok2 k a b) => b -> a `k` (a :* b)
class DelayCat k where
- delay :: Ok k a => a -> a `k` a
class ProductCat k => LoopCat k where
- loop :: Ok3 k s a b => ((a :* s) `k` (b :* s)) -> a `k` b
class ProductCat k => TracedCat k where
- trace :: Ok3 k a b c => ((a :* c) `k` (b :* c)) -> a `k` b
type BiCCC k = (ClosedCat k, CoproductCat k, TerminalCat k, DistribCat k)
data Constrained (con :: Type -> Constraint) k a b = Constrained (a `k` b)
type BoolOf k = Bool
class (ProductCat k, Ok k (BoolOf k)) => BoolCat k where
- notC :: BoolOf k `k` BoolOf k
- andC, orC, xorC :: Prod k (BoolOf k) (BoolOf k) `k` BoolOf k
okTT :: forall k a. OkProd k => Ok' k a |- Ok' k (Prod k a a)
class (BoolCat k, Ok k a) => EqCat k a where
- equal, notEqual :: Prod k a a `k` BoolOf k
class (EqCat k a, Ord a) => OrdCat k a where
- lessThan, greaterThan, lessThanOrEqual, greaterThanOrEqual :: Prod k a a `k` BoolOf k
class Ok k a => MinMaxCat k a where
- minC, maxC :: Prod k a a `k` a
class (Category k, Ok k a) => EnumCat k a where
- succC, predC :: a `k` a
class Ok k a => NumCat k a where
- negateC :: a `k` a
- addC, subC, mulC :: Prod k a a `k` a
- powIC :: Ok k Int => Prod k a Int `k` a
class Ok k a => IntegralCat k a where
- divC :: Prod k a a `k` a
- modC :: Prod k a a `k` a
divModC :: forall k a. (MProductCat k, IntegralCat k a, Ok k a) => Prod k a a `k` Prod k a a
class Ok k a => FractionalCat k a where
- recipC :: a `k` a
- divideC :: Prod k a a `k` a
class Ok k a => FloatingCat k a where
- expC, logC, cosC, sinC, sqrtC, tanhC :: a `k` a
class Ok k a => RealFracCat k a b where
- floorC, ceilingC :: a `k` b
- truncateC :: a `k` b
class FromIntegralCat k a b where
- fromIntegralC :: a `k` b
- foo_FromIntegralCat :: ()
class BottomCat k a b where
- bottomC :: a `k` b
type IfT k a = Prod k (BoolOf k) (Prod k a a) `k` a
class (BoolCat k, Ok k a) => IfCat k a where
- ifC :: IfT k a
class UnknownCat k a b where
- unknownC :: a `k` b
class RepCat k a r where
- reprC :: a `k` r
- abstC :: r `k` a
class TransitiveCon con where
- trans :: (con a b, con b c) :- con a c
class CoerceCat k a b where
- coerceC :: a `k` b
class OkFunctor k h where
- okFunctor :: Ok' k a |- Ok' k (h a)
class OkFunctor k h => FunctorCat k h where
- fmapC :: Ok2 k a b => (a `k` b) -> h a `k` h b
- unzipC :: forall a b. Ok2 k a b => h (a :* b) `k` (h a :* h b)
class (Zip h, OkFunctor k h) => ZipCat k h where
- zipC :: Ok2 k a b => (h a :* h b) `k` h (a :* b)
class OkFunctor k h => ZapCat k h where
- zapC :: Ok2 k a b => h (a `k` b) -> h a `k` h b
class (OkFunctor k h, Ok k a) => PointedCat k h a where
- pointC :: a `k` h a
class Ok k a => AddCat k h a where
- sumAC :: h a `k` a
class TraversableCat k t f where
- sequenceAC :: Ok k a => t (f a) `k` f (t a)
class DistributiveCat k g f where
- distributeC :: Ok k a => f (g a) `k` g (f a)
class RepresentableCat k f where
- tabulateC :: Ok k a => (Rep f -> a) `k` f a
- indexC :: Ok k a => f a `k` (Rep f -> a)
fmap' :: Functor f => (a -> b) -> f a -> f b
liftA2' :: Applicative f => (a -> b -> c) -> f a -> f b -> f c
zipWith' :: Zip f => (a -> b -> c) -> f a -> f b -> f c
class FunctorCat k h => Strong k h where
- strength :: Ok2 k a b => (a :* h b) `k` h (a :* b)
class OkIxProd k h where
- okIxProd :: Ok' k a |- Ok' k (h a)
class (Category k, OkIxProd k h) => IxMonoidalPCat k h where
- crossF :: forall a b. Ok2 k a b => h (a `k` b) -> h a `k` h b
class IxMonoidalPCat k h => IxProductCat k h where
- exF :: forall a. Ok k a => h (h a `k` a)
- forkF :: forall a b. Ok2 k a b => h (a `k` b) -> a `k` h b
- replF :: forall a. Ok k a => a `k` h a
class (OkFunctor k h, Ok k a) => MinMaxFunctorCat k h a where
- minimumC :: h a `k` a
- maximumC :: h a `k` a
class (OkFunctor k h, Ok k a) => MinMaxFFunctorCat k h a where
- minimumCF :: h a -> a :* (h a `k` a)
- maximumCF :: h a -> a :* (h a `k` a)
class Additive1 h where
- additive1 :: Sat Additive a |- Sat Additive (h a)
class (IxMonoidalPCat k h, OkIxProd k h) => IxCoproductPCat k h where
- inPF :: forall a. Ok k a => h (a `k` h a)
- joinPF :: forall a b. Ok2 k a b => h (b `k` a) -> h b `k` a
- jamPF :: forall a. Ok k a => h a `k` a
class FiniteCat k where
- unFinite :: KnownNat n => Finite n `k` Int
- unsafeFinite :: KnownNat n => Int `k` Finite n

Documentation

data U2 a b Source #

Constructors

U2

Instances

Instances details

BottomCat (U2 :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods bottomC :: U2 a b Source #
CoerceCat (U2 :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods coerceC :: U2 a b Source #
FromIntegralCat (U2 :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods fromIntegralC :: U2 a b Source # foo_FromIntegralCat :: () Source #
UnknownCat (U2 :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods unknownC :: U2 a b Source #
r ~ Rep a => RepCat (U2 :: Type -> Type -> Type) (a :: Type) (r :: Type) Source #
Instance details Defined in ConCat.Category Methods reprC :: U2 a r Source # abstC :: U2 r a Source #
BoolCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods notC :: U2 (BoolOf U2) (BoolOf U2) Source # andC :: U2 (Prod U2 (BoolOf U2) (BoolOf U2)) (BoolOf U2) Source # orC :: U2 (Prod U2 (BoolOf U2) (BoolOf U2)) (BoolOf U2) Source # xorC :: U2 (Prod U2 (BoolOf U2) (BoolOf U2)) (BoolOf U2) Source #
BraidedPCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods swapP :: Ok2 U2 a b => U2 (Prod U2 a b) (Prod U2 b a) Source #
BraidedSCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods swapS :: Ok2 U2 a b => U2 (Coprod U2 a b) (Coprod U2 b a) Source #
Category (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Associated Types type Ok U2 :: Type -> Constraint Source # Methods id :: Ok U2 a => U2 a a Source # (.) :: forall b c a. Ok3 U2 a b c => U2 b c -> U2 a b -> U2 a c Source #
ClosedCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods apply :: Ok2 U2 a b => U2 (Prod U2 (Exp U2 a b) a) b Source # curry :: Ok3 U2 a b c => U2 (Prod U2 a b) c -> U2 a (Exp U2 b c) Source # uncurry :: Ok3 U2 a b c => U2 a (Exp U2 b c) -> U2 (Prod U2 a b) c Source #
CoproductCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods inl :: Ok2 U2 a b => U2 a (Coprod U2 a b) Source # inr :: Ok2 U2 a b => U2 b (Coprod U2 a b) Source # jam :: Ok U2 a => U2 (Coprod U2 a a) a Source #
CoproductPCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods inlP :: Ok2 U2 a b => U2 a (CoprodP U2 a b) Source # inrP :: Ok2 U2 a b => U2 b (CoprodP U2 a b) Source # jamP :: Ok U2 a => U2 (CoprodP U2 a a) a Source #
CoterminalCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods ti :: Ok U2 a => U2 (Counit U2) a Source #
DistribCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods distl :: Ok3 U2 a u v => U2 (Prod U2 a (Coprod U2 u v)) (Coprod U2 (Prod U2 a u) (Prod U2 a v)) Source # distr :: Ok3 U2 u v b => U2 (Prod U2 (Coprod U2 u v) b) (Coprod U2 (Prod U2 u b) (Prod U2 v b)) Source #
FlipCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods flipC :: Ok3 U2 a b c => U2 a (b -> c) -> b -> U2 a c Source # flipC' :: Ok3 U2 a b c => (b -> U2 a c) -> U2 a (b -> c) Source #
MonoidalPCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods (***) :: Ok4 U2 a b c d => U2 a c -> U2 b d -> U2 (Prod U2 a b) (Prod U2 c d) Source # first :: forall a a' b. Ok3 U2 a b a' => U2 a a' -> U2 (Prod U2 a b) (Prod U2 a' b) Source # second :: Ok3 U2 a b b' => U2 b b' -> U2 (Prod U2 a b) (Prod U2 a b') Source #
MonoidalSCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods (+++) :: Ok4 U2 a b c d => U2 c a -> U2 d b -> U2 (Coprod U2 c d) (Coprod U2 a b) Source # left :: forall a a' b. Oks U2 '[a, b, a'] => U2 a a' -> U2 (Coprod U2 a b) (Coprod U2 a' b) Source # right :: Oks U2 '[a, b, b'] => U2 b b' -> U2 (Coprod U2 a b) (Coprod U2 a b') Source #
ProductCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods exl :: Ok2 U2 a b => U2 (Prod U2 a b) a Source # exr :: Ok2 U2 a b => U2 (Prod U2 a b) b Source # dup :: Ok U2 a => U2 a (Prod U2 a a) Source #
TerminalCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods it :: Ok U2 a => U2 a (Unit U2) Source #
TracedCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods trace :: Ok3 U2 a b c => U2 (a :* c) (b :* c) -> U2 a b Source #
UnitCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods lunit :: Ok U2 a => U2 a (Prod U2 (Unit U2) a) Source # lcounit :: Ok U2 a => U2 (Prod U2 (Unit U2) a) a Source # runit :: Ok U2 a => U2 a (Prod U2 a (Unit U2)) Source # rcounit :: Ok U2 a => U2 (Prod U2 a (Unit U2)) a Source #
ConstCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods const :: Ok U2 a0 => a -> U2 a0 (ConstObj U2 a) Source # unitArrow :: a -> U2 (Unit U2) (ConstObj U2 a) Source #
EnumCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods succC :: U2 a a Source # predC :: U2 a a Source #
EqCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods equal :: U2 (Prod U2 a a) (BoolOf U2) Source # notEqual :: U2 (Prod U2 a a) (BoolOf U2) Source #
FloatingCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods expC :: U2 a a Source # logC :: U2 a a Source # cosC :: U2 a a Source # sinC :: U2 a a Source # sqrtC :: U2 a a Source # tanhC :: U2 a a Source #
FractionalCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods recipC :: U2 a a Source # divideC :: U2 (Prod U2 a a) a Source #
IfCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods ifC :: IfT U2 a Source #
IntegralCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods divC :: U2 (Prod U2 a a) a Source # modC :: U2 (Prod U2 a a) a Source #
Pointed h => IxCoproductPCat (U2 :: Type -> Type -> Type) h Source #
Instance details Defined in ConCat.Category Methods inPF :: Ok U2 a => h (U2 a (h a)) Source # joinPF :: Ok2 U2 a b => h (U2 b a) -> U2 (h b) a Source # jamPF :: Ok U2 a => U2 (h a) a Source #
IxMonoidalPCat (U2 :: Type -> Type -> Type) h Source #
Instance details Defined in ConCat.Category Methods crossF :: Ok2 U2 a b => h (U2 a b) -> U2 (h a) (h b) Source #
Pointed h => IxProductCat (U2 :: Type -> Type -> Type) h Source #
Instance details Defined in ConCat.Category Methods exF :: Ok U2 a => h (U2 (h a) a) Source # forkF :: Ok2 U2 a b => h (U2 a b) -> U2 a (h b) Source # replF :: Ok U2 a => U2 a (h a) Source #
MinMaxCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods minC :: U2 (Prod U2 a a) a Source # maxC :: U2 (Prod U2 a a) a Source #
NumCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods negateC :: U2 a a Source # addC :: U2 (Prod U2 a a) a Source # subC :: U2 (Prod U2 a a) a Source # mulC :: U2 (Prod U2 a a) a Source # powIC :: U2 (Prod U2 a Int) a Source #
OkIxProd (U2 :: Type -> Type -> Type) h Source #
Instance details Defined in ConCat.Category Methods okIxProd :: Ok' U2 a \|- Ok' U2 (h a) Source #
Ord a => OrdCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods lessThan :: U2 (Prod U2 a a) (BoolOf U2) Source # greaterThan :: U2 (Prod U2 a a) (BoolOf U2) Source # lessThanOrEqual :: U2 (Prod U2 a a) (BoolOf U2) Source # greaterThanOrEqual :: U2 (Prod U2 a a) (BoolOf U2) Source #
ScalarCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods scale :: a -> U2 a a Source #
Integral b => RealFracCat (U2 :: Type -> Type -> Type) a b Source #
Instance details Defined in ConCat.Category Methods floorC :: U2 a b Source # ceilingC :: U2 a b Source # truncateC :: U2 a b Source #
Show (U2 a b) Source #
Instance details Defined in ConCat.Category Methods showsPrec :: Int -> U2 a b -> ShowS Source # show :: U2 a b -> String Source # showList :: [U2 a b] -> ShowS Source #
type Ok (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category type Ok (U2 :: Type -> Type -> Type) = Yes1 :: Type -> Constraint

data (p :**: q) a b infixr 7 Source #

Product for binary type constructors

Constructors

(p a b) :**: (q a b) infixr 7

Instances

Instances details

(BottomCat k3 a b, BottomCat k' a b) => BottomCat (k3 :**: k' :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods bottomC :: (k3 :**: k') a b Source #
(CoerceCat k3 a b, CoerceCat k' a b) => CoerceCat (k3 :**: k' :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods coerceC :: (k3 :**: k') a b Source #
(FromIntegralCat k3 a b, FromIntegralCat k' a b) => FromIntegralCat (k3 :**: k' :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods fromIntegralC :: (k3 :**: k') a b Source # foo_FromIntegralCat :: () Source #
(UnknownCat k3 a b, UnknownCat k' a b) => UnknownCat (k3 :**: k' :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods unknownC :: (k3 :**: k') a b Source #
(RepCat k2 a b, RepCat k' a b) => RepCat (k2 :**: k' :: k1 -> k1 -> Type) (a :: k1) (b :: k1) Source #
Instance details Defined in ConCat.Category Methods reprC :: (k2 :: k') a b Source # abstC :: (k2 :: k') b a Source #
(AssociativePCat k, AssociativePCat k') => AssociativePCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods lassocP :: Ok3 (k :: k') a b c => (k :: k') (Prod (k :: k') a (Prod (k :: k') b c)) (Prod (k :: k') (Prod (k :: k') a b) c) Source # rassocP :: Ok3 (k :: k') a b c => (k :: k') (Prod (k :: k') (Prod (k :: k') a b) c) (Prod (k :: k') a (Prod (k :: k') b c)) Source #
(AssociativeSCat k, AssociativeSCat k') => AssociativeSCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods lassocS :: Oks (k :: k') '[a, b, c] => (k :: k') (Coprod (k :: k') a (Coprod (k :: k') b c)) (Coprod (k :: k') (Coprod (k :: k') a b) c) Source # rassocS :: Oks (k :: k') '[a, b, c] => (k :: k') (Coprod (k :: k') (Coprod (k :: k') a b) c) (Coprod (k :: k') a (Coprod (k :: k') b c)) Source #
(BoolCat k, BoolCat k') => BoolCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods notC :: (k :: k') (BoolOf (k :: k')) (BoolOf (k :: k')) Source # andC :: (k :: k') (Prod (k :: k') (BoolOf (k :: k')) (BoolOf (k :: k'))) (BoolOf (k :: k')) Source # orC :: (k :: k') (Prod (k :: k') (BoolOf (k :: k')) (BoolOf (k :: k'))) (BoolOf (k :: k')) Source # xorC :: (k :: k') (Prod (k :: k') (BoolOf (k :: k')) (BoolOf (k :: k'))) (BoolOf (k :: k')) Source #
(BraidedPCat k, BraidedPCat k') => BraidedPCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods swapP :: Ok2 (k :: k') a b => (k :: k') (Prod (k :: k') a b) (Prod (k :: k') b a) Source #
(BraidedSCat k, BraidedSCat k') => BraidedSCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods swapS :: Ok2 (k :: k') a b => (k :: k') (Coprod (k :: k') a b) (Coprod (k :: k') b a) Source #
(Category k, Category k') => Category (k :**: k') Source #
Instance details Defined in ConCat.Category Associated Types type Ok (k :: k') :: Type -> Constraint Source # Methods id :: Ok (k :: k') a => (k :: k') a a Source # (.) :: forall b c a. Ok3 (k :: k') a b c => (k :: k') b c -> (k :: k') a b -> (k :**: k') a c Source #
(ClosedCat k, ClosedCat k') => ClosedCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods apply :: Ok2 (k :: k') a b => (k :: k') (Prod (k :: k') (Exp (k :: k') a b) a) b Source # curry :: Ok3 (k :: k') a b c => (k :: k') (Prod (k :: k') a b) c -> (k :: k') a (Exp (k :: k') b c) Source # uncurry :: Ok3 (k :: k') a b c => (k :: k') a (Exp (k :: k') b c) -> (k :: k') (Prod (k :: k') a b) c Source #
(CoproductCat k, CoproductCat k') => CoproductCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods inl :: Ok2 (k :: k') a b => (k :: k') a (Coprod (k :: k') a b) Source # inr :: Ok2 (k :: k') a b => (k :: k') b (Coprod (k :: k') a b) Source # jam :: Ok (k :: k') a => (k :: k') (Coprod (k :**: k') a a) a Source #
(CoproductPCat k, CoproductPCat k') => CoproductPCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods inlP :: Ok2 (k :: k') a b => (k :: k') a (CoprodP (k :: k') a b) Source # inrP :: Ok2 (k :: k') a b => (k :: k') b (CoprodP (k :: k') a b) Source # jamP :: Ok (k :: k') a => (k :: k') (CoprodP (k :**: k') a a) a Source #
(CoterminalCat k, CoterminalCat k') => CoterminalCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods ti :: Ok (k :: k') a => (k :: k') (Counit (k :**: k')) a Source #
(DistribCat k, DistribCat k') => DistribCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods distl :: Ok3 (k :: k') a u v => (k :: k') (Prod (k :: k') a (Coprod (k :: k') u v)) (Coprod (k :: k') (Prod (k :: k') a u) (Prod (k :: k') a v)) Source # distr :: Ok3 (k :: k') u v b => (k :: k') (Prod (k :: k') (Coprod (k :: k') u v) b) (Coprod (k :: k') (Prod (k :: k') u b) (Prod (k :: k') v b)) Source #
(FiniteCat k, FiniteCat k') => FiniteCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods unFinite :: forall (n :: Nat). KnownNat n => (k :: k') (Finite n) Int Source # unsafeFinite :: forall (n :: Nat). KnownNat n => (k :: k') Int (Finite n) Source #
(FlipCat k, FlipCat k') => FlipCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods flipC :: Ok3 (k :: k') a b c => (k :: k') a (b -> c) -> b -> (k :: k') a c Source # flipC' :: Ok3 (k :: k') a b c => (b -> (k :: k') a c) -> (k :: k') a (b -> c) Source #
(MonoidalPCat k, MonoidalPCat k') => MonoidalPCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods (*) :: Ok4 (k :: k') a b c d => (k :: k') a c -> (k :: k') b d -> (k :: k') (Prod (k :: k') a b) (Prod (k :: k') c d) Source # first :: forall a a' b. Ok3 (k :: k') a b a' => (k :: k') a a' -> (k :: k') (Prod (k :: k') a b) (Prod (k :: k') a' b) Source # second :: Ok3 (k :: k') a b b' => (k :: k') b b' -> (k :: k') (Prod (k :: k') a b) (Prod (k :**: k') a b') Source #
(MonoidalSCat k, MonoidalSCat k') => MonoidalSCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods (+++) :: Ok4 (k :: k') a b c d => (k :: k') c a -> (k :: k') d b -> (k :: k') (Coprod (k :: k') c d) (Coprod (k :: k') a b) Source # left :: forall a a' b. Oks (k :: k') '[a, b, a'] => (k :: k') a a' -> (k :: k') (Coprod (k :: k') a b) (Coprod (k :: k') a' b) Source # right :: Oks (k :: k') '[a, b, b'] => (k :: k') b b' -> (k :: k') (Coprod (k :: k') a b) (Coprod (k :: k') a b') Source #
(ProductCat k, ProductCat k') => ProductCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods exl :: Ok2 (k :: k') a b => (k :: k') (Prod (k :: k') a b) a Source # exr :: Ok2 (k :: k') a b => (k :: k') (Prod (k :: k') a b) b Source # dup :: Ok (k :: k') a => (k :: k') a (Prod (k :**: k') a a) Source #
(TerminalCat k, TerminalCat k') => TerminalCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods it :: Ok (k :: k') a => (k :: k') a (Unit (k :**: k')) Source #
(TracedCat k, TracedCat k') => TracedCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods trace :: Ok3 (k :: k') a b c => (k :: k') (a :* c) (b :* c) -> (k :**: k') a b Source #
(UnitCat k, UnitCat k') => UnitCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods lunit :: Ok (k :: k') a => (k :: k') a (Prod (k :: k') (Unit (k :: k')) a) Source # lcounit :: Ok (k :: k') a => (k :: k') (Prod (k :: k') (Unit (k :: k')) a) a Source # runit :: Ok (k :: k') a => (k :: k') a (Prod (k :: k') a (Unit (k :: k'))) Source # rcounit :: Ok (k :: k') a => (k :: k') (Prod (k :: k') a (Unit (k :: k'))) a Source #
(ConstCat k a, ConstCat k' a) => ConstCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods const :: Ok (k :: k') a0 => a -> (k :: k') a0 (ConstObj (k :: k') a) Source # unitArrow :: a -> (k :: k') (Unit (k :: k')) (ConstObj (k :: k') a) Source #
(EnumCat k a, EnumCat k' a) => EnumCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods succC :: (k :: k') a a Source # predC :: (k :: k') a a Source #
(EqCat k a, EqCat k' a) => EqCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods equal :: (k :: k') (Prod (k :: k') a a) (BoolOf (k :: k')) Source # notEqual :: (k :: k') (Prod (k :: k') a a) (BoolOf (k :: k')) Source #
(FloatingCat k a, FloatingCat k' a) => FloatingCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods expC :: (k :: k') a a Source # logC :: (k :: k') a a Source # cosC :: (k :: k') a a Source # sinC :: (k :: k') a a Source # sqrtC :: (k :: k') a a Source # tanhC :: (k :: k') a a Source #
(FractionalCat k a, FractionalCat k' a) => FractionalCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods recipC :: (k :: k') a a Source # divideC :: (k :: k') (Prod (k :**: k') a a) a Source #
(FunctorCat k h, FunctorCat k' h) => FunctorCat (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods fmapC :: Ok2 (k :: k') a b => (k :: k') a b -> (k :: k') (h a) (h b) Source # unzipC :: Ok2 (k :: k') a b => (k :*: k') (h (a : b)) (h a :* h b) Source #
(IfCat k a, IfCat k' a) => IfCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods ifC :: IfT (k :**: k') a Source #
(IntegralCat k a, IntegralCat k' a) => IntegralCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods divC :: (k :: k') (Prod (k :: k') a a) a Source # modC :: (k :: k') (Prod (k :: k') a a) a Source #
(IxCoproductPCat k h, IxCoproductPCat k' h, Zip h) => IxCoproductPCat (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods inPF :: Ok (k :: k') a => h ((k :: k') a (h a)) Source # joinPF :: Ok2 (k :: k') a b => h ((k :: k') b a) -> (k :: k') (h b) a Source # jamPF :: Ok (k :: k') a => (k :**: k') (h a) a Source #
(IxMonoidalPCat k h, IxMonoidalPCat k' h, Zip h) => IxMonoidalPCat (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods crossF :: Ok2 (k :: k') a b => h ((k :: k') a b) -> (k :**: k') (h a) (h b) Source #
(IxProductCat k h, IxProductCat k' h, Zip h) => IxProductCat (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods exF :: Ok (k :: k') a => h ((k :: k') (h a) a) Source # forkF :: Ok2 (k :: k') a b => h ((k :: k') a b) -> (k :: k') a (h b) Source # replF :: Ok (k :: k') a => (k :**: k') a (h a) Source #
(MinMaxCat k a, MinMaxCat k' a) => MinMaxCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods minC :: (k :: k') (Prod (k :: k') a a) a Source # maxC :: (k :: k') (Prod (k :: k') a a) a Source #
(NumCat k a, NumCat k' a) => NumCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods negateC :: (k :: k') a a Source # addC :: (k :: k') (Prod (k :: k') a a) a Source # subC :: (k :: k') (Prod (k :: k') a a) a Source # mulC :: (k :: k') (Prod (k :: k') a a) a Source # powIC :: (k :: k') (Prod (k :**: k') a Int) a Source #
(OkFunctor k h, OkFunctor k' h) => OkFunctor (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods okFunctor :: Ok' (k :: k') a \|- Ok' (k :: k') (h a) Source #
(OkIxProd k h, OkIxProd k' h) => OkIxProd (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods okIxProd :: Ok' (k :: k') a \|- Ok' (k :: k') (h a) Source #
(OrdCat k a, OrdCat k' a) => OrdCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods lessThan :: (k :: k') (Prod (k :: k') a a) (BoolOf (k :: k')) Source # greaterThan :: (k :: k') (Prod (k :: k') a a) (BoolOf (k :: k')) Source # lessThanOrEqual :: (k :: k') (Prod (k :: k') a a) (BoolOf (k :: k')) Source # greaterThanOrEqual :: (k :: k') (Prod (k :: k') a a) (BoolOf (k :: k')) Source #
(RepresentableCat k h, RepresentableCat k' h) => RepresentableCat (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods tabulateC :: Ok (k :: k') a => (k :: k') (Rep h -> a) (h a) Source # indexC :: Ok (k :: k') a => (k :: k') (h a) (Rep h -> a) Source #
(ScalarCat k a, ScalarCat k' a) => ScalarCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods scale :: a -> (k :**: k') a a Source #
(Strong k h, Strong k' h) => Strong (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods strength :: Ok2 (k :: k') a b => (k :: k') (a :* h b) (h (a :* b)) Source #
(ZapCat k h, ZapCat k' h, Functor h) => ZapCat (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods zapC :: Ok2 (k :: k') a b => h ((k :: k') a b) -> (k :**: k') (h a) (h b) Source #
(ZipCat k h, ZipCat k' h) => ZipCat (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods zipC :: Ok2 (k :: k') a b => (k :: k') (h a :* h b) (h (a :* b)) Source #
(AddCat k h a, AddCat k' h a) => AddCat (k :**: k') h a Source #
Instance details Defined in ConCat.Category Methods sumAC :: (k :**: k') (h a) a Source #
(DistributiveCat k g f, DistributiveCat k' g f) => DistributiveCat (k :**: k') g f Source #
Instance details Defined in ConCat.Category Methods distributeC :: Ok (k :: k') a => (k :: k') (f (g a)) (g (f a)) Source #
(MinMaxFFunctorCat k h a, MinMaxFFunctorCat k' h a, Ord a) => MinMaxFFunctorCat (k :**: k') h a Source #
Instance details Defined in ConCat.Category Methods minimumCF :: h a -> a :* (k :*: k') (h a) a Source # maximumCF :: h a -> a : (k :**: k') (h a) a Source #
(MinMaxFunctorCat k h a, MinMaxFunctorCat k' h a) => MinMaxFunctorCat (k :**: k') h a Source #
Instance details Defined in ConCat.Category Methods minimumC :: (k :: k') (h a) a Source # maximumC :: (k :: k') (h a) a Source #
(PointedCat k h a, PointedCat k' h a) => PointedCat (k :**: k') h a Source #
Instance details Defined in ConCat.Category Methods pointC :: (k :**: k') a (h a) Source #
(RealFracCat k a b, RealFracCat k' a b) => RealFracCat (k :**: k') a b Source #
Instance details Defined in ConCat.Category Methods floorC :: (k :: k') a b Source # ceilingC :: (k :: k') a b Source # truncateC :: (k :**: k') a b Source #
(TraversableCat k t f, TraversableCat k' t f) => TraversableCat (k :**: k') t f Source #
Instance details Defined in ConCat.Category Methods sequenceAC :: Ok (k :: k') a => (k :: k') (t (f a)) (f (t a)) Source #
HasRep ((k3 :**: k') a b) Source #
Instance details Defined in ConCat.Category Associated Types type Rep ((k3 :: k') a b) Source # Methods repr :: (k3 :: k') a b -> Rep ((k3 :: k') a b) Source # abst :: Rep ((k3 :: k') a b) -> (k3 :**: k') a b Source #
type Ok (k :**: k') Source #
Instance details Defined in ConCat.Category type Ok (k :**: k') = Ok k &+& Ok k'
type Rep ((k3 :**: k') a b) Source #
Instance details Defined in ConCat.Category type Rep ((k3 :*: k') a b) = k3 a b : k' a b

prod :: (p a b :* q a b) -> (p :**: q) a b Source #

unProd :: (p :**: q) a b -> p a b :* q a b Source #

exl2 :: (p :**: q) a b -> p a b Source #

exr2 :: (p :**: q) a b -> q a b Source #

newtype Monoid2 m a b Source #

Constructors

Monoid2 m

Instances

Instances details

Monoid m => Category (Monoid2 m :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Associated Types type Ok (Monoid2 m) :: Type -> Constraint Source # Methods id :: Ok (Monoid2 m) a => Monoid2 m a a Source # (.) :: forall b c a. Ok3 (Monoid2 m) a b c => Monoid2 m b c -> Monoid2 m a b -> Monoid2 m a c Source #
type Ok (Monoid2 m :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category type Ok (Monoid2 m :: Type -> Type -> Type) = Yes1 :: Type -> Constraint

class HasCon a where Source #

Associated Types

type Con a :: Constraint Source #

Methods

toDict :: a -> Dict (Con a) Source #

unDict :: Con a => a Source #

Instances

Instances details

HasCon () Source #
Instance details Defined in ConCat.Category Associated Types type Con () Source # Methods toDict :: () -> Dict (Con ()) Source # unDict :: () Source #
OpCon (:*) (Sat HasCon) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat HasCon a && Sat HasCon b) \|- Sat HasCon (a :* b) Source #
(HasCon a, HasCon b) => HasCon (a :* b) Source #
Instance details Defined in ConCat.Category Associated Types type Con (a :* b) Source # Methods toDict :: (a :* b) -> Dict (Con (a :* b)) Source # unDict :: a :* b Source #
HasCon (Sat kon a) Source #
Instance details Defined in ConCat.Category Associated Types type Con (Sat kon a) Source # Methods toDict :: Sat kon a -> Dict (Con (Sat kon a)) Source # unDict :: Sat kon a Source #

newtype Sat kon a Source #

Constructors

Sat (Dict (kon a))

Instances

Instances details

OpCon (op :: k -> k -> k) (Yes1' :: k -> Type) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k0) (b :: k0). (Yes1' a && Yes1' b) \|- Yes1' (op a b) Source #
OpCon (:*) (Sat Additive) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat Additive a && Sat Additive b) \|- Sat Additive (a :* b) Source #
OpCon (:*) (Sat HasCon) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat HasCon a && Sat HasCon b) \|- Sat HasCon (a :* b) Source #
OpCon (:*) (Sat Eq) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat Eq a && Sat Eq b) \|- Sat Eq (a :* b) Source #
OpCon (:*) (Sat Ord) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat Ord a && Sat Ord b) \|- Sat Ord (a :* b) Source #
OpCon (:+) (Sat Eq) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat Eq a && Sat Eq b) \|- Sat Eq (a :+ b) Source #
OpCon (:+) (Sat Ord) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat Ord a && Sat Ord b) \|- Sat Ord (a :+ b) Source #
Typeable op => OpCon (op :: k -> k -> k) (Sat (Typeable :: k -> Constraint) :: k -> Type) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k0) (b :: k0). (Sat Typeable a && Sat Typeable b) \|- Sat Typeable (op a b) Source #
(OpSat op con, OpSat op con') => OpCon (op :: k -> k -> k) (Sat (con &+& con') :: k -> Type) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k0) (b :: k0). (Sat (con &+& con') a && Sat (con &+& con') b) \|- Sat (con &+& con') (op a b) Source #
OpCon (->) (Sat Additive) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat Additive a && Sat Additive b) \|- Sat Additive (a -> b) Source #
HasCon (Sat kon a) Source #
Instance details Defined in ConCat.Category Associated Types type Con (Sat kon a) Source # Methods toDict :: Sat kon a -> Dict (Con (Sat kon a)) Source # unDict :: Sat kon a Source #
type Con (Sat kon a) Source #
Instance details Defined in ConCat.Category type Con (Sat kon a) = kon a

newtype a |- b infixr 1 Source #

Constructors

Entail (Con a :- Con b)

Instances

Instances details

AssociativePCat (\|-) Source #
Instance details Defined in ConCat.Category Methods lassocP :: Ok3 (\|-) a b c => Prod (\|-) a (Prod (\|-) b c) \|- Prod (\|-) (Prod (\|-) a b) c Source # rassocP :: Ok3 (\|-) a b c => Prod (\|-) (Prod (\|-) a b) c \|- Prod (\|-) a (Prod (\|-) b c) Source #
BraidedPCat (\|-) Source #
Instance details Defined in ConCat.Category Methods swapP :: Ok2 (\|-) a b => Prod (\|-) a b \|- Prod (\|-) b a Source #
Category (\|-) Source #
Instance details Defined in ConCat.Category Associated Types type Ok (\|-) :: Type -> Constraint Source # Methods id :: Ok (\|-) a => a \|- a Source # (.) :: forall b c a. Ok3 (\|-) a b c => (b \|- c) -> (a \|- b) -> a \|- c Source #
MonoidalPCat (\|-) Source #
Instance details Defined in ConCat.Category Methods (***) :: Ok4 (\|-) a b c d => (a \|- c) -> (b \|- d) -> Prod (\|-) a b \|- Prod (\|-) c d Source # first :: forall a a' b. Ok3 (\|-) a b a' => (a \|- a') -> Prod (\|-) a b \|- Prod (\|-) a' b Source # second :: Ok3 (\|-) a b b' => (b \|- b') -> Prod (\|-) a b \|- Prod (\|-) a b' Source #
ProductCat (\|-) Source #
Instance details Defined in ConCat.Category Methods exl :: Ok2 (\|-) a b => Prod (\|-) a b \|- a Source # exr :: Ok2 (\|-) a b => Prod (\|-) a b \|- b Source # dup :: Ok (\|-) a => a \|- Prod (\|-) a a Source #
Newtype (a \|- b) Source #
Instance details Defined in ConCat.Category Associated Types type O (a \|- b) Source # Methods pack :: O (a \|- b) -> a \|- b Source # unpack :: (a \|- b) -> O (a \|- b) Source #
type Ok (\|-) Source #
Instance details Defined in ConCat.Category type Ok (\|-) = Yes1 :: Type -> Constraint
type O (a \|- b) Source #
Instance details Defined in ConCat.Category type O (a \|- b) = Con a :- Con b

(<+) :: Con a => (Con b => r) -> (a |- b) -> r infixl 1 Source #

Wrapper

type (&&) = (:*) infixr 3 Source #

class OpCon op con where Source #

Methods

inOp :: (con a && con b) |- con (a `op` b) Source #

Instances

Instances details

OpCon (op :: k -> k -> k) (Yes1' :: k -> Type) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k0) (b :: k0). (Yes1' a && Yes1' b) \|- Yes1' (op a b) Source #
OpCon (:*) (Sat Additive) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat Additive a && Sat Additive b) \|- Sat Additive (a :* b) Source #
OpCon (:*) (Sat HasCon) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat HasCon a && Sat HasCon b) \|- Sat HasCon (a :* b) Source #
OpCon (:*) (Sat Eq) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat Eq a && Sat Eq b) \|- Sat Eq (a :* b) Source #
OpCon (:*) (Sat Ord) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat Ord a && Sat Ord b) \|- Sat Ord (a :* b) Source #
OpCon (:+) (Sat Eq) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat Eq a && Sat Eq b) \|- Sat Eq (a :+ b) Source #
OpCon (:+) (Sat Ord) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat Ord a && Sat Ord b) \|- Sat Ord (a :+ b) Source #
Typeable op => OpCon (op :: k -> k -> k) (Sat (Typeable :: k -> Constraint) :: k -> Type) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k0) (b :: k0). (Sat Typeable a && Sat Typeable b) \|- Sat Typeable (op a b) Source #
(OpSat op con, OpSat op con') => OpCon (op :: k -> k -> k) (Sat (con &+& con') :: k -> Type) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k0) (b :: k0). (Sat (con &+& con') a && Sat (con &+& con') b) \|- Sat (con &+& con') (op a b) Source #
OpCon (->) (Sat Additive) Source #
Instance details Defined in ConCat.Category Methods inOp :: forall (a :: k) (b :: k). (Sat Additive a && Sat Additive b) \|- Sat Additive (a -> b) Source #

yes1 :: c |- Sat Yes1 a Source #

forkCon :: forall con con' a. Sat (con &+& con') a |- (Sat con a :* Sat con' a) Source #

joinCon :: forall con con' a. (Sat con a :* Sat con' a) |- Sat (con &+& con') a Source #

inForkCon :: ((Sat con1 a :* Sat con2 a) |- (Sat con1' b :* Sat con2' b)) -> Sat (con1 &+& con2) a |- Sat (con1' &+& con2') b Source #

type Yes1' = Sat Yes1 Source #

type Ok' k = Sat (Ok k) Source #

type OpSat op kon = OpCon op (Sat kon) Source #

inSat :: OpCon op (Sat con) => (Sat con a && Sat con b) |- Sat con (a `op` b) Source #

inOpL :: OpCon op con => ((con a && con b) && con c) |- con ((a `op` b) `op` c) Source #

inOpR :: OpCon op con => (con a && (con b && con c)) |- con (a `op` (b `op` c)) Source #

inOpL' :: OpCon op con => ((con a && con b) && con c) |- (con (a `op` b) && con ((a `op` b) `op` c)) Source #

inOpR' :: OpCon op con => (con a && (con b && con c)) |- (con (a `op` (b `op` c)) && con (b `op` c)) Source #

inOpLR :: forall op con a b c. OpCon op con => (((con a && con b) && con c) && (con a && (con b && con c))) |- (con ((a `op` b) `op` c) && con (a `op` (b `op` c))) Source #

class OkAdd k where Source #

Methods

okAdd :: Ok' k a |- Sat Additive a Source #

type Ok2 k a b = C2 (Ok k) a b Source #

type Ok3 k a b c = C3 (Ok k) a b c Source #

type Ok4 k a b c d = C4 (Ok k) a b c d Source #

type Ok5 k a b c d e = C5 (Ok k) a b c d e Source #

type Ok6 k a b c d e f = C6 (Ok k) a b c d e f Source #

type Oks k as = AllC (Ok k) as Source #

class Show2 k where Source #

Methods

show2 :: (a `k` b) -> String Source #

class Category k where Source #

Associated Types

type Ok k :: Type -> Constraint Source #

type Ok k = Yes1

Methods

id :: Ok k a => a `k` a Source #

(.) :: forall b c a. Ok3 k a b c => (b `k` c) -> (a `k` b) -> a `k` c infixr 9 Source #

Instances

Instances details

Category (\|-) Source #
Instance details Defined in ConCat.Category Associated Types type Ok (\|-) :: Type -> Constraint Source # Methods id :: Ok (\|-) a => a \|- a Source # (.) :: forall b c a. Ok3 (\|-) a b c => (b \|- c) -> (a \|- b) -> a \|- c Source #
Monad m => Category (Kleisli m) Source #
Instance details Defined in ConCat.Category Associated Types type Ok (Kleisli m) :: Type -> Constraint Source # Methods id :: Ok (Kleisli m) a => Kleisli m a a Source # (.) :: forall b c a. Ok3 (Kleisli m) a b c => Kleisli m b c -> Kleisli m a b -> Kleisli m a c Source #
Category (Coercion :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Associated Types type Ok Coercion :: Type -> Constraint Source # Methods id :: Ok Coercion a => Coercion a a Source # (.) :: forall b c a. Ok3 Coercion a b c => Coercion b c -> Coercion a b -> Coercion a c Source #
Category ((:~:) :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Associated Types type Ok (:~:) :: Type -> Constraint Source # Methods id :: Ok (:~:) a => a :~: a Source # (.) :: forall b c a. Ok3 (:~:) a b c => (b :~: c) -> (a :~: b) -> a :~: c Source #
Category (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Associated Types type Ok U2 :: Type -> Constraint Source # Methods id :: Ok U2 a => U2 a a Source # (.) :: forall b c a. Ok3 U2 a b c => U2 b c -> U2 a b -> U2 a c Source #
Category (->) Source #
Instance details Defined in ConCat.Category Associated Types type Ok (->) :: Type -> Constraint Source # Methods id :: Ok (->) a => a -> a Source # (.) :: forall b c a. Ok3 (->) a b c => (b -> c) -> (a -> b) -> a -> c Source #
Monoid m => Category (Monoid2 m :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Associated Types type Ok (Monoid2 m) :: Type -> Constraint Source # Methods id :: Ok (Monoid2 m) a => Monoid2 m a a Source # (.) :: forall b c a. Ok3 (Monoid2 m) a b c => Monoid2 m b c -> Monoid2 m a b -> Monoid2 m a c Source #
(Category k, Category k') => Category (k :**: k') Source #
Instance details Defined in ConCat.Category Associated Types type Ok (k :: k') :: Type -> Constraint Source # Methods id :: Ok (k :: k') a => (k :: k') a a Source # (.) :: forall b c a. Ok3 (k :: k') a b c => (k :: k') b c -> (k :: k') a b -> (k :**: k') a c Source #
Category k => Category (Constrained con k) Source #
Instance details Defined in ConCat.Category Associated Types type Ok (Constrained con k) :: Type -> Constraint Source # Methods id :: Ok (Constrained con k) a => Constrained con k a a Source # (.) :: forall b c a. Ok3 (Constrained con k) a b c => Constrained con k b c -> Constrained con k a b -> Constrained con k a c Source #

(<~) :: (Category k, Oks k [a, b, a', b']) => (b `k` b') -> (a' `k` a) -> (a `k` b) -> a' `k` b' infixl 1 Source #

Add post- and pre-processing

(~>) :: (Category k, Oks k [a, b, a', b']) => (a' `k` a) -> (b `k` b') -> (a `k` b) -> a' `k` b' infixr 1 Source #

Add pre- and post-processing

type Prod k = (:*) Source #

type OkProd k = OpCon (Prod k) (Ok' k) Source #

okProd :: forall k a b. OkProd k => (Ok' k a && Ok' k b) |- Ok' k (Prod k a b) Source #

class (Category k, OkProd k) => AssociativePCat k where Source #

Minimal complete definition

Nothing

Methods

lassocP :: forall a b c. Ok3 k a b c => Prod k a (Prod k b c) `k` Prod k (Prod k a b) c Source #

default lassocP :: forall a b c. (MProductCat k, Ok3 k a b c) => Prod k a (Prod k b c) `k` Prod k (Prod k a b) c Source #

rassocP :: forall a b c. Ok3 k a b c => Prod k (Prod k a b) c `k` Prod k a (Prod k b c) Source #

default rassocP :: forall a b c. (MProductCat k, Ok3 k a b c) => Prod k (Prod k a b) c `k` Prod k a (Prod k b c) Source #

Instances

Instances details

AssociativePCat (\|-) Source #
Instance details Defined in ConCat.Category Methods lassocP :: Ok3 (\|-) a b c => Prod (\|-) a (Prod (\|-) b c) \|- Prod (\|-) (Prod (\|-) a b) c Source # rassocP :: Ok3 (\|-) a b c => Prod (\|-) (Prod (\|-) a b) c \|- Prod (\|-) a (Prod (\|-) b c) Source #
AssociativePCat (->) Source #
Instance details Defined in ConCat.Category Methods lassocP :: Ok3 (->) a b c => Prod (->) a (Prod (->) b c) -> Prod (->) (Prod (->) a b) c Source # rassocP :: Ok3 (->) a b c => Prod (->) (Prod (->) a b) c -> Prod (->) a (Prod (->) b c) Source #
(AssociativePCat k, AssociativePCat k') => AssociativePCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods lassocP :: Ok3 (k :: k') a b c => (k :: k') (Prod (k :: k') a (Prod (k :: k') b c)) (Prod (k :: k') (Prod (k :: k') a b) c) Source # rassocP :: Ok3 (k :: k') a b c => (k :: k') (Prod (k :: k') (Prod (k :: k') a b) c) (Prod (k :: k') a (Prod (k :: k') b c)) Source #
(AssociativePCat k, OpSat (Prod k) con) => AssociativePCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods lassocP :: Ok3 (Constrained con k) a b c => Constrained con k (Prod (Constrained con k) a (Prod (Constrained con k) b c)) (Prod (Constrained con k) (Prod (Constrained con k) a b) c) Source # rassocP :: Ok3 (Constrained con k) a b c => Constrained con k (Prod (Constrained con k) (Prod (Constrained con k) a b) c) (Prod (Constrained con k) a (Prod (Constrained con k) b c)) Source #

class (Category k, OkProd k) => MonoidalPCat k where Source #

Category with monoidal product.

Minimal complete definition

(***)

Methods

(***) :: forall a b c d. Ok4 k a b c d => (a `k` c) -> (b `k` d) -> Prod k a b `k` Prod k c d infixr 3 Source #

first :: forall a a' b. Ok3 k a b a' => (a `k` a') -> Prod k a b `k` Prod k a' b Source #

second :: forall a b b'. Ok3 k a b b' => (b `k` b') -> Prod k a b `k` Prod k a b' Source #

Instances

Instances details

MonoidalPCat (\|-) Source #
Instance details Defined in ConCat.Category Methods (***) :: Ok4 (\|-) a b c d => (a \|- c) -> (b \|- d) -> Prod (\|-) a b \|- Prod (\|-) c d Source # first :: forall a a' b. Ok3 (\|-) a b a' => (a \|- a') -> Prod (\|-) a b \|- Prod (\|-) a' b Source # second :: Ok3 (\|-) a b b' => (b \|- b') -> Prod (\|-) a b \|- Prod (\|-) a b' Source #
Monad m => MonoidalPCat (Kleisli m) Source #
Instance details Defined in ConCat.Category Methods (***) :: Ok4 (Kleisli m) a b c d => Kleisli m a c -> Kleisli m b d -> Kleisli m (Prod (Kleisli m) a b) (Prod (Kleisli m) c d) Source # first :: forall a a' b. Ok3 (Kleisli m) a b a' => Kleisli m a a' -> Kleisli m (Prod (Kleisli m) a b) (Prod (Kleisli m) a' b) Source # second :: Ok3 (Kleisli m) a b b' => Kleisli m b b' -> Kleisli m (Prod (Kleisli m) a b) (Prod (Kleisli m) a b') Source #
MonoidalPCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods (***) :: Ok4 U2 a b c d => U2 a c -> U2 b d -> U2 (Prod U2 a b) (Prod U2 c d) Source # first :: forall a a' b. Ok3 U2 a b a' => U2 a a' -> U2 (Prod U2 a b) (Prod U2 a' b) Source # second :: Ok3 U2 a b b' => U2 b b' -> U2 (Prod U2 a b) (Prod U2 a b') Source #
MonoidalPCat (->) Source #
Instance details Defined in ConCat.Category Methods (***) :: Ok4 (->) a b c d => (a -> c) -> (b -> d) -> Prod (->) a b -> Prod (->) c d Source # first :: forall a a' b. Ok3 (->) a b a' => (a -> a') -> Prod (->) a b -> Prod (->) a' b Source # second :: Ok3 (->) a b b' => (b -> b') -> Prod (->) a b -> Prod (->) a b' Source #
(MonoidalPCat k, MonoidalPCat k') => MonoidalPCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods (*) :: Ok4 (k :: k') a b c d => (k :: k') a c -> (k :: k') b d -> (k :: k') (Prod (k :: k') a b) (Prod (k :: k') c d) Source # first :: forall a a' b. Ok3 (k :: k') a b a' => (k :: k') a a' -> (k :: k') (Prod (k :: k') a b) (Prod (k :: k') a' b) Source # second :: Ok3 (k :: k') a b b' => (k :: k') b b' -> (k :: k') (Prod (k :: k') a b) (Prod (k :**: k') a b') Source #
(MonoidalPCat k, OpSat (Prod k) con) => MonoidalPCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods (***) :: Ok4 (Constrained con k) a b c d => Constrained con k a c -> Constrained con k b d -> Constrained con k (Prod (Constrained con k) a b) (Prod (Constrained con k) c d) Source # first :: forall a a' b. Ok3 (Constrained con k) a b a' => Constrained con k a a' -> Constrained con k (Prod (Constrained con k) a b) (Prod (Constrained con k) a' b) Source # second :: Ok3 (Constrained con k) a b b' => Constrained con k b b' -> Constrained con k (Prod (Constrained con k) a b) (Prod (Constrained con k) a b') Source #

class (Category k, OkProd k) => BraidedPCat k where Source #

Braided monoidal category

Minimal complete definition

Nothing

Methods

swapP :: forall a b. Ok2 k a b => Prod k a b `k` Prod k b a Source #

default swapP :: forall a b. (ProductCat k, MonoidalPCat k, Ok2 k a b) => Prod k a b `k` Prod k b a Source #

Instances

Instances details

BraidedPCat (\|-) Source #
Instance details Defined in ConCat.Category Methods swapP :: Ok2 (\|-) a b => Prod (\|-) a b \|- Prod (\|-) b a Source #
Monad m => BraidedPCat (Kleisli m) Source #
Instance details Defined in ConCat.Category Methods swapP :: Ok2 (Kleisli m) a b => Kleisli m (Prod (Kleisli m) a b) (Prod (Kleisli m) b a) Source #
BraidedPCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods swapP :: Ok2 U2 a b => U2 (Prod U2 a b) (Prod U2 b a) Source #
BraidedPCat (->) Source #
Instance details Defined in ConCat.Category Methods swapP :: Ok2 (->) a b => Prod (->) a b -> Prod (->) b a Source #
(BraidedPCat k, BraidedPCat k') => BraidedPCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods swapP :: Ok2 (k :: k') a b => (k :: k') (Prod (k :: k') a b) (Prod (k :: k') b a) Source #
(BraidedPCat k, OpSat (Prod k) con) => BraidedPCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods swapP :: Ok2 (Constrained con k) a b => Constrained con k (Prod (Constrained con k) a b) (Prod (Constrained con k) b a) Source #

type MBraidedPCat k = (BraidedPCat k, MonoidalPCat k) Source #

class (Category k, OkProd k) => ProductCat k where Source #

Category with product.

Methods

exl :: Ok2 k a b => Prod k a b `k` a Source #

exr :: Ok2 k a b => Prod k a b `k` b Source #

dup :: Ok k a => a `k` Prod k a a Source #

Instances

Instances details

ProductCat (\|-) Source #
Instance details Defined in ConCat.Category Methods exl :: Ok2 (\|-) a b => Prod (\|-) a b \|- a Source # exr :: Ok2 (\|-) a b => Prod (\|-) a b \|- b Source # dup :: Ok (\|-) a => a \|- Prod (\|-) a a Source #
Monad m => ProductCat (Kleisli m) Source #
Instance details Defined in ConCat.Category Methods exl :: Ok2 (Kleisli m) a b => Kleisli m (Prod (Kleisli m) a b) a Source # exr :: Ok2 (Kleisli m) a b => Kleisli m (Prod (Kleisli m) a b) b Source # dup :: Ok (Kleisli m) a => Kleisli m a (Prod (Kleisli m) a a) Source #
ProductCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods exl :: Ok2 U2 a b => U2 (Prod U2 a b) a Source # exr :: Ok2 U2 a b => U2 (Prod U2 a b) b Source # dup :: Ok U2 a => U2 a (Prod U2 a a) Source #
ProductCat (->) Source #
Instance details Defined in ConCat.Category Methods exl :: Ok2 (->) a b => Prod (->) a b -> a Source # exr :: Ok2 (->) a b => Prod (->) a b -> b Source # dup :: Ok (->) a => a -> Prod (->) a a Source #
(ProductCat k, ProductCat k') => ProductCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods exl :: Ok2 (k :: k') a b => (k :: k') (Prod (k :: k') a b) a Source # exr :: Ok2 (k :: k') a b => (k :: k') (Prod (k :: k') a b) b Source # dup :: Ok (k :: k') a => (k :: k') a (Prod (k :**: k') a a) Source #
(ProductCat k, OpSat (Prod k) con) => ProductCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods exl :: Ok2 (Constrained con k) a b => Constrained con k (Prod (Constrained con k) a b) a Source # exr :: Ok2 (Constrained con k) a b => Constrained con k (Prod (Constrained con k) a b) b Source # dup :: Ok (Constrained con k) a => Constrained con k a (Prod (Constrained con k) a a) Source #

(&&&) :: forall k a c d. (MProductCat k, Ok3 k a c d) => (a `k` c) -> (a `k` d) -> a `k` Prod k c d infixr 3 Source #

type MProductCat k = (ProductCat k, MonoidalPCat k) Source #

type Coprod k = (:+) Source #

type OkCoprod k = OpCon (Coprod k) (Ok' k) Source #

okCoprod :: forall k a b. OkCoprod k => (Ok' k a && Ok' k b) |- Ok' k (Coprod k a b) Source #

class (Category k, OkCoprod k) => AssociativeSCat k where Source #

Minimal complete definition

Nothing

Methods

lassocS :: forall a b c. Oks k [a, b, c] => Coprod k a (Coprod k b c) `k` Coprod k (Coprod k a b) c Source #

default lassocS :: forall a b c. (MCoproductCat k, Oks k [a, b, c]) => Coprod k a (Coprod k b c) `k` Coprod k (Coprod k a b) c Source #

rassocS :: forall a b c. Oks k [a, b, c] => Coprod k (Coprod k a b) c `k` Coprod k a (Coprod k b c) Source #

default rassocS :: forall a b c. (MCoproductCat k, Oks k [a, b, c]) => Coprod k (Coprod k a b) c `k` Coprod k a (Coprod k b c) Source #

Instances

Instances details

AssociativeSCat (->) Source #
Instance details Defined in ConCat.Category Methods lassocS :: Oks (->) '[a, b, c] => Coprod (->) a (Coprod (->) b c) -> Coprod (->) (Coprod (->) a b) c Source # rassocS :: Oks (->) '[a, b, c] => Coprod (->) (Coprod (->) a b) c -> Coprod (->) a (Coprod (->) b c) Source #
(AssociativeSCat k, AssociativeSCat k') => AssociativeSCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods lassocS :: Oks (k :: k') '[a, b, c] => (k :: k') (Coprod (k :: k') a (Coprod (k :: k') b c)) (Coprod (k :: k') (Coprod (k :: k') a b) c) Source # rassocS :: Oks (k :: k') '[a, b, c] => (k :: k') (Coprod (k :: k') (Coprod (k :: k') a b) c) (Coprod (k :: k') a (Coprod (k :: k') b c)) Source #
(AssociativeSCat k, OpSat (Coprod k) con) => AssociativeSCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods lassocS :: Oks (Constrained con k) '[a, b, c] => Constrained con k (Coprod (Constrained con k) a (Coprod (Constrained con k) b c)) (Coprod (Constrained con k) (Coprod (Constrained con k) a b) c) Source # rassocS :: Oks (Constrained con k) '[a, b, c] => Constrained con k (Coprod (Constrained con k) (Coprod (Constrained con k) a b) c) (Coprod (Constrained con k) a (Coprod (Constrained con k) b c)) Source #

class (Category k, OkCoprod k) => BraidedSCat k where Source #

Minimal complete definition

Nothing

Methods

swapS :: forall a b. Ok2 k a b => Coprod k a b `k` Coprod k b a Source #

default swapS :: forall a b. (MCoproductCat k, Ok2 k a b) => Coprod k a b `k` Coprod k b a Source #

Instances

Instances details

Monad m => BraidedSCat (Kleisli m) Source #
Instance details Defined in ConCat.Category Methods swapS :: Ok2 (Kleisli m) a b => Kleisli m (Coprod (Kleisli m) a b) (Coprod (Kleisli m) b a) Source #
BraidedSCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods swapS :: Ok2 U2 a b => U2 (Coprod U2 a b) (Coprod U2 b a) Source #
BraidedSCat (->) Source #
Instance details Defined in ConCat.Category Methods swapS :: Ok2 (->) a b => Coprod (->) a b -> Coprod (->) b a Source #
(BraidedSCat k, BraidedSCat k') => BraidedSCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods swapS :: Ok2 (k :: k') a b => (k :: k') (Coprod (k :: k') a b) (Coprod (k :: k') b a) Source #
(BraidedSCat k, OpSat (Coprod k) con) => BraidedSCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods swapS :: Ok2 (Constrained con k) a b => Constrained con k (Coprod (Constrained con k) a b) (Coprod (Constrained con k) b a) Source #

class (OkCoprod k, Category k) => MonoidalSCat k where Source #

Minimal complete definition

(+++)

Methods

(+++) :: forall a b c d. Ok4 k a b c d => (c `k` a) -> (d `k` b) -> Coprod k c d `k` Coprod k a b infixr 2 Source #

left :: forall a a' b. Oks k [a, b, a'] => (a `k` a') -> Coprod k a b `k` Coprod k a' b Source #

right :: forall a b b'. Oks k [a, b, b'] => (b `k` b') -> Coprod k a b `k` Coprod k a b' Source #

Instances

Instances details

Monad m => MonoidalSCat (Kleisli m) Source #
Instance details Defined in ConCat.Category Methods (+++) :: Ok4 (Kleisli m) a b c d => Kleisli m c a -> Kleisli m d b -> Kleisli m (Coprod (Kleisli m) c d) (Coprod (Kleisli m) a b) Source # left :: forall a a' b. Oks (Kleisli m) '[a, b, a'] => Kleisli m a a' -> Kleisli m (Coprod (Kleisli m) a b) (Coprod (Kleisli m) a' b) Source # right :: Oks (Kleisli m) '[a, b, b'] => Kleisli m b b' -> Kleisli m (Coprod (Kleisli m) a b) (Coprod (Kleisli m) a b') Source #
MonoidalSCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods (+++) :: Ok4 U2 a b c d => U2 c a -> U2 d b -> U2 (Coprod U2 c d) (Coprod U2 a b) Source # left :: forall a a' b. Oks U2 '[a, b, a'] => U2 a a' -> U2 (Coprod U2 a b) (Coprod U2 a' b) Source # right :: Oks U2 '[a, b, b'] => U2 b b' -> U2 (Coprod U2 a b) (Coprod U2 a b') Source #
MonoidalSCat (->) Source #
Instance details Defined in ConCat.Category Methods (+++) :: Ok4 (->) a b c d => (c -> a) -> (d -> b) -> Coprod (->) c d -> Coprod (->) a b Source # left :: forall a a' b. Oks (->) '[a, b, a'] => (a -> a') -> Coprod (->) a b -> Coprod (->) a' b Source # right :: Oks (->) '[a, b, b'] => (b -> b') -> Coprod (->) a b -> Coprod (->) a b' Source #
(MonoidalSCat k, MonoidalSCat k') => MonoidalSCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods (+++) :: Ok4 (k :: k') a b c d => (k :: k') c a -> (k :: k') d b -> (k :: k') (Coprod (k :: k') c d) (Coprod (k :: k') a b) Source # left :: forall a a' b. Oks (k :: k') '[a, b, a'] => (k :: k') a a' -> (k :: k') (Coprod (k :: k') a b) (Coprod (k :: k') a' b) Source # right :: Oks (k :: k') '[a, b, b'] => (k :: k') b b' -> (k :: k') (Coprod (k :: k') a b) (Coprod (k :: k') a b') Source #
(MonoidalSCat k, OpSat (Coprod k) con) => MonoidalSCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods (+++) :: Ok4 (Constrained con k) a b c d => Constrained con k c a -> Constrained con k d b -> Constrained con k (Coprod (Constrained con k) c d) (Coprod (Constrained con k) a b) Source # left :: forall a a' b. Oks (Constrained con k) '[a, b, a'] => Constrained con k a a' -> Constrained con k (Coprod (Constrained con k) a b) (Coprod (Constrained con k) a' b) Source # right :: Oks (Constrained con k) '[a, b, b'] => Constrained con k b b' -> Constrained con k (Coprod (Constrained con k) a b) (Coprod (Constrained con k) a b') Source #

class (Category k, OkCoprod k) => CoproductCat k where Source #

Category with coproduct.

Methods

inl :: Ok2 k a b => a `k` Coprod k a b Source #

inr :: Ok2 k a b => b `k` Coprod k a b Source #

jam :: Ok k a => Coprod k a a `k` a Source #

Instances

Instances details

Monad m => CoproductCat (Kleisli m) Source #
Instance details Defined in ConCat.Category Methods inl :: Ok2 (Kleisli m) a b => Kleisli m a (Coprod (Kleisli m) a b) Source # inr :: Ok2 (Kleisli m) a b => Kleisli m b (Coprod (Kleisli m) a b) Source # jam :: Ok (Kleisli m) a => Kleisli m (Coprod (Kleisli m) a a) a Source #
CoproductCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods inl :: Ok2 U2 a b => U2 a (Coprod U2 a b) Source # inr :: Ok2 U2 a b => U2 b (Coprod U2 a b) Source # jam :: Ok U2 a => U2 (Coprod U2 a a) a Source #
CoproductCat (->) Source #
Instance details Defined in ConCat.Category Methods inl :: Ok2 (->) a b => a -> Coprod (->) a b Source # inr :: Ok2 (->) a b => b -> Coprod (->) a b Source # jam :: Ok (->) a => Coprod (->) a a -> a Source #
(CoproductCat k, CoproductCat k') => CoproductCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods inl :: Ok2 (k :: k') a b => (k :: k') a (Coprod (k :: k') a b) Source # inr :: Ok2 (k :: k') a b => (k :: k') b (Coprod (k :: k') a b) Source # jam :: Ok (k :: k') a => (k :: k') (Coprod (k :**: k') a a) a Source #
(CoproductCat k, OpSat (Coprod k) con) => CoproductCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods inl :: Ok2 (Constrained con k) a b => Constrained con k a (Coprod (Constrained con k) a b) Source # inr :: Ok2 (Constrained con k) a b => Constrained con k b (Coprod (Constrained con k) a b) Source # jam :: Ok (Constrained con k) a => Constrained con k (Coprod (Constrained con k) a a) a Source #

type MCoproductCat k = (CoproductCat k, MonoidalSCat k) Source #

(|||) :: forall k a c d. (MCoproductCat k, Ok3 k a c d) => (c `k` a) -> (d `k` a) -> Coprod k c d `k` a infixr 2 Source #

type AbelianCat k = (MProductCat k, CoproductPCat k, TerminalCat k, CoterminalCat k, OkAdd k) Source #

zeroC :: (AbelianCat k, Ok2 k a b) => a `k` b Source #

plusC :: forall k a b. (AbelianCat k, Ok2 k a b) => Binop (a `k` b) Source #

type CoprodP k = Prod k Source #

type OkCoprodP k = OkProd k Source #

okCoprodP :: forall k a b. OkCoprodP k => (Ok' k a && Ok' k b) |- Ok' k (CoprodP k a b) Source #

class BraidedPCat k => CoproductPCat k where Source #

Category with coproduct as Cartesian product.

Methods

inlP :: Ok2 k a b => a `k` CoprodP k a b Source #

inrP :: Ok2 k a b => b `k` CoprodP k a b Source #

jamP :: Ok k a => CoprodP k a a `k` a Source #

Instances

Instances details

CoproductPCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods inlP :: Ok2 U2 a b => U2 a (CoprodP U2 a b) Source # inrP :: Ok2 U2 a b => U2 b (CoprodP U2 a b) Source # jamP :: Ok U2 a => U2 (CoprodP U2 a a) a Source #
(CoproductPCat k, CoproductPCat k') => CoproductPCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods inlP :: Ok2 (k :: k') a b => (k :: k') a (CoprodP (k :: k') a b) Source # inrP :: Ok2 (k :: k') a b => (k :: k') b (CoprodP (k :: k') a b) Source # jamP :: Ok (k :: k') a => (k :: k') (CoprodP (k :**: k') a a) a Source #

type MCoproductPCat k = (CoproductPCat k, MonoidalPCat k) Source #

(||||) :: forall k a c d. (MCoproductPCat k, Ok3 k a c d) => (c `k` a) -> (d `k` a) -> CoprodP k c d `k` a infixr 2 Source #

class ScalarCat k a where Source #

Methods

scale :: a -> a `k` a Source #

Instances

Instances details

ScalarCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods scale :: a -> U2 a a Source #
Num a => ScalarCat (->) a Source #
Instance details Defined in ConCat.Category Methods scale :: a -> a -> a Source #
(ScalarCat k a, ScalarCat k' a) => ScalarCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods scale :: a -> (k :**: k') a a Source #

type LinearCat k a = (MProductCat k, CoproductPCat k, ScalarCat k a, Ok k a) Source #

class DistribCat k where Source #

Minimal complete definition

distl | distr

Methods

distl :: forall a u v. Ok3 k a u v => Prod k a (Coprod k u v) `k` Coprod k (Prod k a u) (Prod k a v) Source #

default distl :: forall a u v. (MonoidalSCat k, BraidedPCat k, Ok3 k a u v) => Prod k a (Coprod k u v) `k` Coprod k (Prod k a u) (Prod k a v) Source #

distr :: forall u v b. Ok3 k u v b => Prod k (Coprod k u v) b `k` Coprod k (Prod k u b) (Prod k v b) Source #

default distr :: forall u v b. (MonoidalSCat k, BraidedPCat k, Ok3 k u v b) => Prod k (Coprod k u v) b `k` Coprod k (Prod k u b) (Prod k v b) Source #

Instances

Instances details

DistribCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods distl :: Ok3 U2 a u v => U2 (Prod U2 a (Coprod U2 u v)) (Coprod U2 (Prod U2 a u) (Prod U2 a v)) Source # distr :: Ok3 U2 u v b => U2 (Prod U2 (Coprod U2 u v) b) (Coprod U2 (Prod U2 u b) (Prod U2 v b)) Source #
DistribCat (->) Source #
Instance details Defined in ConCat.Category Methods distl :: Ok3 (->) a u v => Prod (->) a (Coprod (->) u v) -> Coprod (->) (Prod (->) a u) (Prod (->) a v) Source # distr :: Ok3 (->) u v b => Prod (->) (Coprod (->) u v) b -> Coprod (->) (Prod (->) u b) (Prod (->) v b) Source #
(DistribCat k, DistribCat k') => DistribCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods distl :: Ok3 (k :: k') a u v => (k :: k') (Prod (k :: k') a (Coprod (k :: k') u v)) (Coprod (k :: k') (Prod (k :: k') a u) (Prod (k :: k') a v)) Source # distr :: Ok3 (k :: k') u v b => (k :: k') (Prod (k :: k') (Coprod (k :: k') u v) b) (Coprod (k :: k') (Prod (k :: k') u b) (Prod (k :: k') v b)) Source #

type OkExp k = OpCon (Exp k) (Ok' k) Source #

okExp :: forall k a b. OkExp k => (Ok' k a && Ok' k b) |- Ok' k (Exp k a b) Source #

type Exp k = (->) Source #

class (OkExp k, ProductCat k) => ClosedCat k where Source #

Minimal complete definition

curry, (apply | uncurry)

Methods

apply :: forall a b. Ok2 k a b => Prod k (Exp k a b) a `k` b Source #

curry :: Ok3 k a b c => (Prod k a b `k` c) -> a `k` Exp k b c Source #

uncurry :: forall a b c. Ok3 k a b c => (a `k` Exp k b c) -> Prod k a b `k` c Source #

default uncurry :: forall a b c. (MonoidalPCat k, Ok3 k a b c) => (a `k` Exp k b c) -> Prod k a b `k` c Source #

Instances

Instances details

ClosedCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods apply :: Ok2 U2 a b => U2 (Prod U2 (Exp U2 a b) a) b Source # curry :: Ok3 U2 a b c => U2 (Prod U2 a b) c -> U2 a (Exp U2 b c) Source # uncurry :: Ok3 U2 a b c => U2 a (Exp U2 b c) -> U2 (Prod U2 a b) c Source #
ClosedCat (->) Source #
Instance details Defined in ConCat.Category Methods apply :: Ok2 (->) a b => Prod (->) (Exp (->) a b) a -> b Source # curry :: Ok3 (->) a b c => (Prod (->) a b -> c) -> a -> Exp (->) b c Source # uncurry :: Ok3 (->) a b c => (a -> Exp (->) b c) -> Prod (->) a b -> c Source #
(ClosedCat k, ClosedCat k') => ClosedCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods apply :: Ok2 (k :: k') a b => (k :: k') (Prod (k :: k') (Exp (k :: k') a b) a) b Source # curry :: Ok3 (k :: k') a b c => (k :: k') (Prod (k :: k') a b) c -> (k :: k') a (Exp (k :: k') b c) Source # uncurry :: Ok3 (k :: k') a b c => (k :: k') a (Exp (k :: k') b c) -> (k :: k') (Prod (k :: k') a b) c Source #
(ClosedCat k, OpSat (Prod k) con, OpSat (Exp k) con) => ClosedCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods apply :: Ok2 (Constrained con k) a b => Constrained con k (Prod (Constrained con k) (Exp (Constrained con k) a b) a) b Source # curry :: Ok3 (Constrained con k) a b c => Constrained con k (Prod (Constrained con k) a b) c -> Constrained con k a (Exp (Constrained con k) b c) Source # uncurry :: Ok3 (Constrained con k) a b c => Constrained con k a (Exp (Constrained con k) b c) -> Constrained con k (Prod (Constrained con k) a b) c Source #

applyK :: Kleisli m (Kleisli m a b :* a) b Source #

curryK :: Monad m => Kleisli m (a :* b) c -> Kleisli m a (Kleisli m b c) Source #

uncurryK :: Monad m => Kleisli m a (Kleisli m b c) -> Kleisli m (a :* b) c Source #

class OkExp k => FlipCat k where Source #

Methods

flipC :: Ok3 k a b c => (a `k` (b -> c)) -> b -> a `k` c Source #

flipC' :: Ok3 k a b c => (b -> a `k` c) -> a `k` (b -> c) Source #

Instances

Instances details

FlipCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods flipC :: Ok3 U2 a b c => U2 a (b -> c) -> b -> U2 a c Source # flipC' :: Ok3 U2 a b c => (b -> U2 a c) -> U2 a (b -> c) Source #
FlipCat (->) Source #
Instance details Defined in ConCat.Category Methods flipC :: Ok3 (->) a b c => (a -> (b -> c)) -> b -> a -> c Source # flipC' :: Ok3 (->) a b c => (b -> a -> c) -> a -> (b -> c) Source #
(FlipCat k, FlipCat k') => FlipCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods flipC :: Ok3 (k :: k') a b c => (k :: k') a (b -> c) -> b -> (k :: k') a c Source # flipC' :: Ok3 (k :: k') a b c => (b -> (k :: k') a c) -> (k :: k') a (b -> c) Source #

type Unit k = () Source #

type OkUnit k = Ok k (Unit k) Source #

class OkUnit k => TerminalCat k where Source #

Minimal complete definition

Nothing

Methods

it :: Ok k a => a `k` Unit k Source #

default it :: (ConstCat k (Unit k), Ok k a) => a `k` Unit k Source #

Instances

Instances details

Monad m => TerminalCat (Kleisli m) Source #
Instance details Defined in ConCat.Category Methods it :: Ok (Kleisli m) a => Kleisli m a (Unit (Kleisli m)) Source #
TerminalCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods it :: Ok U2 a => U2 a (Unit U2) Source #
TerminalCat (->) Source #
Instance details Defined in ConCat.Category Methods it :: Ok (->) a => a -> Unit (->) Source #
(TerminalCat k, TerminalCat k') => TerminalCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods it :: Ok (k :: k') a => (k :: k') a (Unit (k :**: k')) Source #

class OkUnit k => UnitCat k where Source #

Minimal complete definition

Nothing

Methods

lunit :: Ok k a => a `k` Prod k (Unit k) a Source #

default lunit :: (MProductCat k, TerminalCat k, Ok k a) => a `k` Prod k (Unit k) a Source #

lcounit :: Ok k a => Prod k (Unit k) a `k` a Source #

default lcounit :: (ProductCat k, Ok k a) => Prod k (Unit k) a `k` a Source #

runit :: Ok k a => a `k` Prod k a (Unit k) Source #

default runit :: (MProductCat k, TerminalCat k, Ok k a) => a `k` Prod k a (Unit k) Source #

rcounit :: Ok k a => Prod k a (Unit k) `k` a Source #

default rcounit :: (ProductCat k, TerminalCat k, Ok k a) => Prod k a (Unit k) `k` a Source #

Instances

Instances details

Monad m => UnitCat (Kleisli m) Source #
Instance details Defined in ConCat.Category Methods lunit :: Ok (Kleisli m) a => Kleisli m a (Prod (Kleisli m) (Unit (Kleisli m)) a) Source # lcounit :: Ok (Kleisli m) a => Kleisli m (Prod (Kleisli m) (Unit (Kleisli m)) a) a Source # runit :: Ok (Kleisli m) a => Kleisli m a (Prod (Kleisli m) a (Unit (Kleisli m))) Source # rcounit :: Ok (Kleisli m) a => Kleisli m (Prod (Kleisli m) a (Unit (Kleisli m))) a Source #
UnitCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods lunit :: Ok U2 a => U2 a (Prod U2 (Unit U2) a) Source # lcounit :: Ok U2 a => U2 (Prod U2 (Unit U2) a) a Source # runit :: Ok U2 a => U2 a (Prod U2 a (Unit U2)) Source # rcounit :: Ok U2 a => U2 (Prod U2 a (Unit U2)) a Source #
UnitCat (->) Source #
Instance details Defined in ConCat.Category Methods lunit :: Ok (->) a => a -> Prod (->) (Unit (->)) a Source # lcounit :: Ok (->) a => Prod (->) (Unit (->)) a -> a Source # runit :: Ok (->) a => a -> Prod (->) a (Unit (->)) Source # rcounit :: Ok (->) a => Prod (->) a (Unit (->)) -> a Source #
(UnitCat k, UnitCat k') => UnitCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods lunit :: Ok (k :: k') a => (k :: k') a (Prod (k :: k') (Unit (k :: k')) a) Source # lcounit :: Ok (k :: k') a => (k :: k') (Prod (k :: k') (Unit (k :: k')) a) a Source # runit :: Ok (k :: k') a => (k :: k') a (Prod (k :: k') a (Unit (k :: k'))) Source # rcounit :: Ok (k :: k') a => (k :: k') (Prod (k :: k') a (Unit (k :: k'))) a Source #

type Counit k = () Source #

class Ok k (Counit k) => CoterminalCat k where Source #

Methods

ti :: Ok k a => Counit k `k` a Source #

Instances

Instances details

CoterminalCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods ti :: Ok U2 a => U2 (Counit U2) a Source #
(CoterminalCat k, CoterminalCat k') => CoterminalCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods ti :: Ok (k :: k') a => (k :: k') (Counit (k :**: k')) a Source #

constFun :: forall k p a b. (ClosedCat k, Ok3 k p a b) => (a `k` b) -> p `k` Exp k a b Source #

constFun2 :: forall k p a b c. (ClosedCat k, Oks k [p, a, b, c]) => (Prod k a b `k` c) -> p `k` Exp k a (Exp k b c) Source #

unitFun :: forall k a b. (ClosedCat k, TerminalCat k, Ok2 k a b) => (a `k` b) -> Unit k `k` Exp k a b Source #

unUnitFun :: forall k p a. (ClosedCat k, MonoidalPCat k, TerminalCat k, Oks k [p, a]) => (Unit k `k` Exp k p a) -> p `k` a Source #

type ConstObj k b = b Source #

class (Category k, Ok k (ConstObj k b)) => ConstCat k b where Source #

Minimal complete definition

Nothing

Methods

const :: Ok k a => b -> a `k` ConstObj k b Source #

default const :: (TerminalCat k, Ok k a) => b -> a `k` ConstObj k b Source #

unitArrow :: OkUnit k => b -> Unit k `k` ConstObj k b Source #

Instances

Instances details

(Monad m, ConstCat (->) b) => ConstCat (Kleisli m) b Source #
Instance details Defined in ConCat.Category Methods const :: Ok (Kleisli m) a => b -> Kleisli m a (ConstObj (Kleisli m) b) Source # unitArrow :: b -> Kleisli m (Unit (Kleisli m)) (ConstObj (Kleisli m) b) Source #
ConstCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods const :: Ok U2 a0 => a -> U2 a0 (ConstObj U2 a) Source # unitArrow :: a -> U2 (Unit U2) (ConstObj U2 a) Source #
ConstCat (->) b Source #
Instance details Defined in ConCat.Category Methods const :: Ok (->) a => b -> a -> ConstObj (->) b Source # unitArrow :: b -> Unit (->) -> ConstObj (->) b Source #
(ConstCat k a, ConstCat k' a) => ConstCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods const :: Ok (k :: k') a0 => a -> (k :: k') a0 (ConstObj (k :: k') a) Source # unitArrow :: a -> (k :: k') (Unit (k :: k')) (ConstObj (k :: k') a) Source #
(ConstCat k b, con b) => ConstCat (Constrained con k) b Source #
Instance details Defined in ConCat.Category Methods const :: Ok (Constrained con k) a => b -> Constrained con k a (ConstObj (Constrained con k) b) Source # unitArrow :: b -> Constrained con k (Unit (Constrained con k)) (ConstObj (Constrained con k) b) Source #

repConst :: (HasRep b, r ~ Rep b, RepCat k b (ConstObj k r), ConstCat k r, Ok k a, Ok k (ConstObj k b)) => b -> a `k` ConstObj k b Source #

pairConst :: (MProductCat k, ConstCat k b, ConstCat k c, Ok k a) => (b :* c) -> a `k` (b :* c) Source #

lconst :: forall k a b. (MProductCat k, ConstCat k a, Ok2 k a b) => a -> b `k` (a :* b) Source #

Inject a constant on the left

rconst :: forall k a b. (MProductCat k, ConstCat k b, Ok2 k a b) => b -> a `k` (a :* b) Source #

Inject a constant on the right

class DelayCat k where Source #

Methods

delay :: Ok k a => a -> a `k` a Source #

Instances

Instances details

DelayCat (->) Source #
Instance details Defined in ConCat.Category Methods delay :: Ok (->) a => a -> a -> a Source #

class ProductCat k => LoopCat k where Source #

Methods

loop :: Ok3 k s a b => ((a :* s) `k` (b :* s)) -> a `k` b Source #

Instances

Instances details

LoopCat (->) Source #
Instance details Defined in ConCat.Category Methods loop :: Ok3 (->) s a b => ((a :* s) -> (b :* s)) -> a -> b Source #

class ProductCat k => TracedCat k where Source #

Methods

trace :: Ok3 k a b c => ((a :* c) `k` (b :* c)) -> a `k` b Source #

Instances

Instances details

MonadFix m => TracedCat (Kleisli m) Source #
Instance details Defined in ConCat.Category Methods trace :: Ok3 (Kleisli m) a b c => Kleisli m (a :* c) (b :* c) -> Kleisli m a b Source #
TracedCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods trace :: Ok3 U2 a b c => U2 (a :* c) (b :* c) -> U2 a b Source #
TracedCat (->) Source #
Instance details Defined in ConCat.Category Methods trace :: Ok3 (->) a b c => ((a :* c) -> (b :* c)) -> a -> b Source #
(TracedCat k, TracedCat k') => TracedCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods trace :: Ok3 (k :: k') a b c => (k :: k') (a :* c) (b :* c) -> (k :**: k') a b Source #
(TracedCat k, OpSat (Prod k) con) => TracedCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods trace :: Ok3 (Constrained con k) a b c => Constrained con k (a :* c) (b :* c) -> Constrained con k a b Source #

type BiCCC k = (ClosedCat k, CoproductCat k, TerminalCat k, DistribCat k) Source #

Bi-cartesion (cartesian & co-cartesian) closed categories. Also lumps in terminal and distributive, though should probably be moved out.

data Constrained (con :: Type -> Constraint) k a b Source #

Constructors

Constrained (a `k` b)

Instances

Instances details

(BottomCat k a b, con a, con b) => BottomCat (Constrained con k :: Type -> Type -> Type) (a :: Type) (b :: Type) Source #
Instance details Defined in ConCat.Category Methods bottomC :: Constrained con k a b Source #
(CoerceCat k a b, con a, con b) => CoerceCat (Constrained con k :: Type -> Type -> Type) (a :: Type) (b :: Type) Source #
Instance details Defined in ConCat.Category Methods coerceC :: Constrained con k a b Source #
(FromIntegralCat k a b, con a, con b) => FromIntegralCat (Constrained con k :: Type -> Type -> Type) (a :: Type) (b :: Type) Source #
Instance details Defined in ConCat.Category Methods fromIntegralC :: Constrained con k a b Source # foo_FromIntegralCat :: () Source #
(RepCat k a r, con a, con r) => RepCat (Constrained con k :: Type -> Type -> Type) (a :: Type) (r :: Type) Source #
Instance details Defined in ConCat.Category Methods reprC :: Constrained con k a r Source # abstC :: Constrained con k r a Source #
(AssociativePCat k, OpSat (Prod k) con) => AssociativePCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods lassocP :: Ok3 (Constrained con k) a b c => Constrained con k (Prod (Constrained con k) a (Prod (Constrained con k) b c)) (Prod (Constrained con k) (Prod (Constrained con k) a b) c) Source # rassocP :: Ok3 (Constrained con k) a b c => Constrained con k (Prod (Constrained con k) (Prod (Constrained con k) a b) c) (Prod (Constrained con k) a (Prod (Constrained con k) b c)) Source #
(AssociativeSCat k, OpSat (Coprod k) con) => AssociativeSCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods lassocS :: Oks (Constrained con k) '[a, b, c] => Constrained con k (Coprod (Constrained con k) a (Coprod (Constrained con k) b c)) (Coprod (Constrained con k) (Coprod (Constrained con k) a b) c) Source # rassocS :: Oks (Constrained con k) '[a, b, c] => Constrained con k (Coprod (Constrained con k) (Coprod (Constrained con k) a b) c) (Coprod (Constrained con k) a (Coprod (Constrained con k) b c)) Source #
(BoolCat k, con Bool, OpCon (Prod k) (Sat con)) => BoolCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods notC :: Constrained con k (BoolOf (Constrained con k)) (BoolOf (Constrained con k)) Source # andC :: Constrained con k (Prod (Constrained con k) (BoolOf (Constrained con k)) (BoolOf (Constrained con k))) (BoolOf (Constrained con k)) Source # orC :: Constrained con k (Prod (Constrained con k) (BoolOf (Constrained con k)) (BoolOf (Constrained con k))) (BoolOf (Constrained con k)) Source # xorC :: Constrained con k (Prod (Constrained con k) (BoolOf (Constrained con k)) (BoolOf (Constrained con k))) (BoolOf (Constrained con k)) Source #
(BraidedPCat k, OpSat (Prod k) con) => BraidedPCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods swapP :: Ok2 (Constrained con k) a b => Constrained con k (Prod (Constrained con k) a b) (Prod (Constrained con k) b a) Source #
(BraidedSCat k, OpSat (Coprod k) con) => BraidedSCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods swapS :: Ok2 (Constrained con k) a b => Constrained con k (Coprod (Constrained con k) a b) (Coprod (Constrained con k) b a) Source #
Category k => Category (Constrained con k) Source #
Instance details Defined in ConCat.Category Associated Types type Ok (Constrained con k) :: Type -> Constraint Source # Methods id :: Ok (Constrained con k) a => Constrained con k a a Source # (.) :: forall b c a. Ok3 (Constrained con k) a b c => Constrained con k b c -> Constrained con k a b -> Constrained con k a c Source #
(ClosedCat k, OpSat (Prod k) con, OpSat (Exp k) con) => ClosedCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods apply :: Ok2 (Constrained con k) a b => Constrained con k (Prod (Constrained con k) (Exp (Constrained con k) a b) a) b Source # curry :: Ok3 (Constrained con k) a b c => Constrained con k (Prod (Constrained con k) a b) c -> Constrained con k a (Exp (Constrained con k) b c) Source # uncurry :: Ok3 (Constrained con k) a b c => Constrained con k a (Exp (Constrained con k) b c) -> Constrained con k (Prod (Constrained con k) a b) c Source #
(CoproductCat k, OpSat (Coprod k) con) => CoproductCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods inl :: Ok2 (Constrained con k) a b => Constrained con k a (Coprod (Constrained con k) a b) Source # inr :: Ok2 (Constrained con k) a b => Constrained con k b (Coprod (Constrained con k) a b) Source # jam :: Ok (Constrained con k) a => Constrained con k (Coprod (Constrained con k) a a) a Source #
(MonoidalPCat k, OpSat (Prod k) con) => MonoidalPCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods (***) :: Ok4 (Constrained con k) a b c d => Constrained con k a c -> Constrained con k b d -> Constrained con k (Prod (Constrained con k) a b) (Prod (Constrained con k) c d) Source # first :: forall a a' b. Ok3 (Constrained con k) a b a' => Constrained con k a a' -> Constrained con k (Prod (Constrained con k) a b) (Prod (Constrained con k) a' b) Source # second :: Ok3 (Constrained con k) a b b' => Constrained con k b b' -> Constrained con k (Prod (Constrained con k) a b) (Prod (Constrained con k) a b') Source #
(MonoidalSCat k, OpSat (Coprod k) con) => MonoidalSCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods (+++) :: Ok4 (Constrained con k) a b c d => Constrained con k c a -> Constrained con k d b -> Constrained con k (Coprod (Constrained con k) c d) (Coprod (Constrained con k) a b) Source # left :: forall a a' b. Oks (Constrained con k) '[a, b, a'] => Constrained con k a a' -> Constrained con k (Coprod (Constrained con k) a b) (Coprod (Constrained con k) a' b) Source # right :: Oks (Constrained con k) '[a, b, b'] => Constrained con k b b' -> Constrained con k (Coprod (Constrained con k) a b) (Coprod (Constrained con k) a b') Source #
(ProductCat k, OpSat (Prod k) con) => ProductCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods exl :: Ok2 (Constrained con k) a b => Constrained con k (Prod (Constrained con k) a b) a Source # exr :: Ok2 (Constrained con k) a b => Constrained con k (Prod (Constrained con k) a b) b Source # dup :: Ok (Constrained con k) a => Constrained con k a (Prod (Constrained con k) a a) Source #
(TracedCat k, OpSat (Prod k) con) => TracedCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods trace :: Ok3 (Constrained con k) a b c => Constrained con k (a :* c) (b :* c) -> Constrained con k a b Source #
(ConstCat k b, con b) => ConstCat (Constrained con k) b Source #
Instance details Defined in ConCat.Category Methods const :: Ok (Constrained con k) a => b -> Constrained con k a (ConstObj (Constrained con k) b) Source # unitArrow :: b -> Constrained con k (Unit (Constrained con k)) (ConstObj (Constrained con k) b) Source #
(EqCat k a, con a, con Bool, OpSat (Prod k) con) => EqCat (Constrained con k) a Source #
Instance details Defined in ConCat.Category Methods equal :: Constrained con k (Prod (Constrained con k) a a) (BoolOf (Constrained con k)) Source # notEqual :: Constrained con k (Prod (Constrained con k) a a) (BoolOf (Constrained con k)) Source #
(FloatingCat k a, con a) => FloatingCat (Constrained con k) a Source #
Instance details Defined in ConCat.Category Methods expC :: Constrained con k a a Source # logC :: Constrained con k a a Source # cosC :: Constrained con k a a Source # sinC :: Constrained con k a a Source # sqrtC :: Constrained con k a a Source # tanhC :: Constrained con k a a Source #
(FractionalCat k a, con a) => FractionalCat (Constrained con k) a Source #
Instance details Defined in ConCat.Category Methods recipC :: Constrained con k a a Source # divideC :: Constrained con k (Prod (Constrained con k) a a) a Source #
FunctorCat k f => FunctorCat (Constrained con k) f Source #
Instance details Defined in ConCat.Category Methods fmapC :: Ok2 (Constrained con k) a b => Constrained con k a b -> Constrained con k (f a) (f b) Source # unzipC :: Ok2 (Constrained con k) a b => Constrained con k (f (a :* b)) (f a :* f b) Source #
(IfCat k a, OpCon (Prod k) (Sat con), con Bool, con a) => IfCat (Constrained con k) a Source #
Instance details Defined in ConCat.Category Methods ifC :: IfT (Constrained con k) a Source #
(IntegralCat k a, con a) => IntegralCat (Constrained con k) a Source #
Instance details Defined in ConCat.Category Methods divC :: Constrained con k (Prod (Constrained con k) a a) a Source # modC :: Constrained con k (Prod (Constrained con k) a a) a Source #
(NumCat k a, con a) => NumCat (Constrained con k) a Source #
Instance details Defined in ConCat.Category Methods negateC :: Constrained con k a a Source # addC :: Constrained con k (Prod (Constrained con k) a a) a Source # subC :: Constrained con k (Prod (Constrained con k) a a) a Source # mulC :: Constrained con k (Prod (Constrained con k) a a) a Source # powIC :: Constrained con k (Prod (Constrained con k) a Int) a Source #
OkFunctor (Constrained con k) f Source #
Instance details Defined in ConCat.Category Methods okFunctor :: Ok' (Constrained con k) a \|- Ok' (Constrained con k) (f a) Source #
(OrdCat k a, con a, con Bool, OpSat (Prod k) con) => OrdCat (Constrained con k) a Source #
Instance details Defined in ConCat.Category Methods lessThan :: Constrained con k (Prod (Constrained con k) a a) (BoolOf (Constrained con k)) Source # greaterThan :: Constrained con k (Prod (Constrained con k) a a) (BoolOf (Constrained con k)) Source # lessThanOrEqual :: Constrained con k (Prod (Constrained con k) a a) (BoolOf (Constrained con k)) Source # greaterThanOrEqual :: Constrained con k (Prod (Constrained con k) a a) (BoolOf (Constrained con k)) Source #
RepresentableCat k f => RepresentableCat (Constrained con k) f Source #
Instance details Defined in ConCat.Category Methods tabulateC :: Ok (Constrained con k) a => Constrained con k (Rep f -> a) (f a) Source # indexC :: Ok (Constrained con k) a => Constrained con k (f a) (Rep f -> a) Source #
(Applicative m, con a) => PointedCat (Constrained con (->)) m a Source #
Instance details Defined in ConCat.Category Methods pointC :: Constrained con (->) a (m a) Source #
(RealFracCat k a b, con a, con b) => RealFracCat (Constrained con k) a b Source #
Instance details Defined in ConCat.Category Methods floorC :: Constrained con k a b Source # ceilingC :: Constrained con k a b Source # truncateC :: Constrained con k a b Source #
type Ok (Constrained con k) Source #
Instance details Defined in ConCat.Category type Ok (Constrained con k) = Ok k &+& con

type BoolOf k = Bool Source #

class (ProductCat k, Ok k (BoolOf k)) => BoolCat k where Source #

Methods

notC :: BoolOf k `k` BoolOf k Source #

andC :: Prod k (BoolOf k) (BoolOf k) `k` BoolOf k Source #

orC :: Prod k (BoolOf k) (BoolOf k) `k` BoolOf k Source #

xorC :: Prod k (BoolOf k) (BoolOf k) `k` BoolOf k Source #

Instances

Instances details

Monad m => BoolCat (Kleisli m) Source #
Instance details Defined in ConCat.Category Methods notC :: Kleisli m (BoolOf (Kleisli m)) (BoolOf (Kleisli m)) Source # andC :: Kleisli m (Prod (Kleisli m) (BoolOf (Kleisli m)) (BoolOf (Kleisli m))) (BoolOf (Kleisli m)) Source # orC :: Kleisli m (Prod (Kleisli m) (BoolOf (Kleisli m)) (BoolOf (Kleisli m))) (BoolOf (Kleisli m)) Source # xorC :: Kleisli m (Prod (Kleisli m) (BoolOf (Kleisli m)) (BoolOf (Kleisli m))) (BoolOf (Kleisli m)) Source #
BoolCat (U2 :: Type -> Type -> Type) Source #
Instance details Defined in ConCat.Category Methods notC :: U2 (BoolOf U2) (BoolOf U2) Source # andC :: U2 (Prod U2 (BoolOf U2) (BoolOf U2)) (BoolOf U2) Source # orC :: U2 (Prod U2 (BoolOf U2) (BoolOf U2)) (BoolOf U2) Source # xorC :: U2 (Prod U2 (BoolOf U2) (BoolOf U2)) (BoolOf U2) Source #
BoolCat (->) Source #
Instance details Defined in ConCat.Category Methods notC :: BoolOf (->) -> BoolOf (->) Source # andC :: Prod (->) (BoolOf (->)) (BoolOf (->)) -> BoolOf (->) Source # orC :: Prod (->) (BoolOf (->)) (BoolOf (->)) -> BoolOf (->) Source # xorC :: Prod (->) (BoolOf (->)) (BoolOf (->)) -> BoolOf (->) Source #
(BoolCat k, BoolCat k') => BoolCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods notC :: (k :: k') (BoolOf (k :: k')) (BoolOf (k :: k')) Source # andC :: (k :: k') (Prod (k :: k') (BoolOf (k :: k')) (BoolOf (k :: k'))) (BoolOf (k :: k')) Source # orC :: (k :: k') (Prod (k :: k') (BoolOf (k :: k')) (BoolOf (k :: k'))) (BoolOf (k :: k')) Source # xorC :: (k :: k') (Prod (k :: k') (BoolOf (k :: k')) (BoolOf (k :: k'))) (BoolOf (k :: k')) Source #
(BoolCat k, con Bool, OpCon (Prod k) (Sat con)) => BoolCat (Constrained con k) Source #
Instance details Defined in ConCat.Category Methods notC :: Constrained con k (BoolOf (Constrained con k)) (BoolOf (Constrained con k)) Source # andC :: Constrained con k (Prod (Constrained con k) (BoolOf (Constrained con k)) (BoolOf (Constrained con k))) (BoolOf (Constrained con k)) Source # orC :: Constrained con k (Prod (Constrained con k) (BoolOf (Constrained con k)) (BoolOf (Constrained con k))) (BoolOf (Constrained con k)) Source # xorC :: Constrained con k (Prod (Constrained con k) (BoolOf (Constrained con k)) (BoolOf (Constrained con k))) (BoolOf (Constrained con k)) Source #

okTT :: forall k a. OkProd k => Ok' k a |- Ok' k (Prod k a a) Source #

class (BoolCat k, Ok k a) => EqCat k a where Source #

Minimal complete definition

equal | notEqual

Methods

equal :: Prod k a a `k` BoolOf k Source #

notEqual :: Prod k a a `k` BoolOf k Source #

Instances

Instances details

(Monad m, Eq a) => EqCat (Kleisli m) a Source #
Instance details Defined in ConCat.Category Methods equal :: Kleisli m (Prod (Kleisli m) a a) (BoolOf (Kleisli m)) Source # notEqual :: Kleisli m (Prod (Kleisli m) a a) (BoolOf (Kleisli m)) Source #
EqCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods equal :: U2 (Prod U2 a a) (BoolOf U2) Source # notEqual :: U2 (Prod U2 a a) (BoolOf U2) Source #
Eq a => EqCat (->) a Source #
Instance details Defined in ConCat.Category Methods equal :: Prod (->) a a -> BoolOf (->) Source # notEqual :: Prod (->) a a -> BoolOf (->) Source #
(EqCat k a, EqCat k' a) => EqCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods equal :: (k :: k') (Prod (k :: k') a a) (BoolOf (k :: k')) Source # notEqual :: (k :: k') (Prod (k :: k') a a) (BoolOf (k :: k')) Source #
(EqCat k a, con a, con Bool, OpSat (Prod k) con) => EqCat (Constrained con k) a Source #
Instance details Defined in ConCat.Category Methods equal :: Constrained con k (Prod (Constrained con k) a a) (BoolOf (Constrained con k)) Source # notEqual :: Constrained con k (Prod (Constrained con k) a a) (BoolOf (Constrained con k)) Source #

class (EqCat k a, Ord a) => OrdCat k a where Source #

Minimal complete definition

lessThan | greaterThan

Methods

lessThan :: Prod k a a `k` BoolOf k Source #

default lessThan :: BraidedPCat k => Prod k a a `k` BoolOf k Source #

greaterThan :: Prod k a a `k` BoolOf k Source #

default greaterThan :: BraidedPCat k => Prod k a a `k` BoolOf k Source #

lessThanOrEqual :: Prod k a a `k` BoolOf k Source #

greaterThanOrEqual :: Prod k a a `k` BoolOf k Source #

Instances

Instances details

(Monad m, Ord a) => OrdCat (Kleisli m) a Source #
Instance details Defined in ConCat.Category Methods lessThan :: Kleisli m (Prod (Kleisli m) a a) (BoolOf (Kleisli m)) Source # greaterThan :: Kleisli m (Prod (Kleisli m) a a) (BoolOf (Kleisli m)) Source # lessThanOrEqual :: Kleisli m (Prod (Kleisli m) a a) (BoolOf (Kleisli m)) Source # greaterThanOrEqual :: Kleisli m (Prod (Kleisli m) a a) (BoolOf (Kleisli m)) Source #
Ord a => OrdCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods lessThan :: U2 (Prod U2 a a) (BoolOf U2) Source # greaterThan :: U2 (Prod U2 a a) (BoolOf U2) Source # lessThanOrEqual :: U2 (Prod U2 a a) (BoolOf U2) Source # greaterThanOrEqual :: U2 (Prod U2 a a) (BoolOf U2) Source #
Ord a => OrdCat (->) a Source #
Instance details Defined in ConCat.Category Methods lessThan :: Prod (->) a a -> BoolOf (->) Source # greaterThan :: Prod (->) a a -> BoolOf (->) Source # lessThanOrEqual :: Prod (->) a a -> BoolOf (->) Source # greaterThanOrEqual :: Prod (->) a a -> BoolOf (->) Source #
(OrdCat k a, OrdCat k' a) => OrdCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods lessThan :: (k :: k') (Prod (k :: k') a a) (BoolOf (k :: k')) Source # greaterThan :: (k :: k') (Prod (k :: k') a a) (BoolOf (k :: k')) Source # lessThanOrEqual :: (k :: k') (Prod (k :: k') a a) (BoolOf (k :: k')) Source # greaterThanOrEqual :: (k :: k') (Prod (k :: k') a a) (BoolOf (k :: k')) Source #
(OrdCat k a, con a, con Bool, OpSat (Prod k) con) => OrdCat (Constrained con k) a Source #
Instance details Defined in ConCat.Category Methods lessThan :: Constrained con k (Prod (Constrained con k) a a) (BoolOf (Constrained con k)) Source # greaterThan :: Constrained con k (Prod (Constrained con k) a a) (BoolOf (Constrained con k)) Source # lessThanOrEqual :: Constrained con k (Prod (Constrained con k) a a) (BoolOf (Constrained con k)) Source # greaterThanOrEqual :: Constrained con k (Prod (Constrained con k) a a) (BoolOf (Constrained con k)) Source #

class Ok k a => MinMaxCat k a where Source #

Methods

minC :: Prod k a a `k` a Source #

maxC :: Prod k a a `k` a Source #

Instances

Instances details

MinMaxCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods minC :: U2 (Prod U2 a a) a Source # maxC :: U2 (Prod U2 a a) a Source #
Ord a => MinMaxCat (->) a Source #
Instance details Defined in ConCat.Category Methods minC :: Prod (->) a a -> a Source # maxC :: Prod (->) a a -> a Source #
(MinMaxCat k a, MinMaxCat k' a) => MinMaxCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods minC :: (k :: k') (Prod (k :: k') a a) a Source # maxC :: (k :: k') (Prod (k :: k') a a) a Source #

class (Category k, Ok k a) => EnumCat k a where Source #

Minimal complete definition

Nothing

Methods

succC :: a `k` a Source #

default succC :: (MProductCat k, NumCat k a, ConstCat k a, Num a) => a `k` a Source #

predC :: a `k` a Source #

default predC :: (MProductCat k, NumCat k a, ConstCat k a, Num a) => a `k` a Source #

Instances

Instances details

EnumCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods succC :: U2 a a Source # predC :: U2 a a Source #
Enum a => EnumCat (->) a Source #
Instance details Defined in ConCat.Category Methods succC :: a -> a Source # predC :: a -> a Source #
(EnumCat k a, EnumCat k' a) => EnumCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods succC :: (k :: k') a a Source # predC :: (k :: k') a a Source #

class Ok k a => NumCat k a where Source #

Minimal complete definition

negateC, addC, mulC, powIC

Methods

negateC :: a `k` a Source #

addC :: Prod k a a `k` a Source #

subC :: Prod k a a `k` a Source #

default subC :: MProductCat k => Prod k a a `k` a Source #

mulC :: Prod k a a `k` a Source #

powIC :: Ok k Int => Prod k a Int `k` a Source #

Instances

Instances details

(Monad m, Num a) => NumCat (Kleisli m) a Source #
Instance details Defined in ConCat.Category Methods negateC :: Kleisli m a a Source # addC :: Kleisli m (Prod (Kleisli m) a a) a Source # subC :: Kleisli m (Prod (Kleisli m) a a) a Source # mulC :: Kleisli m (Prod (Kleisli m) a a) a Source # powIC :: Kleisli m (Prod (Kleisli m) a Int) a Source #
NumCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods negateC :: U2 a a Source # addC :: U2 (Prod U2 a a) a Source # subC :: U2 (Prod U2 a a) a Source # mulC :: U2 (Prod U2 a a) a Source # powIC :: U2 (Prod U2 a Int) a Source #
Num a => NumCat (->) a Source #
Instance details Defined in ConCat.Category Methods negateC :: a -> a Source # addC :: Prod (->) a a -> a Source # subC :: Prod (->) a a -> a Source # mulC :: Prod (->) a a -> a Source # powIC :: Prod (->) a Int -> a Source #
(NumCat k a, NumCat k' a) => NumCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods negateC :: (k :: k') a a Source # addC :: (k :: k') (Prod (k :: k') a a) a Source # subC :: (k :: k') (Prod (k :: k') a a) a Source # mulC :: (k :: k') (Prod (k :: k') a a) a Source # powIC :: (k :: k') (Prod (k :**: k') a Int) a Source #
(NumCat k a, con a) => NumCat (Constrained con k) a Source #
Instance details Defined in ConCat.Category Methods negateC :: Constrained con k a a Source # addC :: Constrained con k (Prod (Constrained con k) a a) a Source # subC :: Constrained con k (Prod (Constrained con k) a a) a Source # mulC :: Constrained con k (Prod (Constrained con k) a a) a Source # powIC :: Constrained con k (Prod (Constrained con k) a Int) a Source #

class Ok k a => IntegralCat k a where Source #

Methods

divC :: Prod k a a `k` a Source #

modC :: Prod k a a `k` a Source #

Instances

Instances details

(Monad m, Integral a) => IntegralCat (Kleisli m) a Source #
Instance details Defined in ConCat.Category Methods divC :: Kleisli m (Prod (Kleisli m) a a) a Source # modC :: Kleisli m (Prod (Kleisli m) a a) a Source #
IntegralCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods divC :: U2 (Prod U2 a a) a Source # modC :: U2 (Prod U2 a a) a Source #
Integral a => IntegralCat (->) a Source #
Instance details Defined in ConCat.Category Methods divC :: Prod (->) a a -> a Source # modC :: Prod (->) a a -> a Source #
(IntegralCat k a, IntegralCat k' a) => IntegralCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods divC :: (k :: k') (Prod (k :: k') a a) a Source # modC :: (k :: k') (Prod (k :: k') a a) a Source #
(IntegralCat k a, con a) => IntegralCat (Constrained con k) a Source #
Instance details Defined in ConCat.Category Methods divC :: Constrained con k (Prod (Constrained con k) a a) a Source # modC :: Constrained con k (Prod (Constrained con k) a a) a Source #

divModC :: forall k a. (MProductCat k, IntegralCat k a, Ok k a) => Prod k a a `k` Prod k a a Source #

class Ok k a => FractionalCat k a where Source #

Minimal complete definition

recipC | divideC

Methods

recipC :: a `k` a Source #

default recipC :: (MProductCat k, ConstCat k a, Num a) => a `k` a Source #

divideC :: Prod k a a `k` a Source #

default divideC :: (MProductCat k, NumCat k a) => Prod k a a `k` a Source #

Instances

Instances details

(Monad m, Fractional a) => FractionalCat (Kleisli m) a Source #
Instance details Defined in ConCat.Category Methods recipC :: Kleisli m a a Source # divideC :: Kleisli m (Prod (Kleisli m) a a) a Source #
FractionalCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods recipC :: U2 a a Source # divideC :: U2 (Prod U2 a a) a Source #
Fractional a => FractionalCat (->) a Source #
Instance details Defined in ConCat.Category Methods recipC :: a -> a Source # divideC :: Prod (->) a a -> a Source #
(FractionalCat k a, FractionalCat k' a) => FractionalCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods recipC :: (k :: k') a a Source # divideC :: (k :: k') (Prod (k :**: k') a a) a Source #
(FractionalCat k a, con a) => FractionalCat (Constrained con k) a Source #
Instance details Defined in ConCat.Category Methods recipC :: Constrained con k a a Source # divideC :: Constrained con k (Prod (Constrained con k) a a) a Source #

class Ok k a => FloatingCat k a where Source #

Methods

expC :: a `k` a Source #

logC :: a `k` a Source #

cosC :: a `k` a Source #

sinC :: a `k` a Source #

sqrtC :: a `k` a Source #

tanhC :: a `k` a Source #

Instances

Instances details

(Monad m, Floating a) => FloatingCat (Kleisli m) a Source #
Instance details Defined in ConCat.Category Methods expC :: Kleisli m a a Source # logC :: Kleisli m a a Source # cosC :: Kleisli m a a Source # sinC :: Kleisli m a a Source # sqrtC :: Kleisli m a a Source # tanhC :: Kleisli m a a Source #
FloatingCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods expC :: U2 a a Source # logC :: U2 a a Source # cosC :: U2 a a Source # sinC :: U2 a a Source # sqrtC :: U2 a a Source # tanhC :: U2 a a Source #
Floating a => FloatingCat (->) a Source #
Instance details Defined in ConCat.Category Methods expC :: a -> a Source # logC :: a -> a Source # cosC :: a -> a Source # sinC :: a -> a Source # sqrtC :: a -> a Source # tanhC :: a -> a Source #
(FloatingCat k a, FloatingCat k' a) => FloatingCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods expC :: (k :: k') a a Source # logC :: (k :: k') a a Source # cosC :: (k :: k') a a Source # sinC :: (k :: k') a a Source # sqrtC :: (k :: k') a a Source # tanhC :: (k :: k') a a Source #
(FloatingCat k a, con a) => FloatingCat (Constrained con k) a Source #
Instance details Defined in ConCat.Category Methods expC :: Constrained con k a a Source # logC :: Constrained con k a a Source # cosC :: Constrained con k a a Source # sinC :: Constrained con k a a Source # sqrtC :: Constrained con k a a Source # tanhC :: Constrained con k a a Source #

class Ok k a => RealFracCat k a b where Source #

Methods

floorC :: a `k` b Source #

ceilingC :: a `k` b Source #

truncateC :: a `k` b Source #

Instances

Instances details

(Monad m, RealFrac a, Integral b) => RealFracCat (Kleisli m) a b Source #
Instance details Defined in ConCat.Category Methods floorC :: Kleisli m a b Source # ceilingC :: Kleisli m a b Source # truncateC :: Kleisli m a b Source #
Integral b => RealFracCat (U2 :: Type -> Type -> Type) a b Source #
Instance details Defined in ConCat.Category Methods floorC :: U2 a b Source # ceilingC :: U2 a b Source # truncateC :: U2 a b Source #
(RealFrac a, Integral b) => RealFracCat (->) a b Source #
Instance details Defined in ConCat.Category Methods floorC :: a -> b Source # ceilingC :: a -> b Source # truncateC :: a -> b Source #
(RealFracCat k a b, RealFracCat k' a b) => RealFracCat (k :**: k') a b Source #
Instance details Defined in ConCat.Category Methods floorC :: (k :: k') a b Source # ceilingC :: (k :: k') a b Source # truncateC :: (k :**: k') a b Source #
(RealFracCat k a b, con a, con b) => RealFracCat (Constrained con k) a b Source #
Instance details Defined in ConCat.Category Methods floorC :: Constrained con k a b Source # ceilingC :: Constrained con k a b Source # truncateC :: Constrained con k a b Source #

class FromIntegralCat k a b where Source #

Minimal complete definition

fromIntegralC

Methods

fromIntegralC :: a `k` b Source #

foo_FromIntegralCat :: () Source #

Instances

Instances details

(Monad m, Integral a, Num b) => FromIntegralCat (Kleisli m :: Type -> Type -> Type) (a :: Type) (b :: Type) Source #
Instance details Defined in ConCat.Category Methods fromIntegralC :: Kleisli m a b Source # foo_FromIntegralCat :: () Source #
(Integral a, Num b) => FromIntegralCat (->) (a :: Type) (b :: Type) Source #
Instance details Defined in ConCat.Category Methods fromIntegralC :: a -> b Source # foo_FromIntegralCat :: () Source #
FromIntegralCat (U2 :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods fromIntegralC :: U2 a b Source # foo_FromIntegralCat :: () Source #
(FromIntegralCat k a b, con a, con b) => FromIntegralCat (Constrained con k :: Type -> Type -> Type) (a :: Type) (b :: Type) Source #
Instance details Defined in ConCat.Category Methods fromIntegralC :: Constrained con k a b Source # foo_FromIntegralCat :: () Source #
(FromIntegralCat k3 a b, FromIntegralCat k' a b) => FromIntegralCat (k3 :**: k' :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods fromIntegralC :: (k3 :**: k') a b Source # foo_FromIntegralCat :: () Source #

class BottomCat k a b where Source #

Methods

bottomC :: a `k` b Source #

Instances

Instances details

(BottomCat k a b, ClosedCat k, Ok4 k z b a (z -> b)) => BottomCat (k :: Type -> Type -> Type) (a :: Type) (z -> b :: Type) Source #
Instance details Defined in ConCat.Category Methods bottomC :: k a (z -> b) Source #
BottomCat (->) (a :: Type) (b :: Type) Source #
Instance details Defined in ConCat.Category Methods bottomC :: a -> b Source #
BottomCat (U2 :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods bottomC :: U2 a b Source #
(BottomCat k a b, con a, con b) => BottomCat (Constrained con k :: Type -> Type -> Type) (a :: Type) (b :: Type) Source #
Instance details Defined in ConCat.Category Methods bottomC :: Constrained con k a b Source #
(BottomCat k3 a b, BottomCat k' a b) => BottomCat (k3 :**: k' :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods bottomC :: (k3 :**: k') a b Source #

type IfT k a = Prod k (BoolOf k) (Prod k a a) `k` a Source #

class (BoolCat k, Ok k a) => IfCat k a where Source #

Methods

ifC :: IfT k a Source #

Instances

Instances details

Monad m => IfCat (Kleisli m) a Source #
Instance details Defined in ConCat.Category Methods ifC :: IfT (Kleisli m) a Source #
IfCat (U2 :: Type -> Type -> Type) a Source #
Instance details Defined in ConCat.Category Methods ifC :: IfT U2 a Source #
IfCat (->) a Source #
Instance details Defined in ConCat.Category Methods ifC :: IfT (->) a Source #
(IfCat k a, IfCat k' a) => IfCat (k :**: k') a Source #
Instance details Defined in ConCat.Category Methods ifC :: IfT (k :**: k') a Source #
(IfCat k a, OpCon (Prod k) (Sat con), con Bool, con a) => IfCat (Constrained con k) a Source #
Instance details Defined in ConCat.Category Methods ifC :: IfT (Constrained con k) a Source #

class UnknownCat k a b where Source #

Methods

unknownC :: a `k` b Source #

Instances

Instances details

UnknownCat (->) (a :: Type) (b :: Type) Source #
Instance details Defined in ConCat.Category Methods unknownC :: a -> b Source #
UnknownCat (U2 :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods unknownC :: U2 a b Source #
(UnknownCat k3 a b, UnknownCat k' a b) => UnknownCat (k3 :**: k' :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods unknownC :: (k3 :**: k') a b Source #

class RepCat k a r where Source #

Methods

reprC :: a `k` r Source #

abstC :: r `k` a Source #

Instances

Instances details

r ~ Rep a => RepCat (U2 :: Type -> Type -> Type) (a :: Type) (r :: Type) Source #
Instance details Defined in ConCat.Category Methods reprC :: U2 a r Source # abstC :: U2 r a Source #
(HasRep a, r ~ Rep a) => RepCat (->) (a :: Type) (r :: Type) Source #
Instance details Defined in ConCat.Category Methods reprC :: a -> r Source # abstC :: r -> a Source #
(RepCat k a r, con a, con r) => RepCat (Constrained con k :: Type -> Type -> Type) (a :: Type) (r :: Type) Source #
Instance details Defined in ConCat.Category Methods reprC :: Constrained con k a r Source # abstC :: Constrained con k r a Source #
(RepCat k2 a b, RepCat k' a b) => RepCat (k2 :**: k' :: k1 -> k1 -> Type) (a :: k1) (b :: k1) Source #
Instance details Defined in ConCat.Category Methods reprC :: (k2 :: k') a b Source # abstC :: (k2 :: k') b a Source #

class TransitiveCon con where Source #

Methods

trans :: (con a b, con b c) :- con a c Source #

Instances

Instances details

TransitiveCon (Coercible :: k -> k -> Constraint) Source #
Instance details Defined in ConCat.Category Methods trans :: forall (a :: k0) (b :: k0) (c :: k0). (Coercible a b, Coercible b c) :- Coercible a c Source #

class CoerceCat k a b where Source #

Methods

coerceC :: a `k` b Source #

Instances

Instances details

Coercible a b => CoerceCat (->) (a :: Type) (b :: Type) Source #
Instance details Defined in ConCat.Category Methods coerceC :: a -> b Source #
CoerceCat (U2 :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods coerceC :: U2 a b Source #
(CoerceCat k a b, con a, con b) => CoerceCat (Constrained con k :: Type -> Type -> Type) (a :: Type) (b :: Type) Source #
Instance details Defined in ConCat.Category Methods coerceC :: Constrained con k a b Source #
(CoerceCat k3 a b, CoerceCat k' a b) => CoerceCat (k3 :**: k' :: k1 -> k2 -> Type) (a :: k1) (b :: k2) Source #
Instance details Defined in ConCat.Category Methods coerceC :: (k3 :**: k') a b Source #

class OkFunctor k h where Source #

Methods

okFunctor :: Ok' k a |- Ok' k (h a) Source #

Instances

Instances details

OkFunctor (->) h Source #
Instance details Defined in ConCat.Category Methods okFunctor :: Ok' (->) a \|- Ok' (->) (h a) Source #
(OkFunctor k h, OkFunctor k' h) => OkFunctor (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods okFunctor :: Ok' (k :: k') a \|- Ok' (k :: k') (h a) Source #
OkFunctor (Constrained con k) f Source #
Instance details Defined in ConCat.Category Methods okFunctor :: Ok' (Constrained con k) a \|- Ok' (Constrained con k) (f a) Source #

class OkFunctor k h => FunctorCat k h where Source #

Methods

fmapC :: Ok2 k a b => (a `k` b) -> h a `k` h b Source #

unzipC :: forall a b. Ok2 k a b => h (a :* b) `k` (h a :* h b) Source #

Instances

Instances details

Functor h => FunctorCat (->) h Source #
Instance details Defined in ConCat.Category Methods fmapC :: Ok2 (->) a b => (a -> b) -> h a -> h b Source # unzipC :: Ok2 (->) a b => h (a :* b) -> (h a :* h b) Source #
(FunctorCat k h, FunctorCat k' h) => FunctorCat (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods fmapC :: Ok2 (k :: k') a b => (k :: k') a b -> (k :: k') (h a) (h b) Source # unzipC :: Ok2 (k :: k') a b => (k :*: k') (h (a : b)) (h a :* h b) Source #
FunctorCat k f => FunctorCat (Constrained con k) f Source #
Instance details Defined in ConCat.Category Methods fmapC :: Ok2 (Constrained con k) a b => Constrained con k a b -> Constrained con k (f a) (f b) Source # unzipC :: Ok2 (Constrained con k) a b => Constrained con k (f (a :* b)) (f a :* f b) Source #

class (Zip h, OkFunctor k h) => ZipCat k h where Source #

Methods

zipC :: Ok2 k a b => (h a :* h b) `k` h (a :* b) Source #

Instances

Instances details

Zip h => ZipCat (->) h Source #
Instance details Defined in ConCat.Category Methods zipC :: Ok2 (->) a b => (h a :* h b) -> h (a :* b) Source #
(ZipCat k h, ZipCat k' h) => ZipCat (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods zipC :: Ok2 (k :: k') a b => (k :: k') (h a :* h b) (h (a :* b)) Source #

class OkFunctor k h => ZapCat k h where Source #

Methods

zapC :: Ok2 k a b => h (a `k` b) -> h a `k` h b Source #

Instances

Instances details

Zip h => ZapCat (->) h Source #
Instance details Defined in ConCat.Category Methods zapC :: Ok2 (->) a b => h (a -> b) -> h a -> h b Source #
(ZapCat k h, ZapCat k' h, Functor h) => ZapCat (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods zapC :: Ok2 (k :: k') a b => h ((k :: k') a b) -> (k :**: k') (h a) (h b) Source #

class (OkFunctor k h, Ok k a) => PointedCat k h a where Source #

Methods

pointC :: a `k` h a Source #

Instances

Instances details

Pointed h => PointedCat (->) h a Source #
Instance details Defined in ConCat.Category Methods pointC :: a -> h a Source #
(PointedCat k h a, PointedCat k' h a) => PointedCat (k :**: k') h a Source #
Instance details Defined in ConCat.Category Methods pointC :: (k :**: k') a (h a) Source #
(Applicative m, con a) => PointedCat (Constrained con (->)) m a Source #
Instance details Defined in ConCat.Category Methods pointC :: Constrained con (->) a (m a) Source #

class Ok k a => AddCat k h a where Source #

Methods

sumAC :: h a `k` a Source #

Instances

Instances details

(Foldable h, Additive a) => AddCat (->) h a Source #
Instance details Defined in ConCat.Category Methods sumAC :: h a -> a Source #
(AddCat k h a, AddCat k' h a) => AddCat (k :**: k') h a Source #
Instance details Defined in ConCat.Category Methods sumAC :: (k :**: k') (h a) a Source #

class TraversableCat k t f where Source #

Methods

sequenceAC :: Ok k a => t (f a) `k` f (t a) Source #

Instances

Instances details

(Traversable t, Applicative f) => TraversableCat (->) t f Source #
Instance details Defined in ConCat.Category Methods sequenceAC :: Ok (->) a => t (f a) -> f (t a) Source #
(TraversableCat k t f, TraversableCat k' t f) => TraversableCat (k :**: k') t f Source #
Instance details Defined in ConCat.Category Methods sequenceAC :: Ok (k :: k') a => (k :: k') (t (f a)) (f (t a)) Source #

class DistributiveCat k g f where Source #

Methods

distributeC :: Ok k a => f (g a) `k` g (f a) Source #

Instances

Instances details

(Distributive g, Functor f) => DistributiveCat (->) g f Source #
Instance details Defined in ConCat.Category Methods distributeC :: Ok (->) a => f (g a) -> g (f a) Source #
(DistributiveCat k g f, DistributiveCat k' g f) => DistributiveCat (k :**: k') g f Source #
Instance details Defined in ConCat.Category Methods distributeC :: Ok (k :: k') a => (k :: k') (f (g a)) (g (f a)) Source #

class RepresentableCat k f where Source #

Methods

tabulateC :: Ok k a => (Rep f -> a) `k` f a Source #

indexC :: Ok k a => f a `k` (Rep f -> a) Source #

Instances

Instances details

Representable f => RepresentableCat (->) f Source #
Instance details Defined in ConCat.Category Methods tabulateC :: Ok (->) a => (Rep f -> a) -> f a Source # indexC :: Ok (->) a => f a -> (Rep f -> a) Source #
(RepresentableCat k h, RepresentableCat k' h) => RepresentableCat (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods tabulateC :: Ok (k :: k') a => (k :: k') (Rep h -> a) (h a) Source # indexC :: Ok (k :: k') a => (k :: k') (h a) (Rep h -> a) Source #
RepresentableCat k f => RepresentableCat (Constrained con k) f Source #
Instance details Defined in ConCat.Category Methods tabulateC :: Ok (Constrained con k) a => Constrained con k (Rep f -> a) (f a) Source # indexC :: Ok (Constrained con k) a => Constrained con k (f a) (Rep f -> a) Source #

fmap' :: Functor f => (a -> b) -> f a -> f b Source #

liftA2' :: Applicative f => (a -> b -> c) -> f a -> f b -> f c Source #

zipWith' :: Zip f => (a -> b -> c) -> f a -> f b -> f c Source #

class FunctorCat k h => Strong k h where Source #

Methods

strength :: Ok2 k a b => (a :* h b) `k` h (a :* b) Source #

Instances

Instances details

Functor h => Strong (->) h Source #
Instance details Defined in ConCat.Category Methods strength :: Ok2 (->) a b => (a :* h b) -> h (a :* b) Source #
(Strong k h, Strong k' h) => Strong (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods strength :: Ok2 (k :: k') a b => (k :: k') (a :* h b) (h (a :* b)) Source #

class OkIxProd k h where Source #

Methods

okIxProd :: Ok' k a |- Ok' k (h a) Source #

Instances

Instances details

OkIxProd (U2 :: Type -> Type -> Type) h Source #
Instance details Defined in ConCat.Category Methods okIxProd :: Ok' U2 a \|- Ok' U2 (h a) Source #
OkIxProd (->) h Source #
Instance details Defined in ConCat.Category Methods okIxProd :: Ok' (->) a \|- Ok' (->) (h a) Source #
(OkIxProd k h, OkIxProd k' h) => OkIxProd (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods okIxProd :: Ok' (k :: k') a \|- Ok' (k :: k') (h a) Source #

class (Category k, OkIxProd k h) => IxMonoidalPCat k h where Source #

Methods

crossF :: forall a b. Ok2 k a b => h (a `k` b) -> h a `k` h b Source #

Instances

Instances details

IxMonoidalPCat (U2 :: Type -> Type -> Type) h Source #
Instance details Defined in ConCat.Category Methods crossF :: Ok2 U2 a b => h (U2 a b) -> U2 (h a) (h b) Source #
Zip h => IxMonoidalPCat (->) h Source #
Instance details Defined in ConCat.Category Methods crossF :: Ok2 (->) a b => h (a -> b) -> h a -> h b Source #
(IxMonoidalPCat k h, IxMonoidalPCat k' h, Zip h) => IxMonoidalPCat (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods crossF :: Ok2 (k :: k') a b => h ((k :: k') a b) -> (k :**: k') (h a) (h b) Source #

class IxMonoidalPCat k h => IxProductCat k h where Source #

Minimal complete definition

exF, (forkF | replF)

Methods

exF :: forall a. Ok k a => h (h a `k` a) Source #

forkF :: forall a b. Ok2 k a b => h (a `k` b) -> a `k` h b Source #

replF :: forall a. Ok k a => a `k` h a Source #

default replF :: forall a. (Pointed h, Ok k a) => a `k` h a Source #

Instances

Instances details

Pointed h => IxProductCat (U2 :: Type -> Type -> Type) h Source #
Instance details Defined in ConCat.Category Methods exF :: Ok U2 a => h (U2 (h a) a) Source # forkF :: Ok2 U2 a b => h (U2 a b) -> U2 a (h b) Source # replF :: Ok U2 a => U2 a (h a) Source #
(Representable h, Zip h, Pointed h) => IxProductCat (->) h Source #
Instance details Defined in ConCat.Category Methods exF :: Ok (->) a => h (h a -> a) Source # forkF :: Ok2 (->) a b => h (a -> b) -> a -> h b Source # replF :: Ok (->) a => a -> h a Source #
(IxProductCat k h, IxProductCat k' h, Zip h) => IxProductCat (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods exF :: Ok (k :: k') a => h ((k :: k') (h a) a) Source # forkF :: Ok2 (k :: k') a b => h ((k :: k') a b) -> (k :: k') a (h b) Source # replF :: Ok (k :: k') a => (k :**: k') a (h a) Source #

class (OkFunctor k h, Ok k a) => MinMaxFunctorCat k h a where Source #

Methods

minimumC :: h a `k` a Source #

maximumC :: h a `k` a Source #

Instances

Instances details

MinMax h a => MinMaxFunctorCat (->) h a Source #
Instance details Defined in ConCat.Category Methods minimumC :: h a -> a Source # maximumC :: h a -> a Source #
(MinMaxFunctorCat k h a, MinMaxFunctorCat k' h a) => MinMaxFunctorCat (k :**: k') h a Source #
Instance details Defined in ConCat.Category Methods minimumC :: (k :: k') (h a) a Source # maximumC :: (k :: k') (h a) a Source #

class (OkFunctor k h, Ok k a) => MinMaxFFunctorCat k h a where Source #

Methods

minimumCF :: h a -> a :* (h a `k` a) Source #

maximumCF :: h a -> a :* (h a `k` a) Source #

Instances

Instances details

MinMaxRep h a => MinMaxFFunctorCat (->) h a Source #
Instance details Defined in ConCat.Category Methods minimumCF :: h a -> a :* (h a -> a) Source # maximumCF :: h a -> a :* (h a -> a) Source #
(MinMaxFFunctorCat k h a, MinMaxFFunctorCat k' h a, Ord a) => MinMaxFFunctorCat (k :**: k') h a Source #
Instance details Defined in ConCat.Category Methods minimumCF :: h a -> a :* (k :*: k') (h a) a Source # maximumCF :: h a -> a : (k :**: k') (h a) a Source #

class Additive1 h where Source #

Methods

additive1 :: Sat Additive a |- Sat Additive (h a) Source #

Instances

Instances details

Additive1 Product Source #
Instance details Defined in ConCat.Category Methods additive1 :: Sat Additive a \|- Sat Additive (Product a) Source #
Additive1 Sum Source #
Instance details Defined in ConCat.Category Methods additive1 :: Sat Additive a \|- Sat Additive (Sum a) Source #
Additive1 Par1 Source #
Instance details Defined in ConCat.Category Methods additive1 :: Sat Additive a \|- Sat Additive (Par1 a) Source #
Additive1 (U1 :: Type -> Type) Source #
Instance details Defined in ConCat.Category Methods additive1 :: Sat Additive a \|- Sat Additive (U1 a) Source #
KnownNat n => Additive1 (Vector n) Source #
Instance details Defined in ConCat.Category Methods additive1 :: Sat Additive a \|- Sat Additive (Vector n a) Source #
(AddF f, AddF g) => Additive1 (f :*: g) Source #
Instance details Defined in ConCat.Category Methods additive1 :: Sat Additive a \|- Sat Additive ((f :*: g) a) Source #
Additive1 ((->) a) Source #
Instance details Defined in ConCat.Category Methods additive1 :: Sat Additive a0 \|- Sat Additive (a -> a0) Source #
(AddF f, AddF g) => Additive1 (g :.: f) Source #
Instance details Defined in ConCat.Category Methods additive1 :: Sat Additive a \|- Sat Additive ((g :.: f) a) Source #

class (IxMonoidalPCat k h, OkIxProd k h) => IxCoproductPCat k h where Source #

Indexed coproducts as indexed products.

Minimal complete definition

inPF, (joinPF | jamPF)

Methods

inPF :: forall a. Ok k a => h (a `k` h a) Source #

joinPF :: forall a b. Ok2 k a b => h (b `k` a) -> h b `k` a Source #

default joinPF :: forall a b. (IxMonoidalPCat k h, Ok2 k a b) => h (b `k` a) -> h b `k` a Source #

jamPF :: forall a. Ok k a => h a `k` a Source #

default jamPF :: forall a. (Pointed h, Ok k a) => h a `k` a Source #

Instances

Instances details

Pointed h => IxCoproductPCat (U2 :: Type -> Type -> Type) h Source #
Instance details Defined in ConCat.Category Methods inPF :: Ok U2 a => h (U2 a (h a)) Source # joinPF :: Ok2 U2 a b => h (U2 b a) -> U2 (h b) a Source # jamPF :: Ok U2 a => U2 (h a) a Source #
(IxCoproductPCat k h, IxCoproductPCat k' h, Zip h) => IxCoproductPCat (k :**: k') h Source #
Instance details Defined in ConCat.Category Methods inPF :: Ok (k :: k') a => h ((k :: k') a (h a)) Source # joinPF :: Ok2 (k :: k') a b => h ((k :: k') b a) -> (k :: k') (h b) a Source # jamPF :: Ok (k :: k') a => (k :**: k') (h a) a Source #

class FiniteCat k where Source #

Methods

unFinite :: KnownNat n => Finite n `k` Int Source #

unsafeFinite :: KnownNat n => Int `k` Finite n Source #

Instances

Instances details

FiniteCat (->) Source #
Instance details Defined in ConCat.Category Methods unFinite :: forall (n :: Nat). KnownNat n => Finite n -> Int Source # unsafeFinite :: forall (n :: Nat). KnownNat n => Int -> Finite n Source #
(FiniteCat k, FiniteCat k') => FiniteCat (k :**: k') Source #
Instance details Defined in ConCat.Category Methods unFinite :: forall (n :: Nat). KnownNat n => (k :: k') (Finite n) Int Source # unsafeFinite :: forall (n :: Nat). KnownNat n => (k :: k') Int (Finite n) Source #

AssociativePCat (\|-) Source #
Instance details Defined in ConCat.Category Methods lassocP :: Ok3 (\|-) a b c => Prod (\|-) a (Prod (\|-) b c) \|- Prod (\|-) (Prod (\|-) a b) c Source # rassocP :: Ok3 (\|-) a b c => Prod (\|-) (Prod (\|-) a b) c \|- Prod (\|-) a (Prod (\|-) b c) Source #
BraidedPCat (\|-) Source #
Instance details Defined in ConCat.Category Methods swapP :: Ok2 (\|-) a b => Prod (\|-) a b \|- Prod (\|-) b a Source #
Category (\|-) Source #
Instance details Defined in ConCat.Category Associated Types type Ok (\|-) :: Type -> Constraint Source # Methods id :: Ok (\|-) a => a \|- a Source # (.) :: forall b c a. Ok3 (\|-) a b c => (b \|- c) -> (a \|- b) -> a \|- c Source #
MonoidalPCat (\|-) Source #
Instance details Defined in ConCat.Category Methods (***) :: Ok4 (\|-) a b c d => (a \|- c) -> (b \|- d) -> Prod (\|-) a b \|- Prod (\|-) c d Source # first :: forall a a' b. Ok3 (\|-) a b a' => (a \|- a') -> Prod (\|-) a b \|- Prod (\|-) a' b Source # second :: Ok3 (\|-) a b b' => (b \|- b') -> Prod (\|-) a b \|- Prod (\|-) a b' Source #
ProductCat (\|-) Source #
Instance details Defined in ConCat.Category Methods exl :: Ok2 (\|-) a b => Prod (\|-) a b \|- a Source # exr :: Ok2 (\|-) a b => Prod (\|-) a b \|- b Source # dup :: Ok (\|-) a => a \|- Prod (\|-) a a Source #
Newtype (a \|- b) Source #
Instance details Defined in ConCat.Category Associated Types type O (a \|- b) Source # Methods pack :: O (a \|- b) -> a \|- b Source # unpack :: (a \|- b) -> O (a \|- b) Source #
type Ok (\|-) Source #
Instance details Defined in ConCat.Category type Ok (\|-) = Yes1 :: Type -> Constraint
type O (a \|- b) Source #
Instance details Defined in ConCat.Category type O (a \|- b) = Con a :- Con b