-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Category theory
--   
--   Data-category is a collection of categories, and some categorical
--   constructions on them.
--   
--   You can restrict the types of the objects of your category by using a
--   GADT for the arrow type. To be able to proof to the compiler that a
--   type is an object in some category, objects also need to be
--   represented at the value level. The corresponding identity arrow of
--   the object is used for that.
--   
--   See the <a>Boolean</a> and <a>Product</a> categories for some
--   examples.
--   
--   Note: Strictly speaking this package defines Hask-enriched categories,
--   not ordinary categories (which are Set-enriched.) In practice this
--   means we are allowed to ignore <a>undefined</a> (f.e. when talking
--   about uniqueness of morphisms), and we can treat the categories as
--   normal categories.
@package data-category
@version 0.5.0


module Data.Category

-- | An instance of <tt>Category k</tt> declares the arrow <tt>k</tt> as a
--   category.
class Category k
src :: Category k => k a b -> Obj k a
tgt :: Category k => k a b -> Obj k b
(.) :: Category k => k b c -> k a b -> k a c

-- | Whenever objects are required at value level, they are represented by
--   their identity arrows.
type Obj k a = k a a
data Op k a b
Op :: k b a -> Op k a b
unOp :: Op k a b -> k b a
instance Category k => Category (Op k)
instance Category (->)


module Data.Category.Product
data (:**:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> *
(:**:) :: c1 a1 b1 -> c2 a2 b2 -> :**: c1 c2 (a1, a2) (b1, b2)
instance (Category c1, Category c2) => Category (c1 :**: c2)


module Data.Category.Functor

-- | Functors are arrows in the category Cat.
data Cat :: * -> * -> *
CatA :: ftag -> Cat (CatW (Dom ftag)) (CatW (Cod ftag))

-- | We need a wrapper here because objects need to be of kind *, and
--   categories are of kind * -&gt; * -&gt; *.
data CatW :: (* -> * -> *) -> *

-- | The domain, or source category, of the functor.

-- | The codomain, or target category, of the functor.

-- | Functors map objects and arrows.
class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag
(%) :: Functor ftag => ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)

-- | <tt>:%</tt> maps objects.
data Id (k :: * -> * -> *)
Id :: Id
data (:.:) g h
(:.:) :: g -> h -> g :.: h
data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x
Const :: Obj c2 x -> Const c1 c2 x

-- | The constant functor with the same domain and codomain as f.
type ConstF f = Const (Dom f) (Cod f)
data Opposite f
Opposite :: f -> Opposite f
data OpOp (k :: * -> * -> *)
OpOp :: OpOp
data OpOpInv (k :: * -> * -> *)
OpOpInv :: OpOpInv
data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *)
Proj1 :: Proj1
data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *)
Proj2 :: Proj2
data (:***:) f1 f2
(:***:) :: f1 -> f2 -> :***: f1 f2
data DiagProd (k :: * -> * -> *)
DiagProd :: DiagProd
data Tuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a
Tuple1 :: (Obj c1 a) -> Tuple1 a
data Tuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a
Tuple2 :: (Obj c2 a) -> Tuple2 a
data Hom (k :: * -> * -> *)
Hom :: Hom
type (:*-:) x k = Hom k :.: Tuple1 (Op k) k x

-- | The covariant functor Hom(X,--)
homX_ :: Category k => Obj k x -> x :*-: k
type (:-*:) k x = Hom k :.: Tuple2 (Op k) k x

-- | The contravariant functor Hom(--,X)
hom_X :: Category k => Obj k x -> k :-*: x
instance Category k => Functor (Hom k)
instance (Category c1, Category c2) => Functor (Tuple2 c1 c2 a2)
instance (Category c1, Category c2) => Functor (Tuple1 c1 c2 a1)
instance Category k => Functor (DiagProd k)
instance (Functor f1, Functor f2) => Functor (f1 :***: f2)
instance (Category c1, Category c2) => Functor (Proj2 c1 c2)
instance (Category c1, Category c2) => Functor (Proj1 c1 c2)
instance Category k => Functor (OpOpInv k)
instance Category k => Functor (OpOp k)
instance (Category (Dom f), Category (Cod f)) => Functor (Opposite f)
instance (Category c1, Category c2) => Functor (Const c1 c2 x)
instance (Category (Cod g), Category (Dom h)) => Functor (g :.: h)
instance Category k => Functor (Id k)
instance Category Cat


module Data.Category.NaturalTransformation

-- | <tt>f :~&gt; g</tt> is a natural transformation from functor f to
--   functor g.
type (:~>) f g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g

-- | A component for an object <tt>z</tt> is an arrow from <tt>F z</tt> to
--   <tt>G z</tt>.
type Component f g z = Cod f (f :% z) (g :% z)

-- | A newtype wrapper for components, which can be useful for helper
--   functions dealing with components.
newtype Com f g z
Com :: Component f g z -> Com f g z
unCom :: Com f g z -> Component f g z

-- | 'n ! a' returns the component for the object <tt>a</tt> of a natural
--   transformation <tt>n</tt>. This can be generalized to any arrow
--   (instead of just identity arrows).
(!) :: (Category c, Category d) => Nat c d f g -> c a b -> d (f :% a) (g :% b)

-- | Horizontal composition of natural transformations.
o :: (Category c, Category d, Category e) => Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)

-- | The identity natural transformation of a functor.
natId :: Functor f => f -> Nat (Dom f) (Cod f) f f
srcF :: Nat c d f g -> f
tgtF :: Nat c d f g -> g

-- | Natural transformations are built up of components, one for each
--   object <tt>z</tt> in the domain category of <tt>f</tt> and <tt>g</tt>.
data Nat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> *
Nat :: f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g

-- | The category of endofunctors.
type Endo k = Nat k k
compAssoc :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) => f -> g -> h -> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))
compAssocInv :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) => f -> g -> h -> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)
idPrecomp :: Functor f => f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecompInv :: Functor f => f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPostcomp :: Functor f => f -> Nat (Dom f) (Cod f) (Id (Cod f) :.: f) f
idPostcompInv :: Functor f => f -> Nat (Dom f) (Cod f) f (Id (Cod f) :.: f)
constPrecomp :: (Category c1, Functor f) => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (f :.: Const c1 (Dom f) x) (Const c1 (Cod f) (f :% x))
constPrecompInv :: (Category c1, Functor f) => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (Const c1 (Cod f) (f :% x)) (f :.: Const c1 (Dom f) x)
constPostcomp :: Functor f => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Cod f) c2 x :.: f) (Const (Dom f) c2 x)
constPostcompInv :: Functor f => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Dom f) c2 x) (Const (Cod f) c2 x :.: f)
data FunctorCompose (k :: * -> * -> *)
FunctorCompose :: FunctorCompose
data Precompose :: * -> (* -> * -> *) -> *
Precompose :: f -> Precompose f d
data Postcompose :: * -> (* -> * -> *) -> *
Postcompose :: f -> Postcompose f c
data Wrap f h
Wrap :: f -> h -> Wrap f h
instance (Functor f, Functor h) => Functor (Wrap f h)
instance (Functor f, Category c) => Functor (Postcompose f c)
instance (Functor f, Category d) => Functor (Precompose f d)
instance Category k => Functor (FunctorCompose k)
instance (Category c, Category d) => Category (Nat c d)


module Data.Category.Unit
data Unit a b
Unit :: Unit () ()
instance Category Unit


module Data.Category.Void
data Void a b
magic :: Void a b -> x
voidNat :: (Functor f, Functor g, Category d, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d) => f -> g -> Nat Void d f g
data Magic (k :: * -> * -> *)
Magic :: Magic
instance Category k => Functor (Magic k)
instance Category Void


module Data.Category.Coproduct
data I1 a
data I2 a
data (:++:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> *
I1 :: c1 a1 b1 -> :++: c1 c2 (I1 a1) (I1 b1)
I2 :: c2 a2 b2 -> :++: c1 c2 (I2 a2) (I2 b2)
data Inj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *)
Inj1 :: Inj1
data Inj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *)
Inj2 :: Inj2
data (:+++:) f1 f2
(:+++:) :: f1 -> f2 -> :+++: f1 f2
data CodiagCoprod (k :: * -> * -> *)
CodiagCoprod :: CodiagCoprod
data Cotuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a
Cotuple1 :: (Obj c1 a) -> Cotuple1 a
data Cotuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a
Cotuple2 :: (Obj c2 a) -> Cotuple2 a
data (:>>:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> *
I1A :: c1 a1 b1 -> :>>: c1 c2 (I1 a1) (I1 b1)
I12 :: Obj c1 a -> Obj c2 b -> :>>: c1 c2 (I1 a) (I2 b)
I2A :: c2 a2 b2 -> :>>: c1 c2 (I2 a2) (I2 b2)
data NatAsFunctor f g
NatAsFunctor :: (Nat (Dom f) (Cod f) f g) -> NatAsFunctor f g
instance (Functor f, Functor g, Dom f ~ Dom g, Cod f ~ Cod g) => Functor (NatAsFunctor f g)
instance (Category c1, Category c2) => Category (c1 :>>: c2)
instance (Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2)
instance (Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1)
instance Category k => Functor (CodiagCoprod k)
instance (Functor f1, Functor f2) => Functor (f1 :+++: f2)
instance (Category c1, Category c2) => Functor (Inj2 c1 c2)
instance (Category c1, Category c2) => Functor (Inj1 c1 c2)
instance (Category c1, Category c2) => Category (c1 :++: c2)


module Data.Category.RepresentableFunctor
data Representable f repObj
Representable :: f -> Obj (Dom f) repObj -> (forall k z. (Dom f ~ k, Cod f ~ (->)) => Obj k z -> f :% z -> k repObj z) -> (forall k. (Dom f ~ k, Cod f ~ (->)) => f :% repObj) -> Representable f repObj
representedFunctor :: Representable f repObj -> f
representingObject :: Representable f repObj -> Obj (Dom f) repObj
represent :: Representable f repObj -> forall k z. (Dom f ~ k, Cod f ~ (->)) => Obj k z -> f :% z -> k repObj z
universalElement :: Representable f repObj -> forall k. (Dom f ~ k, Cod f ~ (->)) => f :% repObj
unrepresent :: (Functor f, Dom f ~ k, Cod f ~ (->)) => Representable f repObj -> k repObj z -> f :% z
covariantHomRepr :: Category k => Obj k x -> Representable (x :*-: k) x
contravariantHomRepr :: Category k => Obj k x -> Representable (k :-*: x) x
type InitialUniversal x u a = Representable ((x :*-: Cod u) :.: u) a

-- | An initial universal property, a universal morphism from x to u.
initialUniversal :: Functor u => u -> Obj (Dom u) a -> Cod u x (u :% a) -> (forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y) -> InitialUniversal x u a
type TerminalUniversal x u a = Representable ((Cod u :-*: x) :.: Opposite u) a

-- | A terminal universal property, a universal morphism from u to x.
terminalUniversal :: Functor u => u -> Obj (Dom u) a -> Cod u (u :% a) x -> (forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a) -> TerminalUniversal x u a


module Data.Category.Adjunction
data Adjunction c d f g
Adjunction :: f -> g -> Nat d d (Id d) (g :.: f) -> Nat c c (f :.: g) (Id c) -> Adjunction c d f g
leftAdjoint :: Adjunction c d f g -> f
rightAdjoint :: Adjunction c d f g -> g
unit :: Adjunction c d f g -> Nat d d (Id d) (g :.: f)
counit :: Adjunction c d f g -> Nat c c (f :.: g) (Id c)
mkAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall a. Obj d a -> Component (Id d) (g :.: f) a) -> (forall a. Obj c a -> Component (f :.: g) (Id c) a) -> Adjunction c d f g
leftAdjunct :: Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
rightAdjunct :: Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
idAdj :: Category k => Adjunction k k (Id k) (Id k)
composeAdj :: Adjunction d e f g -> Adjunction c d f' g' -> Adjunction c e (f' :.: f) (g :.: g')
data AdjArrow c d
AdjArrow :: Adjunction c d f g -> AdjArrow (CatW c) (CatW d)
initialPropAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall y. Obj d y -> InitialUniversal y g (f :% y)) -> Adjunction c d f g
terminalPropAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall x. Obj c x -> TerminalUniversal x f (g :% x)) -> Adjunction c d f g
adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)
adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)
contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r)
instance Category AdjArrow


module Data.Category.Limit
data Diag :: (* -> * -> *) -> (* -> * -> *) -> *
Diag :: Diag j k

-- | The diagonal functor with the same domain and codomain as <tt>f</tt>.
type DiagF f = Diag (Dom f) (Cod f)

-- | A cone from N to F is a natural transformation from the constant
--   functor to N to F.
type Cone f n = Nat (Dom f) (Cod f) (ConstF f n) f

-- | A co-cone from F to N is a natural transformation from F to the
--   constant functor to N.
type Cocone f n = Nat (Dom f) (Cod f) f (ConstF f n)

-- | The vertex (or apex) of a cone.
coneVertex :: Cone f n -> Obj (Cod f) n

-- | The vertex (or apex) of a co-cone.
coconeVertex :: Cocone f n -> Obj (Cod f) n

-- | Limits in a category <tt>k</tt> by means of a diagram of type
--   <tt>j</tt>, which is a functor from <tt>j</tt> to <tt>k</tt>.
type Limit f = LimitFam (Dom f) (Cod f) f

-- | An instance of <tt>HasLimits j k</tt> says that <tt>k</tt> has all
--   limits of type <tt>j</tt>.
class (Category j, Category k) => HasLimits j k
limit :: HasLimits j k => Obj (Nat j k) f -> Cone f (Limit f)
limitFactorizer :: HasLimits j k => Obj (Nat j k) f -> (forall n. Cone f n -> k n (Limit f))
data LimitFunctor (j :: * -> * -> *) (k :: * -> * -> *)
LimitFunctor :: LimitFunctor

-- | The limit functor is right adjoint to the diagonal functor.
limitAdj :: HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)

-- | Colimits in a category <tt>k</tt> by means of a diagram of type
--   <tt>j</tt>, which is a functor from <tt>j</tt> to <tt>k</tt>.
type Colimit f = ColimitFam (Dom f) (Cod f) f

-- | An instance of <tt>HasColimits j k</tt> says that <tt>k</tt> has all
--   colimits of type <tt>j</tt>.
class (Category j, Category k) => HasColimits j k
colimit :: HasColimits j k => Obj (Nat j k) f -> Cocone f (Colimit f)
colimitFactorizer :: HasColimits j k => Obj (Nat j k) f -> (forall n. Cocone f n -> k (Colimit f) n)
data ColimitFunctor (j :: * -> * -> *) (k :: * -> * -> *)
ColimitFunctor :: ColimitFunctor

-- | The colimit functor is left adjoint to the diagonal functor.
colimitAdj :: HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
class Category k => HasTerminalObject k where type family TerminalObject k :: *
terminalObject :: HasTerminalObject k => Obj k (TerminalObject k)
terminate :: HasTerminalObject k => Obj k a -> k a (TerminalObject k)
class Category k => HasInitialObject k where type family InitialObject k :: *
initialObject :: HasInitialObject k => Obj k (InitialObject k)
initialize :: HasInitialObject k => Obj k a -> k (InitialObject k) a
data Zero
class Category k => HasBinaryProducts k where l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r))
proj1 :: HasBinaryProducts k => Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj2 :: HasBinaryProducts k => Obj k x -> Obj k y -> k (BinaryProduct k x y) y
(&&&) :: HasBinaryProducts k => (k a x) -> (k a y) -> (k a (BinaryProduct k x y))
(***) :: HasBinaryProducts k => (k a1 b1) -> (k a2 b2) -> (k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2))
data ProductFunctor (k :: * -> * -> *)
ProductFunctor :: ProductFunctor
data (:*:) p q
(:*:) :: p -> q -> p :*: q
class Category k => HasBinaryCoproducts k where l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r)
inj1 :: HasBinaryCoproducts k => Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj2 :: HasBinaryCoproducts k => Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
(|||) :: HasBinaryCoproducts k => (k x a) -> (k y a) -> (k (BinaryCoproduct k x y) a)
(+++) :: HasBinaryCoproducts k => (k a1 b1) -> (k a2 b2) -> (k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2))
data CoproductFunctor (k :: * -> * -> *)
CoproductFunctor :: CoproductFunctor
data (:+:) p q
(:+:) :: p -> q -> p :+: q
instance (HasTerminalObject (i :>>: j), Category k) => HasColimits (i :>>: j) k
instance Category k => HasColimits Unit k
instance (HasInitialObject (i :>>: j), Category k) => HasLimits (i :>>: j) k
instance Category k => HasLimits Unit k
instance HasBinaryProducts k => HasBinaryCoproducts (Op k)
instance HasBinaryCoproducts k => HasBinaryProducts (Op k)
instance HasTerminalObject k => HasInitialObject (Op k)
instance HasInitialObject k => HasTerminalObject (Op k)
instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d)
instance (Category (Dom p), Category (Cod p)) => Functor (p :+: q)
instance HasBinaryCoproducts k => Functor (CoproductFunctor k)
instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :>>: c2)
instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2)
instance HasBinaryCoproducts Unit
instance HasBinaryCoproducts Cat
instance (HasColimits i k, HasColimits j k, HasBinaryCoproducts k) => HasColimits (i :++: j) k
instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d)
instance (Category (Dom p), Category (Cod p)) => Functor (p :*: q)
instance HasBinaryProducts k => Functor (ProductFunctor k)
instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :>>: c2)
instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2)
instance HasBinaryProducts Unit
instance HasBinaryProducts Cat
instance HasBinaryProducts (->)
instance (HasLimits i k, HasLimits j k, HasBinaryProducts k) => HasLimits (i :++: j) k
instance (HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2)
instance HasInitialObject Unit
instance (HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2)
instance (Category c, HasInitialObject d) => HasInitialObject (Nat c d)
instance HasInitialObject Cat
instance HasInitialObject (->)
instance HasInitialObject k => HasColimits Void k
instance (Category c1, HasTerminalObject c2) => HasTerminalObject (c1 :>>: c2)
instance (HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (c1 :**: c2)
instance HasTerminalObject Unit
instance (Category c, HasTerminalObject d) => HasTerminalObject (Nat c d)
instance HasTerminalObject Cat
instance HasTerminalObject (->)
instance HasTerminalObject k => HasLimits Void k
instance HasColimits j k => Functor (ColimitFunctor j k)
instance HasLimits j k => Functor (LimitFunctor j k)
instance (Category j, Category k) => Functor (Diag j k)


module Data.Category.Monoidal

-- | A monoidal category is a category with some kind of tensor product. A
--   tensor product is a bifunctor, with a unit object.
class (Functor f, Dom f ~ (Cod f :**: Cod f)) => TensorProduct f where type family Unit f :: *
unitObject :: TensorProduct f => f -> Obj (Cod f) (Unit f)
leftUnitor :: (TensorProduct f, Cod f ~ k) => f -> Obj k a -> k (f :% (Unit f, a)) a
leftUnitorInv :: (TensorProduct f, Cod f ~ k) => f -> Obj k a -> k a (f :% (Unit f, a))
rightUnitor :: (TensorProduct f, Cod f ~ k) => f -> Obj k a -> k (f :% (a, Unit f)) a
rightUnitorInv :: (TensorProduct f, Cod f ~ k) => f -> Obj k a -> k a (f :% (a, Unit f))
associator :: (TensorProduct f, Cod f ~ k) => f -> Obj k a -> Obj k b -> Obj k c -> k (f :% (f :% (a, b), c)) (f :% (a, f :% (b, c)))
associatorInv :: (TensorProduct f, Cod f ~ k) => f -> Obj k a -> Obj k b -> Obj k c -> k (f :% (a, f :% (b, c))) (f :% (f :% (a, b), c))

-- | <tt>MonoidObject f a</tt> defines a monoid <tt>a</tt> in a monoidal
--   category with tensor product <tt>f</tt>.
data MonoidObject f a
MonoidObject :: (forall k. Cod f ~ k => k (Unit f) a) -> (forall k. Cod f ~ k => k ((f :% (a, a))) a) -> MonoidObject f a
unit :: MonoidObject f a -> forall k. Cod f ~ k => k (Unit f) a
multiply :: MonoidObject f a -> forall k. Cod f ~ k => k ((f :% (a, a))) a

-- | <tt>ComonoidObject f a</tt> defines a comonoid <tt>a</tt> in a
--   comonoidal category with tensor product <tt>f</tt>.
data ComonoidObject f a
ComonoidObject :: (forall k. Cod f ~ k => k a (Unit f)) -> (forall k. Cod f ~ k => k a (f :% (a, a))) -> ComonoidObject f a
counit :: ComonoidObject f a -> forall k. Cod f ~ k => k a (Unit f)
comultiply :: ComonoidObject f a -> forall k. Cod f ~ k => k a (f :% (a, a))
data MonoidAsCategory f m a b
MonoidValue :: f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m m

-- | A monad is a monoid in the category of endofunctors.
type Monad f = MonoidObject (FunctorCompose (Dom f)) f
mkMonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k) => f -> (forall a. Obj k a -> Component (Id k) f a) -> (forall a. Obj k a -> Component (f :.: f) f a) -> Monad f
monadFunctor :: Monad f -> f

-- | A comonad is a comonoid in the category of endofunctors.
type Comonad f = ComonoidObject (FunctorCompose (Dom f)) f
mkComonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k) => f -> (forall a. Obj k a -> Component f (Id k) a) -> (forall a. Obj k a -> Component f (f :.: f) a) -> Comonad f

-- | Every adjunction gives rise to an associated monad.
adjunctionMonad :: Adjunction c d f g -> Monad (g :.: f)

-- | Every adjunction gives rise to an associated comonad.
adjunctionComonad :: Adjunction c d f g -> Comonad (f :.: g)
instance Category (MonoidAsCategory f m)
instance Category k => TensorProduct (FunctorCompose k)
instance (HasInitialObject k, HasBinaryCoproducts k) => TensorProduct (CoproductFunctor k)
instance (HasTerminalObject k, HasBinaryProducts k) => TensorProduct (ProductFunctor k)


module Data.Category.CartesianClosed

-- | A category is cartesian closed if it has all products and exponentials
--   for all objects.
class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k
apply :: CartesianClosed k => Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
tuple :: CartesianClosed k => Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
(^^^) :: CartesianClosed k => k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
data ExpFunctor (k :: * -> * -> *)
ExpFunctor :: ExpFunctor
data Apply (y :: * -> * -> *) (z :: * -> * -> *)
Apply :: Apply
data ToTuple1 (y :: * -> * -> *) (z :: * -> * -> *)
ToTuple1 :: ToTuple1
data ToTuple2 (y :: * -> * -> *) (z :: * -> * -> *)
ToTuple2 :: ToTuple2

-- | The product functor is left adjoint the the exponential functor.
curryAdj :: CartesianClosed k => Obj k y -> Adjunction k k (ProductFunctor k :.: Tuple2 k k y) (ExpFunctor k :.: Tuple1 (Op k) k y)

-- | From the adjunction between the product functor and the exponential
--   functor we get the curry and uncurry functions, generalized to any
--   cartesian closed category.
curry :: CartesianClosed k => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z)
uncurry :: CartesianClosed k => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) z

-- | From every adjunction we get a monad, in this case the State monad.
type State k s a = Exponential k s (BinaryProduct k a s)
stateMonadReturn :: CartesianClosed k => Obj k s -> Obj k a -> k a (State k s a)
stateMonadJoin :: CartesianClosed k => Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a)
type Context k s a = BinaryProduct k (Exponential k s a) s
contextComonadExtract :: CartesianClosed k => Obj k s -> Obj k a -> k (Context k s a) a
contextComonadDuplicate :: CartesianClosed k => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a))
instance CartesianClosed Cat
instance (Category y, Category z) => Functor (ToTuple2 y z)
instance (Category y, Category z) => Functor (ToTuple1 y z)
instance (Category y, Category z) => Functor (Apply y z)
instance CartesianClosed (->)
instance CartesianClosed k => Functor (ExpFunctor k)


module Data.Category.Yoneda
type YonedaEmbedding k = Postcompose (Hom k) (Op k) :.: ToTuple2 k (Op k)

-- | The Yoneda embedding functor, <tt>C -&gt; Set^(C^op)</tt>.
yonedaEmbedding :: Category k => YonedaEmbedding k
data Yoneda (k :: * -> * -> *) f
Yoneda :: Yoneda f

-- | <a>fromYoneda</a> and <a>toYoneda</a> are together the isomophism from
--   the Yoneda lemma.
fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Yoneda k f :~> f
toYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> f :~> Yoneda k f
instance (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => Functor (Yoneda k f)


module Data.Category.Presheaf
type Presheaves k = Nat (Op k) (->)
type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite ((ProductFunctor (Presheaves k) :.: Tuple2 (Presheaves k) (Presheaves k) y) :.: YonedaEmbedding k)
pshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z
instance Category k => CartesianClosed (Presheaves k)


-- | <i>2</i>, or the Boolean category. It contains 2 objects, one for true
--   and one for false. It contains 3 arrows, 2 identity arrows and one
--   from false to true.
module Data.Category.Boolean
data Fls
data Tru
data Boolean a b
Fls :: Boolean Fls Fls
F2T :: Boolean Fls Tru
Tru :: Boolean Tru Tru
trueProductMonoid :: MonoidObject (ProductFunctor Boolean) Tru
falseCoproductComonoid :: ComonoidObject (CoproductFunctor Boolean) Fls
trueProductComonoid :: ComonoidObject (ProductFunctor Boolean) Tru
falseCoproductMonoid :: MonoidObject (CoproductFunctor Boolean) Fls
trueCoproductMonoid :: MonoidObject (CoproductFunctor Boolean) Tru
falseProductComonoid :: ComonoidObject (ProductFunctor Boolean) Fls
instance CartesianClosed Boolean
instance HasBinaryCoproducts Boolean
instance HasBinaryProducts Boolean
instance HasTerminalObject Boolean
instance HasInitialObject Boolean
instance Category Boolean


module Data.Category.Fix
newtype Fix f a b
Fix :: (f (Fix f) a b) -> Fix f a b
data Wrap (f :: (* -> * -> *) -> * -> * -> *)
Wrap :: Wrap

-- | Take the <a>Omega</a> category, add a new disctinct object, and an
--   arrow from that object to every object in <a>Omega</a>, and you get
--   <a>Omega</a> again.
type Omega = Fix (:>>: Unit)
instance Category (f (Fix f)) => Functor (Wrap f)
instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f)
instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f)
instance HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f)
instance HasInitialObject (f (Fix f)) => HasInitialObject (Fix f)
instance Category (f (Fix f)) => Category (Fix f)


-- | This is an attempt at the Kleisli category, and the construction of an
--   adjunction for each monad.
module Data.Category.Kleisli
data Kleisli m a b
Kleisli :: Monad m -> Obj k b -> k a (m :% b) -> Kleisli m a b
kleisliId :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj k a -> Kleisli m a a
data KleisliAdjF m
KleisliAdjF :: (Monad m) -> KleisliAdjF m
data KleisliAdjG m
KleisliAdjG :: (Monad m) -> KleisliAdjG m
kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Adjunction (Kleisli m) k (KleisliAdjF m) (KleisliAdjG m)
instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjG m)
instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjF m)
instance Category (Kleisli m)


-- | Dialg(F,G), the category of (F,G)-dialgebras and (F,G)-homomorphisms.
module Data.Category.Dialg

-- | Objects of Dialg(F,G) are (F,G)-dialgebras.
data Dialgebra f g a
Dialgebra :: Obj c a -> d (f :% a) (g :% a) -> Dialgebra f g a

-- | Arrows of Dialg(F,G) are (F,G)-homomorphisms.
data Dialg f g a b
DialgA :: Dialgebra f g a -> Dialgebra f g b -> c a b -> Dialg f g a b
dialgId :: Dialgebra f g a -> Obj (Dialg f g) a
dialgebra :: Obj (Dialg f g) a -> Dialgebra f g a
type Alg f = Dialg f (Id (Dom f))
type Algebra f a = Dialgebra f (Id (Dom f)) a
type Coalg f = Dialg (Id (Dom f)) f
type Coalgebra f a = Dialgebra (Id (Dom f)) f a

-- | The initial F-algebra is the initial object in the category of
--   F-algebras.
type InitialFAlgebra f = InitialObject (Alg f)

-- | The terminal F-coalgebra is the terminal object in the category of
--   F-coalgebras.
type TerminalFAlgebra f = TerminalObject (Coalg f)

-- | A catamorphism of an F-algebra is the arrow to it from the initial
--   F-algebra.
type Cata f a = Algebra f a -> Alg f (InitialFAlgebra f) a

-- | A anamorphism of an F-coalgebra is the arrow from it to the terminal
--   F-coalgebra.
type Ana f a = Coalgebra f a -> Coalg f a (TerminalFAlgebra f)
data NatNum
Z :: () -> NatNum
S :: NatNum -> NatNum
primRec :: (() -> t) -> (t -> t) -> NatNum -> t
data FreeAlg m
FreeAlg :: (Monad m) -> FreeAlg m
data ForgetAlg m
ForgetAlg :: ForgetAlg m
eilenbergMooreAdj :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Adjunction (Alg m) k (FreeAlg m) (ForgetAlg m)
instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (ForgetAlg m)
instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (FreeAlg m)
instance HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))
instance Category (Dialg f g)


module Data.Category.NNO
class HasTerminalObject k => HasNaturalNumberObject k where type family NaturalNumberObject k :: *
zero :: HasNaturalNumberObject k => k (TerminalObject k) (NaturalNumberObject k)
succ :: HasNaturalNumberObject k => k (NaturalNumberObject k) (NaturalNumberObject k)
primRec :: HasNaturalNumberObject k => k (TerminalObject k) a -> k a a -> k (NaturalNumberObject k) a
data NatNum
Z :: NatNum
S :: NatNum -> NatNum
type Nat = Fix (:++: Unit)
data PrimRec z s
PrimRec :: z -> s -> PrimRec z s
instance (Functor z, Functor s, Dom z ~ Unit, Cod z ~ Dom s, Dom s ~ Cod s) => Functor (PrimRec z s)
instance HasNaturalNumberObject Cat
instance HasNaturalNumberObject (->)


-- | The (augmented) simplex category.
module Data.Category.Simplex
data Simplex :: * -> * -> *
Z :: Simplex Z Z
Y :: Simplex x y -> Simplex x (S y)
X :: Simplex x (S y) -> Simplex (S x) (S y)
data Z
data S n
suc :: Obj Simplex n -> Obj Simplex (S n)
data Forget
Forget :: Forget
data Fin :: * -> *
Fz :: Fin (S n)
Fs :: Fin n -> Fin (S n)
data Add
Add :: Add

-- | The maps <tt>0 -&gt; 1</tt> and <tt>2 -&gt; 1</tt> form a monoid,
--   which is universal, c.f. <a>Replicate</a>.
universalMonoid :: MonoidObject (CoproductFunctor Simplex) (S Z)
data Replicate f a
Replicate :: f -> (MonoidObject f a) -> Replicate f a
instance TensorProduct f => Functor (Replicate f a)
instance TensorProduct Add
instance Functor Add
instance Functor Forget
instance HasBinaryCoproducts Simplex
instance HasTerminalObject Simplex
instance HasInitialObject Simplex
instance Category Simplex


-- | Comma categories.
module Data.Category.Comma
data CommaO :: * -> * -> * -> *
CommaO :: Obj (Dom t) a -> k (t :% a) (s :% b) -> Obj (Dom s) b -> CommaO t s (a, b)
data (:/\:) :: * -> * -> * -> * -> *
CommaA :: CommaO t s (a, b) -> Dom t a a' -> Dom s b b' -> CommaO t s (a', b') -> (t :/\: s) (a, b) (a', b')
commaId :: CommaO t s (a, b) -> Obj (t :/\: s) (a, b)
type ObjectsFUnder f a = ConstF f a :/\: f
type ObjectsFOver f a = f :/\: ConstF f a
type ObjectsUnder c a = Id c ObjectsFUnder a
type ObjectsOver c a = Id c ObjectsFOver a
initialUniversalComma :: (Functor u, c ~ (u ObjectsFUnder x), HasInitialObject c, (a_, a) ~ InitialObject c) => u -> InitialUniversal x u a
terminalUniversalComma :: (Functor u, c ~ (u ObjectsFOver x), HasTerminalObject c, (a, a_) ~ TerminalObject c) => u -> TerminalUniversal x u a
instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s)