-- 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. Therefore the <a>Category</a> class
--   has an associated data type <a>Obj</a>. This which will often also be
--   a GADT.
--   
--   See the <a>Monoid</a>, <a>Boolean</a> and <a>Product</a> categories
--   for some examples.
@package data-category
@version 0.2.0


module Data.Category

-- | An instance of <tt>Category (~&gt;)</tt> declares the arrow
--   <tt>(~&gt;)</tt> as a category.
class Category ~> where { data family Obj ~> :: * -> *; }
src :: (Category ~>) => a ~> b -> Obj ~> a
tgt :: (Category ~>) => a ~> b -> Obj ~> b
id :: (Category ~>) => Obj ~> a -> a ~> a
(.) :: (Category ~>) => b ~> c -> a ~> b -> a ~> c
data Op :: (* -> * -> *) -> * -> * -> *
Op :: (a ~> b) -> Op ~> b a
instance (Category (~>)) => Category (Op (~>))
instance Category (->)


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. As objects are represented at both
--   the type and value level, we need 3 maps in total.
class Functor ftag
(%%) :: (Functor ftag) => ftag -> Obj (Dom ftag) a -> Obj (Cod ftag) (ftag :% a)
(%) :: (Functor ftag) => ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)

-- | <tt>:%</tt> maps objects at the type level.

-- | 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 covariant functor Hom(X,--)
data (:*-:) :: * -> (* -> * -> *) -> *
HomX_ :: Obj ~> x -> x :*-: ~>

-- | The contravariant functor Hom(--,X)
data (:-*:) :: (* -> * -> *) -> * -> *
Hom_X :: Obj ~> x -> ~> :-*: x

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

-- | An initial universal property, a universal morphism from x to u.
data InitialUniversal x u a
InitialUniversal :: 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
iuObject :: InitialUniversal x u a -> Obj (Dom u) a
initialMorphism :: InitialUniversal x u a -> Cod u x (u :% a)
initialFactorizer :: InitialUniversal x u a -> forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y

-- | A terminal universal property, a universal morphism from u to x.
data TerminalUniversal x u a
TerminalUniversal :: 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
tuObject :: TerminalUniversal x u a -> Obj (Dom u) a
terminalMorphism :: TerminalUniversal x u a -> Cod u (u :% a) x
terminalFactorizer :: TerminalUniversal x u a -> forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a
instance Functor (EndoHask f)
instance Functor (Opposite f)
instance Functor ((~>) :-*: x)
instance Functor (x :*-: (~>))
instance Functor (Const c1 c2 x)
instance Functor (g :.: h)
instance 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

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

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

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

-- | 'n ! a' returns the component for the object <tt>a</tt> of a natural
--   transformation <tt>n</tt>.
(!) :: ((Cod f) ~ d, (Cod g) ~ d) => Nat ~> d f g -> Obj ~> a -> d (f :% a) (g :% a)

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

-- | The Yoneda embedding functor.
data YonedaEmbedding :: (* -> * -> *) -> *
YonedaEmbedding :: YonedaEmbedding ~>
instance Functor (YonedaEmbedding (~>))
instance (Category (~>)) => Representable ((~>) :-*: x)
instance Functor (Postcompose f c)
instance Functor (Precompose f d)
instance (Category c, Category d) => Category (Nat c d)


-- | <i>0</i>, the empty category. The limit and colimit of the functor
--   from <i>0</i> to some category provide terminal and initial objects in
--   that category.
module Data.Category.Void

-- | The (empty) data type of the arrows in <i>0</i>.
data Void a b
magicVoid :: Void a b -> x
magicVoidO :: Obj Void a -> x

-- | The functor from <i>0</i> to (~&gt;), the empty diagram in (~&gt;).
data VoidDiagram ~> :: (* -> * -> *)
VoidDiagram :: VoidDiagram
voidNat :: (Functor f, Functor g, (Dom f) ~ Void, (Dom g) ~ Void, (Cod f) ~ d, (Cod g) ~ d) => f -> g -> Nat Void d f g
instance Functor (VoidDiagram (~>))
instance Category Void


-- | Pair, the category with just 2 objects and their identity arrows. The
--   limit and colimit of the functor from Pair to some category provide
--   products and coproducts in that category.
module Data.Category.Pair
data P1
data P2

-- | The arrows of Pair.
data Pair :: * -> * -> *
IdFst :: Pair P1 P1
IdSnd :: Pair P2 P2

-- | The functor from Pair to (~&gt;), a diagram of 2 objects in (~&gt;).
data PairDiagram :: (* -> * -> *) -> * -> * -> *
PairDiagram :: Obj ~> x -> Obj ~> y -> PairDiagram ~> x y
pairNat :: (Functor f, Functor g, (Dom f) ~ Pair, (Cod f) ~ d, (Dom g) ~ Pair, (Cod g) ~ d) => f -> g -> Com f g P1 -> Com f g P2 -> Nat Pair d f g
arrowPair :: (Category ~>) => (x1 ~> x2) -> (y1 ~> y2) -> Nat Pair ~> (PairDiagram ~> x1 y1) (PairDiagram ~> x2 y2)
instance Functor (PairDiagram (~>) x y)
instance Category Pair


-- | <i>1</i>, The singleton category with just one object with only its
--   identity arrow.
module Data.Category.Unit
data UnitO

-- | The arrows of Unit.
data Unit a b
UnitId :: Unit UnitO UnitO
instance Category Unit


module Data.Category.Product
data (:*:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> *
(:**:) :: c1 a1 b1 -> c2 a2 b2 -> :*: c1 c2 (a1, a2) (b1, b2)
data Proj1 c1 :: (* -> * -> *) c2 :: (* -> * -> *)
Proj1 :: Proj1
data Proj2 c1 :: (* -> * -> *) c2 :: (* -> * -> *)
Proj2 :: Proj2
data (:***:) f1 f2
(:***:) :: f1 -> f2 -> f1 :***: f2
data Hom ~>
Hom :: Hom ~>
data DiagProd :: (* -> * -> *) -> *
DiagProd :: DiagProd ~>
instance Functor (DiagProd (~>))
instance Functor (Hom (~>))
instance Functor (f1 :***: f2)
instance Functor (Proj2 c1 c2)
instance Functor (Proj1 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
data Z
data S n
S :: n -> S n

-- | The arrows in Discrete n, a finite set of identity arrows.
data Discrete :: * -> * -> * -> *
IdZ :: Discrete (S n) Z Z
StepS :: Discrete n a a -> Discrete (S n) (S a) (S a)
magicZ :: Discrete Z a b -> x
magicZO :: Obj (Discrete Z) a -> x
data Next :: * -> * -> *
Next :: f -> Next n f
data DiscreteDiagram :: (* -> * -> *) -> * -> * -> *
Nil :: DiscreteDiagram ~> Z ()
(:::) :: Obj ~> x -> DiscreteDiagram ~> n xs -> DiscreteDiagram ~> (S n) (x, xs)
instance Functor (DiscreteDiagram (~>) n xs)
instance Functor (Next n f)
instance Category (Discrete Z)
instance (Category (Discrete n)) => Category (Discrete (S n))


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

-- | A limit of <tt>f</tt> is a universal morphism from the diagonal
--   functor to <tt>f</tt>.
type LimitUniversal f = TerminalUniversal f (DiagF f) (Limit f)

-- | <tt>limitUniversal</tt> is a helper function to create the universal
--   property from the limit and the limit factorizer.
limitUniversal :: ((Cod f) ~ ~>) => Cone f (Limit f) -> (forall n. Cone f n -> n ~> Limit f) -> LimitUniversal f

-- | A limit of the diagram <tt>f</tt> is a cone of <tt>f</tt>.
limit :: LimitUniversal f -> Cone f (Limit f)

-- | For any other cone of <tt>f</tt> with vertex <tt>n</tt> there exists a
--   unique morphism from <tt>n</tt> to the limit of <tt>f</tt>.
limitFactorizer :: ((Cod f) ~ ~>) => LimitUniversal f -> (forall n. Cone f n -> n ~> Limit f)

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

-- | A colimit of <tt>f</tt> is a universal morphism from <tt>f</tt> to the
--   diagonal functor.
type ColimitUniversal f = InitialUniversal f (DiagF f) (Colimit f)

-- | <tt>colimitUniversal</tt> is a helper function to create the universal
--   property from the colimit and the colimit factorizer.
colimitUniversal :: ((Cod f) ~ ~>) => Cocone f (Colimit f) -> (forall n. Cocone f n -> Colimit f ~> n) -> ColimitUniversal f

-- | A colimit of the diagram <tt>f</tt> is a co-cone of <tt>f</tt>.
colimit :: ColimitUniversal f -> Cocone f (Colimit f)

-- | For any other co-cone of <tt>f</tt> with vertex <tt>n</tt> there
--   exists a unique morphism from the colimit of <tt>f</tt> to <tt>n</tt>.
colimitFactorizer :: ((Cod f) ~ ~>) => ColimitUniversal f -> (forall n. Cocone f n -> Colimit f ~> n)

-- | 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 ~>
limitUniv :: (HasLimits j ~>) => Obj (Nat j ~>) f -> LimitUniversal 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 ~>
colimitUniv :: (HasColimits j ~>) => Obj (Nat j ~>) f -> ColimitUniversal 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>
--   <a>arrowPair</a> <tt>l r</tt>
data LimitFunctor :: (* -> * -> *) -> (* -> * -> *) -> *
LimitFunctor :: LimitFunctor j ~>

-- | 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>
--   <a>arrowPair</a> <tt>l r</tt>
data ColimitFunctor :: (* -> * -> *) -> (* -> * -> *) -> *
ColimitFunctor :: ColimitFunctor 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

-- | Any empty data type is an initial object in Hask.
data Zero

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

-- | The coproduct of 2 objects is the colimit of the functor from Pair to
--   (~&gt;).
class (Category ~>) => HasBinaryCoproducts ~>
coproduct :: (HasBinaryCoproducts ~>) => Obj ~> x -> Obj ~> y -> Obj ~> (BinaryCoproduct ~> x y)
inj :: (HasBinaryCoproducts ~>) => Obj ~> x -> Obj ~> y -> (x ~> BinaryCoproduct ~> x 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)
newtype ForAll f
ForAll :: (forall a. f a) -> ForAll f
unForAll :: ForAll f -> forall a. f a
endoHaskLimit :: (Functor f) => LimitUniversal (EndoHask f)
data Exists f
Exists :: (f a) -> Exists f
endoHaskColimit :: (Functor f) => ColimitUniversal (EndoHask f)
instance HasBinaryCoproducts (->)
instance (HasBinaryCoproducts (~>)) => HasColimits Pair (~>)
instance HasBinaryProducts Cat
instance HasBinaryProducts (->)
instance (HasBinaryProducts (~>)) => HasLimits Pair (~>)
instance HasInitialObject Cat
instance HasInitialObject (->)
instance (HasInitialObject (~>)) => HasColimits Void (~>)
instance HasTerminalObject Cat
instance HasTerminalObject (->)
instance (HasTerminalObject (~>)) => HasLimits Void (~>)
instance Functor (ColimitFunctor j (~>))
instance Functor (LimitFunctor j (~>))
instance Functor (Diag j (~>))


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
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
unit :: Adjunction c d f g -> Id d :~> (g :.: f)
counit :: Adjunction c d f g -> (f :.: g) :~> Id c
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
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)
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
data AdjArrow c d
AdjArrow :: Adjunction c d f g -> AdjArrow (CatW c) (CatW d)
wrap :: (Functor g, Functor f, (Dom g) ~ (Dom f'), (Dom g) ~ (Cod f)) => g -> f -> Nat (Dom f') (Dom f') (Id (Dom f')) (g' :.: f') -> (g :.: f) :~> ((g :.: g') :.: (f' :.: f))
cowrap :: (Functor f', Functor g', (Dom f') ~ (Dom g), (Dom f') ~ (Cod g')) => f' -> g' -> Nat (Dom g) (Dom g) (f :.: g) (Id (Dom g)) -> ((f' :.: f) :.: (g :.: g')) :~> (f' :.: g')
curryAdj :: Adjunction (->) (->) (EndoHask ((,) e)) (EndoHask ((->) e))

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

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


-- | 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
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 BF
data BT
data Boolean a b
IdFls :: Boolean BF BF
FlsTru :: Boolean BF BT
IdTru :: Boolean BT BT
instance Show (Obj Boolean a)
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 :: * -> * -> *
IdZ :: Omega Z Z
GTZ :: Omega Z n -> Omega Z (S n)
StS :: Omega a b -> Omega (S a) (S b)
instance Show (Obj Omega a)
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
class (Functor m) => Pointed m
point :: (Pointed m) => m -> Id (Dom m) :~> m
class (Pointed m) => Monad m
join :: (Monad m) => m -> (m :.: m) :~> m
data Kleisli ~> :: (* -> * -> *) m a b
Kleisli :: m -> Obj ~> b -> a ~> (m :% b) -> Kleisli ~> m a b
data KleisliAdjF ~> :: (* -> * -> *) m
KleisliAdjF :: m -> KleisliAdjF ~> m
data KleisliAdjG ~> :: (* -> * -> *) m
KleisliAdjG :: m -> KleisliAdjG ~> m
kleisliAdj :: (Monad m, (Dom m) ~ ~>, (Cod m) ~ ~>, Category ~>) => m -> Adjunction (Kleisli ~> m) ~> (KleisliAdjF ~> m) (KleisliAdjG ~> m)
instance Functor (KleisliAdjG (~>) m)
instance Functor (KleisliAdjF (~>) m)
instance (Dom m ~ (~>), Cod m ~ (~>), Category (~>), Monad m) => 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.
type Dialgebra f g a = Obj (Dialg 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
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
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
instance HasInitialObject (Dialg (NatF (->)) (DiagProd (->)))
instance 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 Peano :: (* -> * -> *) -> * -> * -> *
PeanoA :: Obj (Peano ~>) a -> Obj (Peano ~>) b -> (a ~> b) -> Peano ~> a b

-- | 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 (Category (~>)) => Category (Peano (~>))


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