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


-- | Restricted categories
--   
--   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>Monoid</a>, <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.4


module Data.Category

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

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

-- | The identity functor on (~&gt;)
data Id ~> :: (* -> * -> *)
Id :: Id

-- | The composition of two functors.
data (:.:) g h
(:.:) :: g -> h -> g :.: h

-- | The constant functor.
data Const c1 :: (* -> * -> *) c2 :: (* -> * -> *) x
Const :: Obj c2 x -> Const c1 c2 x
type ConstF f = Const (Dom f) (Cod f)

-- | The dual of a functor
data Opposite f
Opposite :: f -> Opposite f

-- | <a>EndoHask</a> is a wrapper to turn instances of the <a>Functor</a>
--   class into categorical functors.
data EndoHask :: (* -> *) -> *
EndoHask :: EndoHask f

-- | <a>Proj1</a> is a bifunctor that projects out the first component of a
--   product.
data Proj1 c1 :: (* -> * -> *) c2 :: (* -> * -> *)
Proj1 :: Proj1

-- | <a>Proj2</a> is a bifunctor that projects out the second component of
--   a product.
data Proj2 c1 :: (* -> * -> *) c2 :: (* -> * -> *)
Proj2 :: Proj2

-- | <tt>f1 :***: f2</tt> is the product of the functors <tt>f1</tt> and
--   <tt>f2</tt>.
data (:***:) f1 f2
(:***:) :: f1 -> f2 -> :***: f1 f2

-- | <a>DiagProd</a> is the diagonal functor for products.
data DiagProd ~> :: (* -> * -> *)
DiagProd :: DiagProd

-- | <a>Tuple1</a> tuples with a fixed object on the left.
data Tuple1 c1 :: (* -> * -> *) c2 :: (* -> * -> *) a
Tuple1 :: (Obj c1 a) -> Tuple1 a

-- | <a>Tuple2</a> tuples with a fixed object on the right.
data Tuple2 c1 :: (* -> * -> *) c2 :: (* -> * -> *) a
Tuple2 :: (Obj c2 a) -> Tuple2 a

-- | The Hom functor, Hom(,), a bifunctor contravariant in its first
--   argument and covariant in its second argument.
data Hom ~> :: (* -> * -> *)
Hom :: Hom
type :*-: x ~> = Hom ~> :.: Tuple1 (Op ~>) ~> x

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

-- | The contravariant functor Hom(,X)
hom_X :: Category ~> => Obj ~> x -> ~> :-*: x
instance Category (~>) => Functor (Hom (~>))
instance (Category c1, Category c2) => Functor (Tuple2 c1 c2 a2)
instance (Category c1, Category c2) => Functor (Tuple1 c1 c2 a1)
instance Category (~>) => Functor (DiagProd (~>))
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 Functor (EndoHask f)
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 (~>) => Functor (Id (~>))
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 ~> = Nat ~> ~>
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)

-- | Composition of endofunctors is a functor.
data FunctorCompose ~> :: (* -> * -> *)
FunctorCompose :: FunctorCompose

-- | <tt>Precompose f d</tt> is the functor such that <tt>Precompose f d :%
--   g = g :.: f</tt>, for functors <tt>g</tt> that compose with <tt>f</tt>
--   and with codomain <tt>d</tt>.
data Precompose :: * -> (* -> * -> *) -> *
Precompose :: f -> Precompose f d

-- | <tt>Postcompose f c</tt> is the functor such that <tt>Postcompose f c
--   :% g = f :.: g</tt>, for functors <tt>g</tt> that compose with
--   <tt>f</tt> and with domain <tt>c</tt>.
data Postcompose :: * -> (* -> * -> *) -> *
Postcompose :: f -> Postcompose f c

-- | <tt>Wrap f h</tt> is the functor such that <tt>Wrap f h :% g = f :.: g
--   :.: h</tt>, for functors <tt>g</tt> that compose with <tt>f</tt> and
--   <tt>h</tt>.
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 (~>) => Functor (FunctorCompose (~>))
instance (Category c, Category d) => Category (Nat c d)


module Data.Category.RepresentableFunctor
data Representable f repObj
Representable :: f -> Obj (Dom f) repObj -> (forall ~> z. ((Dom f) ~ ~>, (Cod f) ~ (->)) => Obj ~> z -> f :% z -> repObj ~> z) -> (forall ~>. ((Dom f) ~ ~>, (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 ~> z. ((Dom f) ~ ~>, (Cod f) ~ (->)) => Obj ~> z -> f :% z -> repObj ~> z
universalElement :: Representable f repObj -> forall ~>. ((Dom f) ~ ~>, (Cod f) ~ (->)) => f :% repObj
unrepresent :: (Functor f, (Dom f) ~ ~>, (Cod f) ~ (->)) => Representable f repObj -> repObj ~> z -> f :% z
covariantHomRepr :: Category ~> => Obj ~> x -> Representable (x :*-: ~>) x
contravariantHomRepr :: Category ~> => Obj ~> x -> Representable (~> :-*: 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
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 (->)) (->) (Cont1 r) (Cont2 r)
instance Functor (Cont2 r)
instance Functor (Cont1 r)
instance Category AdjArrow


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 ~> :: (* -> * -> *)
CodiagCoprod :: CodiagCoprod
data Cotuple1 c1 :: (* -> * -> *) c2 :: (* -> * -> *) a
Cotuple1 :: (Obj c1 a) -> Cotuple1 a
data Cotuple2 c1 :: (* -> * -> *) c2 :: (* -> * -> *) a
Cotuple2 :: (Obj c2 a) -> Cotuple2 a
instance (Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2)
instance (Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1)
instance Category (~>) => Functor (CodiagCoprod (~>))
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)


-- | Discrete n, the category with n objects, and as the only arrows their
--   identities.
module Data.Category.Discrete

-- | The arrows in Discrete n, a finite set of identity arrows.
data Discrete :: * -> * -> * -> *
Z :: Discrete (S n) Z Z
S :: Discrete n a a -> Discrete (S n) (S a) (S a)
data Z
data S n

-- | <tt>Void</tt> is the empty category.
type Void = Discrete Z

-- | <tt>Unit</tt> is the discrete category with one object.
type Unit = Discrete (S Z)

-- | <tt>Pair</tt> is the discrete category with two objects.
type Pair = Discrete (S (S Z))
magicZ :: Discrete Z a b -> x
data Succ n
Succ :: Succ n

-- | The functor from <tt>Discrete n</tt> to <tt>(~&gt;)</tt>, a diagram of
--   <tt>n</tt> objects in <tt>(~&gt;)</tt>.
data DiscreteDiagram :: (* -> * -> *) -> * -> * -> *
Nil :: DiscreteDiagram ~> Z ()
(:::) :: Obj ~> x -> DiscreteDiagram ~> n xs -> DiscreteDiagram ~> (S n) (x, xs)
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
instance (Category (~>), Category (Discrete n), Functor (DiscreteDiagram (~>) n xs)) => Functor (DiscreteDiagram (~>) (S n) (x, xs))
instance Category (~>) => Functor (DiscreteDiagram (~>) Z ())
instance Category (Discrete n) => Functor (Succ n)
instance Category (Discrete n) => Category (Discrete (S n))
instance Category (Discrete Z)


module Data.Category.Limit

-- | The diagonal functor from (index-) category J to (~&gt;).
data Diag :: (* -> * -> *) -> (* -> * -> *) -> *
Diag :: Diag j ~>

-- | 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>(~&gt;)</tt> by means of a diagram of type
--   <tt>j</tt>, which is a functor from <tt>j</tt> to <tt>(~&gt;)</tt>.
type Limit f = LimitFam (Dom f) (Cod f) f

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

-- | If every diagram of type <tt>j</tt> has a limit in <tt>(~&gt;)</tt>
--   there exists a limit functor.
--   
--   Applied to a natural transformation it is a generalisation of
--   <tt>(***)</tt>:
--   
--   <tt>l</tt> <a>***</a> <tt>r =</tt> <a>LimitFunctor</a> <a>%</a>
--   <tt>arrowPair</tt> <tt>l r</tt>
data LimitFunctor j :: (* -> * -> *) ~> :: (* -> * -> *)
LimitFunctor :: LimitFunctor

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

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

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

-- | If every diagram of type <tt>j</tt> has a colimit in <tt>(~&gt;)</tt>
--   there exists a colimit functor.
--   
--   Applied to a natural transformation it is a generalisation of
--   <tt>(+++)</tt>:
--   
--   <tt>l</tt> <a>+++</a> <tt>r =</tt> <a>ColimitFunctor</a> <a>%</a>
--   <tt>arrowPair</tt> <tt>l r</tt>
data ColimitFunctor j :: (* -> * -> *) ~> :: (* -> * -> *)
ColimitFunctor :: ColimitFunctor

-- | The colimit functor is left adjoint to the diagonal functor.
colimitAdj :: HasColimits j ~> => Adjunction ~> (Nat j ~>) (ColimitFunctor j ~>) (Diag j ~>)

-- | A terminal object is the limit of the functor from <i>0</i> to
--   (~&gt;).
class Category ~> => HasTerminalObject ~> where { type family TerminalObject ~> :: *; }
terminalObject :: HasTerminalObject ~> => Obj ~> (TerminalObject ~>)
terminate :: HasTerminalObject ~> => Obj ~> a -> a ~> TerminalObject ~>

-- | An initial object is the colimit of the functor from <i>0</i> to
--   (~&gt;).
class Category ~> => HasInitialObject ~> where { type family InitialObject ~> :: *; }
initialObject :: HasInitialObject ~> => Obj ~> (InitialObject ~>)
initialize :: HasInitialObject ~> => Obj ~> a -> InitialObject ~> ~> a
data Zero

-- | The product of 2 objects is the limit of the functor from Pair to
--   (~&gt;).
class Category ~> => HasBinaryProducts ~>
proj1 :: HasBinaryProducts ~> => Obj ~> x -> Obj ~> y -> BinaryProduct ~> x y ~> x
proj2 :: HasBinaryProducts ~> => Obj ~> x -> Obj ~> y -> BinaryProduct ~> x y ~> y
(&&&) :: HasBinaryProducts ~> => (a ~> x) -> (a ~> y) -> (a ~> BinaryProduct ~> x y)
(***) :: HasBinaryProducts ~> => (a1 ~> b1) -> (a2 ~> b2) -> (BinaryProduct ~> a1 a2 ~> BinaryProduct ~> b1 b2)

-- | Binary product as a bifunctor.
data ProductFunctor ~> :: (* -> * -> *)
ProductFunctor :: ProductFunctor

-- | The product of two functors.
data (:*:) p q
(:*:) :: p -> q -> p :*: q

-- | The coproduct of 2 objects is the colimit of the functor from Pair to
--   (~&gt;).
class Category ~> => HasBinaryCoproducts ~>
inj1 :: HasBinaryCoproducts ~> => Obj ~> x -> Obj ~> y -> x ~> BinaryCoproduct ~> x y
inj2 :: HasBinaryCoproducts ~> => Obj ~> x -> Obj ~> y -> y ~> BinaryCoproduct ~> x y
(|||) :: HasBinaryCoproducts ~> => (x ~> a) -> (y ~> a) -> (BinaryCoproduct ~> x y ~> a)
(+++) :: HasBinaryCoproducts ~> => (a1 ~> b1) -> (a2 ~> b2) -> (BinaryCoproduct ~> a1 a2 ~> BinaryCoproduct ~> b1 b2)

-- | Binary coproduct as a bifunctor.
data CoproductFunctor ~> :: (* -> * -> *)
CoproductFunctor :: CoproductFunctor

-- | The coproduct of two functors.
data (:+:) p q
(:+:) :: p -> q -> p :+: q
instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d)
instance (Category (Dom p), Category (Cod p)) => Functor (p :+: q)
instance HasBinaryCoproducts (~>) => Functor (CoproductFunctor (~>))
instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2)
instance HasBinaryCoproducts Cat
instance HasBinaryCoproducts (->)
instance (HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>)) => HasColimits (Discrete (S n)) (~>)
instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d)
instance (Category (Dom p), Category (Cod p)) => Functor (p :*: q)
instance HasBinaryProducts (~>) => Functor (ProductFunctor (~>))
instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2)
instance HasBinaryProducts Cat
instance HasBinaryProducts (->)
instance (HasLimits (Discrete n) (~>), HasBinaryProducts (~>)) => HasLimits (Discrete (S n)) (~>)
instance (HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2)
instance (Category c, HasInitialObject d) => HasInitialObject (Nat c d)
instance HasInitialObject Cat
instance HasInitialObject (->)
instance HasInitialObject (~>) => HasColimits Void (~>)
instance (HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (c1 :**: c2)
instance (Category c, HasTerminalObject d) => HasTerminalObject (Nat c d)
instance HasTerminalObject Cat
instance HasTerminalObject (->)
instance HasTerminalObject (~>) => HasLimits Void (~>)
instance HasColimits j (~>) => Functor (ColimitFunctor j (~>))
instance HasLimits j (~>) => Functor (LimitFunctor j (~>))
instance (Category j, Category (~>)) => Functor (Diag j (~>))


module Data.Category.Monoidal
class Functor f => HasUnit f where { type family Unit f :: *; }
unitObject :: HasUnit f => f -> Obj (Cod f) (Unit f)
class HasUnit f => TensorProduct f
leftUnitor :: (TensorProduct f, (Cod f) ~ ~>) => f -> Obj ~> a -> (f :% (Unit f, a)) ~> a
leftUnitorInv :: (TensorProduct f, (Cod f) ~ ~>) => f -> Obj ~> a -> a ~> (f :% (Unit f, a))
rightUnitor :: (TensorProduct f, (Cod f) ~ ~>) => f -> Obj ~> a -> (f :% (a, Unit f)) ~> a
rightUnitorInv :: (TensorProduct f, (Cod f) ~ ~>) => f -> Obj ~> a -> a ~> (f :% (a, Unit f))
associator :: (TensorProduct f, (Cod f) ~ ~>) => f -> Obj ~> a -> Obj ~> b -> Obj ~> c -> (f :% (f :% (a, b), c)) ~> (f :% (a, f :% (b, c)))
associatorInv :: (TensorProduct f, (Cod f) ~ ~>) => f -> Obj ~> a -> Obj ~> b -> Obj ~> c -> (f :% (a, f :% (b, c))) ~> (f :% (f :% (a, b), c))
data MonoidObject f a
MonoidObject :: (forall ~>. (Cod f) ~ ~> => Unit f ~> a) -> (forall ~>. (Cod f) ~ ~> => (f :% (a, a)) ~> a) -> MonoidObject f a
unit :: MonoidObject f a -> forall ~>. (Cod f) ~ ~> => Unit f ~> a
multiply :: MonoidObject f a -> forall ~>. (Cod f) ~ ~> => (f :% (a, a)) ~> a
data ComonoidObject f a
ComonoidObject :: (forall ~>. (Cod f) ~ ~> => a ~> Unit f) -> (forall ~>. (Cod f) ~ ~> => a ~> (f :% (a, a))) -> ComonoidObject f a
counit :: ComonoidObject f a -> forall ~>. (Cod f) ~ ~> => a ~> Unit f
comultiply :: ComonoidObject f a -> forall ~>. (Cod f) ~ ~> => a ~> (f :% (a, a))
preludeMonoid :: Monoid m => MonoidObject (ProductFunctor (->)) m
data MonoidAsCategory f m a b
MonoidValue :: f -> MonoidObject f m -> Unit f ~> m -> MonoidAsCategory f m m m
type Monad f = MonoidObject (FunctorCompose (Dom f)) f
mkMonad :: (Functor f, (Dom f) ~ ~>, (Cod f) ~ ~>, Category ~>) => f -> (forall a. Obj ~> a -> Component (Id ~>) f a) -> (forall a. Obj ~> a -> Component (f :.: f) f a) -> Monad f
preludeMonad :: (Functor f, Monad f) => Monad (EndoHask f)
monadFunctor :: Monad f -> f
type Comonad f = ComonoidObject (FunctorCompose (Dom f)) f
mkComonad :: (Functor f, (Dom f) ~ ~>, (Cod f) ~ ~>, Category ~>) => f -> (forall a. Obj ~> a -> Component f (Id ~>) a) -> (forall a. Obj ~> a -> Component f (f :.: f) a) -> Comonad f
adjunctionMonad :: Adjunction c d f g -> Monad (g :.: f)
adjunctionComonad :: Adjunction c d f g -> Comonad (f :.: g)
instance Category (MonoidAsCategory f m)
instance Category (~>) => TensorProduct (FunctorCompose (~>))
instance (HasInitialObject (~>), HasBinaryCoproducts (~>)) => TensorProduct (CoproductFunctor (~>))
instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => TensorProduct (ProductFunctor (~>))
instance Category (~>) => HasUnit (FunctorCompose (~>))
instance (HasInitialObject (~>), HasBinaryCoproducts (~>)) => HasUnit (CoproductFunctor (~>))
instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => HasUnit (ProductFunctor (~>))


module Data.Category.CartesianClosed
class (HasTerminalObject ~>, HasBinaryProducts ~>) => CartesianClosed ~>
apply :: CartesianClosed ~> => Obj ~> y -> Obj ~> z -> BinaryProduct ~> (Exponential ~> y z) y ~> z
tuple :: CartesianClosed ~> => Obj ~> y -> Obj ~> z -> z ~> Exponential ~> y (BinaryProduct ~> z y)
(^^^) :: CartesianClosed ~> => (z1 ~> z2) -> (y2 ~> y1) -> (Exponential ~> y1 z1 ~> Exponential ~> y2 z2)
data ExpFunctor ~> :: (* -> * -> *)
ExpFunctor :: ExpFunctor
data CatApply y :: (* -> * -> *) z :: (* -> * -> *)
CatApply :: CatApply
data CatTuple y :: (* -> * -> *) z :: (* -> * -> *)
CatTuple :: CatTuple
type Presheaves ~> = Nat (Op ~>) (->)
data PShExponential ~> :: (* -> * -> *) p q
PShExponential :: PShExponential p q
data ProductWith ~> y
ProductWith :: (Obj ~> y) -> ProductWith ~> y
data ExponentialWith ~> y
ExponentialWith :: (Obj ~> y) -> ExponentialWith ~> y
curryAdj :: CartesianClosed ~> => Obj ~> y -> Adjunction ~> ~> (ProductWith ~> y) (ExponentialWith ~> y)
curry :: CartesianClosed ~> => Obj ~> x -> Obj ~> y -> Obj ~> z -> (ProductWith ~> y :% x) ~> z -> x ~> (ExponentialWith ~> y :% z)
uncurry :: CartesianClosed ~> => Obj ~> x -> Obj ~> y -> Obj ~> z -> x ~> (ExponentialWith ~> y :% z) -> (ProductWith ~> y :% x) ~> z
type State ~> s a = ExponentialWith ~> s :% (ProductWith ~> s :% a)
stateMonadReturn :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> a ~> State ~> s a
stateMonadJoin :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> State ~> s (State ~> s a) ~> State ~> s a
type Context ~> s a = ProductWith ~> s :% (ExponentialWith ~> s :% a)
contextComonadExtract :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> Context ~> s a ~> a
contextComonadDuplicate :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> Context ~> s a ~> Context ~> s (Context ~> s a)
instance CartesianClosed (~>) => Functor (ExponentialWith (~>) y)
instance HasBinaryProducts (~>) => Functor (ProductWith (~>) y)
instance Category (~>) => CartesianClosed (Presheaves (~>))
instance (Dom p ~ Op (~>), Dom q ~ Op (~>), Cod p ~ (->), Cod q ~ (->), Category (~>), Functor p, Functor q) => Functor (PShExponential (~>) p q)
instance CartesianClosed Cat
instance (Category y, Category z) => Functor (CatTuple y z)
instance (Category y, Category z) => Functor (CatApply y z)
instance CartesianClosed (->)
instance CartesianClosed (~>) => Functor (ExpFunctor (~>))


module Data.Category.Yoneda

-- | The Yoneda embedding functor.
yonedaEmbedding :: Category ~> => Postcompose (Hom ~>) ~> :.: CatTuple ~> (Op ~>)
data Yoneda f
Yoneda :: Yoneda f
fromYoneda :: (Functor f, (Cod f) ~ (->)) => f -> Yoneda f :~> f
toYoneda :: (Functor f, (Cod f) ~ (->)) => f -> f :~> Yoneda f
instance Functor f => Functor (Yoneda f)


-- | A monoid as a category with one object.
module Data.Category.Monoid

-- | The arrows are the values of the monoid.
data MonoidA m a b
MonoidA :: m -> MonoidA m m m
data Mon :: * -> * -> *
MonoidMorphism :: (m1 -> m2) -> Mon m1 m2
unMonoidMorphism :: (Monoid m1, Monoid m2) => Mon m1 m2 -> m1 -> m2
data ForgetMonoid
ForgetMonoid :: ForgetMonoid
data FreeMonoid
FreeMonoid :: FreeMonoid
freeMonoidAdj :: Adjunction Mon (->) FreeMonoid ForgetMonoid
foldMap :: Monoid m => (a -> m) -> [a] -> m
listMonadReturn :: a -> [a]
listMonadJoin :: [[a]] -> [a]
listComonadExtract :: Monoid m => [m] -> m
listComonadDuplicate :: Monoid m => [m] -> [[m]]
instance Functor FreeMonoid
instance Functor ForgetMonoid
instance Category Mon
instance Monoid m => Category (MonoidA m)


-- | <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

-- | A natural transformation <tt>Nat c d</tt> is isomorphic to a functor
--   from <tt>c :**: 2</tt> to <tt>d</tt>.
data NatAsFunctor f g
NatAsFunctor :: (Nat (Dom f) (Cod f) f g) -> NatAsFunctor f g
instance (Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d, Functor f, Functor g, Category c, Category d) => Functor (NatAsFunctor f g)
instance CartesianClosed Boolean
instance HasBinaryCoproducts Boolean
instance HasBinaryProducts Boolean
instance HasTerminalObject Boolean
instance HasInitialObject Boolean
instance Category Boolean


-- | Omega, the category 0 -&gt; 1 -&gt; 2 -&gt; 3 -&gt; ... The objects
--   are the natural numbers, and there's an arrow from a to b iff a &lt;=
--   b.
module Data.Category.Omega
data Z
data S n

-- | The arrows of omega, there's an arrow from a to b iff a &lt;= b.
data Omega :: * -> * -> *
Z :: Omega Z Z
Z2S :: Omega Z n -> Omega Z (S n)
S :: Omega a b -> Omega (S a) (S b)
zeroMonoid :: MonoidObject (CoproductFunctor Omega) Z
zeroComonoid :: ComonoidObject (CoproductFunctor Omega) Z
instance HasBinaryCoproducts Omega
instance HasBinaryProducts Omega
instance HasInitialObject Omega
instance Category Omega


-- | 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 ~> b -> a ~> (m :% b) -> Kleisli m a b
kleisliId :: (Functor m, (Dom m) ~ ~>, (Cod m) ~ ~>) => Monad m -> Obj ~> 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) ~ ~>, (Cod m) ~ ~>) => Monad m -> Adjunction (Kleisli m) ~> (KleisliAdjF m) (KleisliAdjG m)
instance (Dom m ~ (~>), Cod m ~ (~>), Functor m) => Functor (KleisliAdjG m)
instance (Dom m ~ (~>), Cod m ~ (~>), Functor m) => 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)

-- | <a>FixF</a> provides the initial F-algebra for endofunctors in Hask.
newtype FixF f
InF :: f :% FixF f -> FixF f
outF :: FixF f -> f :% FixF f

-- | Catamorphisms for endofunctors in Hask.
cataHask :: Functor f => Cata (EndoHask f) a

-- | Anamorphisms for endofunctors in Hask.
anaHask :: Functor f => Ana (EndoHask f) a

-- | The category for defining the natural numbers and primitive recursion
--   can be described as <tt>Dialg(F,G)</tt>, with
--   <tt>F(A)=&lt;1,A&gt;</tt> and <tt>G(A)=&lt;A,A&gt;</tt>.
data NatF ~> :: (* -> * -> *)
NatF :: NatF ~>
data NatNum
Z :: () -> NatNum
S :: NatNum -> NatNum
primRec :: (() -> t) -> (t -> t) -> NatNum -> t
data EMAdjF m
EMAdjF :: (Monad m) -> EMAdjF m
data EMAdjG m
EMAdjG :: EMAdjG m
eilenbergMooreAdj :: (Functor m, (Dom m) ~ ~>, (Cod m) ~ ~>) => Monad m -> Adjunction (Alg m) ~> (EMAdjF m) (EMAdjG m)
instance (Dom m ~ (~>), Cod m ~ (~>), Functor m) => Functor (EMAdjG m)
instance (Dom m ~ (~>), Cod m ~ (~>), Functor m) => Functor (EMAdjF m)
instance HasInitialObject (Dialg (NatF (->)) (DiagProd (->)))
instance HasTerminalObject (~>) => Functor (NatF (~>))
instance Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f))
instance Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->)))
instance Category (Dialg f g)


-- | A Peano category as in <tt>When is one thing equal to some other
--   thing?</tt> Barry Mazur, 2007
module Data.Category.Peano
data PeanoO ~> a
PeanoO :: (TerminalObject ~> ~> x) -> (x ~> x) -> PeanoO ~> x
data Peano :: (* -> * -> *) -> * -> * -> *
PeanoA :: PeanoO ~> a -> PeanoO ~> b -> (a ~> b) -> Peano ~> a b
peanoId :: Category ~> => PeanoO ~> a -> Obj (Peano ~>) a
peanoO :: Category ~> => Obj (Peano ~>) a -> PeanoO ~> a

-- | The natural numbers are the initial object for the <a>Peano</a>
--   category.
data NatNum
Z :: () -> NatNum
S :: NatNum -> NatNum

-- | Primitive recursion is the factorizer from the natural numbers.
primRec :: (() -> t) -> (t -> t) -> NatNum -> t
instance HasInitialObject (Peano (->))
instance HasTerminalObject (~>) => Category (Peano (~>))


-- | Comma categories.
module Data.Category.Comma
data CommaO :: * -> * -> * -> *
CommaO :: Obj (Dom t) a -> ((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')
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
instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s)