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


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
infixr 8 .

-- | Whenever objects are required at value level, they are represented by
--   their identity arrows.
type Obj k a = k a a

-- | <tt>Kind k</tt> is the kind of the objects of the category <tt>k</tt>.
type family Kind (k :: o -> o -> Type) :: Type
newtype Op k a b
Op :: k b a -> Op k a b
[unOp] :: Op k a b -> k b a
obj :: Obj (FUN m) a
instance forall k1 (k2 :: k1 -> k1 -> *). Data.Category.Category k2 => Data.Category.Category (Data.Category.Op k2)
instance Data.Category.Category (->)


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


module Data.Category.Functor

-- | Functors are arrows in the category Cat.
data Cat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type
[CatA] :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (Dom ftag) (Cod ftag)

-- | Functors map objects and arrows.
class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where {
    
    -- | The domain, or source category, of the functor.
    type Dom ftag :: Type -> Type -> Type;
    
    -- | The codomain, or target category, of the functor.
    type Cod ftag :: Type -> Type -> Type;
    
    -- | <tt>:%</tt> maps objects.
    type ftag :% a :: Type;
}

-- | <tt>%</tt> maps arrows.
(%) :: Functor ftag => ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
infixr 9 :%
infixr 9 %
type FunctorOf a b t = (Functor t, Dom t ~ a, Cod t ~ b)
data Id (k :: Type -> Type -> Type)
Id :: Id (k :: Type -> Type -> Type)
data g :.: h
[:.:] :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h
data Const (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) 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 OpOp (k :: Type -> Type -> Type)
OpOp :: OpOp (k :: Type -> Type -> Type)
data OpOpInv (k :: Type -> Type -> Type)
OpOpInv :: OpOpInv (k :: Type -> Type -> Type)

-- | A functor wrapper in case of conflicting family instance declarations
newtype Any f
Any :: f -> Any f
data Proj1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type)
Proj1 :: Proj1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type)
data Proj2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type)
Proj2 :: Proj2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type)
data f1 :***: f2
[:***:] :: (Functor f1, Functor f2) => f1 -> f2 -> f1 :***: f2
data DiagProd (k :: Type -> Type -> Type)
DiagProd :: DiagProd (k :: Type -> Type -> Type)
type Tuple1 c1 c2 a = (Const c2 c1 a :***: Id c2) :.: DiagProd c2

-- | <a>Tuple1</a> tuples with a fixed object on the left.
pattern Tuple1 :: (Category c1, Category c2) => Obj c1 a -> Tuple1 c1 c2 a
type Tuple2 c1 c2 a = Swap c2 c1 :.: Tuple1 c2 c1 a

-- | <a>Tuple2</a> tuples with a fixed object on the right.
pattern Tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a
type Swap (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2)

-- | <tt>swap</tt> swaps the 2 categories of the product of categories.
pattern Swap :: (Category c1, Category c2) => Swap c1 c2
data Hom (k :: Type -> Type -> Type)
Hom :: Hom (k :: Type -> Type -> Type)
type x :*-: k = Hom k :.: Tuple1 (Op k) k x

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

-- | The contravariant functor Hom(--,X)
pattern Hom_X :: Category k => Obj k x -> k :-*: x
type ProfunctorOf c d t = (FunctorOf (Op c :**: d) (->) t, Category c, Category d)
instance Data.Category.Functor.Functor f => Data.Category.Functor.Functor (Data.Category.Functor.Any f)
instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Functor.Hom k)
instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Functor.DiagProd k)
instance (Data.Category.Functor.Functor f1, Data.Category.Functor.Functor f2) => Data.Category.Functor.Functor (f1 Data.Category.Functor.:***: f2)
instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Functor.Proj2 c1 c2)
instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Functor.Proj1 c1 c2)
instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Functor.OpOpInv k)
instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Functor.OpOp k)
instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Functor.Const c1 c2 x)
instance Data.Category.Category Data.Category.Functor.Cat
instance (Data.Category.Category (Data.Category.Functor.Cod g), Data.Category.Category (Data.Category.Functor.Dom h)) => Data.Category.Functor.Functor (g Data.Category.Functor.:.: h)
instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Functor.Id k)


module Data.Category.NaturalTransformation

-- | <tt>f :~&gt; g</tt> is a natural transformation from functor f to
--   functor g.
type f :~> g = forall c d. (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)

-- | '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)
infixl 9 !

-- | 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
pattern NatId :: () => (Functor f, c ~ Dom f, d ~ Cod f) => f -> Nat c d 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 :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type
[Nat] :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => 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
type Presheaves k = Nat (Op k) (->)
type Profunctors c d = Nat (Op d :**: c) (->)
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)
constPrecompIn :: Nat j d (f :.: Const j c x) g -> Nat j d (Const j d (f :% x)) g
constPrecompOut :: Nat j d f (g :.: Const j c x) -> Nat j d f (Const j d (g :% x))
constPostcompIn :: Nat j d (Const k d x :.: f) g -> Nat j d (Const j d x) g
constPostcompOut :: Nat j d f (Const k d x :.: g) -> Nat j d f (Const j d x)
data FunctorCompose (c :: Type -> Type -> Type) (d :: Type -> Type -> Type) (e :: Type -> Type -> Type)
FunctorCompose :: FunctorCompose (c :: Type -> Type -> Type) (d :: Type -> Type -> Type) (e :: Type -> Type -> Type)

-- | Composition of endofunctors is a functor.
type EndoFunctorCompose k = FunctorCompose k k k

-- | <tt>Precompose f e</tt> is the functor such that <tt>Precompose f e :%
--   g = g :.: f</tt>, for functors <tt>g</tt> that compose with <tt>f</tt>
--   and with codomain <tt>e</tt>.
type Precompose f e = FunctorCompose (Dom f) (Cod f) e :.: Tuple2 (Nat (Cod f) e) (Nat (Dom f) (Cod f)) f
pattern Precompose :: (Category e, Functor f) => f -> Precompose f e

-- | <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>.
type Postcompose f c = FunctorCompose c (Dom f) (Cod f) :.: Tuple1 (Nat (Dom f) (Cod f)) (Nat c (Dom f)) f
pattern Postcompose :: (Category c, Functor f) => f -> Postcompose f c
type Curry1 c1 c2 f = Postcompose f c2 :.: Tuple c1 c2

-- | Curry on the first "argument" of a functor from a product category.
pattern Curry1 :: (Functor f, Dom f ~ (c1 :**: c2), Category c1, Category c2) => f -> Curry1 c1 c2 f
type Curry2 c1 c2 f = Postcompose f c1 :.: Curry1 c2 c1 (Swap c2 c1)

-- | Curry on the second "argument" of a functor from a product category.
pattern Curry2 :: (Functor f, Dom f ~ (c1 :**: c2), Category c1, Category c2) => f -> Curry2 c1 c2 f
data Wrap f h
Wrap :: f -> h -> Wrap f h
data Apply (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type)
Apply :: Apply (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type)
data Tuple (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type)
Tuple :: Tuple (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type)
data Opp (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type)
Opp :: Opp (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type)
type Opposite f = Opp (Dom f) (Cod f) :.: Tuple1 (Op (Nat (Dom f) (Cod f))) (Op (Dom f)) f

-- | The dual of a functor
pattern Opposite :: Functor f => f -> Opposite f
type HomF f g = Hom (Cod f) :.: (Opposite f :***: g)
pattern HomF :: (Functor f, Functor g, Cod f ~ Cod g) => f -> g -> HomF f g
type Star f = HomF (Id (Cod f)) f
pattern Star :: Functor f => f -> Star f
type Costar f = HomF f (Id (Cod f))
pattern Costar :: Functor f => f -> Costar f
type x :*%: f = (x :*-: Cod f) :.: f

-- | The covariant functor Hom(X,F-)
pattern HomXF :: Functor f => Obj (Cod f) x -> f -> x :*%: f
type f :%*: x = (Cod f :-*: x) :.: Opposite f

-- | The contravariant functor Hom(F-,X)
pattern HomFX :: Functor f => f -> Obj (Cod f) x -> f :%*: x
instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.NaturalTransformation.Opp c1 c2)
instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.NaturalTransformation.Tuple c1 c2)
instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.NaturalTransformation.Apply c1 c2)
instance (Data.Category.Functor.Functor f, Data.Category.Functor.Functor h) => Data.Category.Functor.Functor (Data.Category.NaturalTransformation.Wrap f h)
instance (Data.Category.Category c, Data.Category.Category d, Data.Category.Category e) => Data.Category.Functor.Functor (Data.Category.NaturalTransformation.FunctorCompose c d e)
instance Data.Category.Category d => Data.Category.Category (Data.Category.NaturalTransformation.Nat c d)


module Data.Category.Adjunction
data Adjunction c d f g
Adjunction :: f -> g -> Profunctors c d (Costar f) (Star g) -> Profunctors c d (Star g) (Costar f) -> Adjunction c d f g
[leftAdjoint] :: Adjunction c d f g -> f
[rightAdjoint] :: Adjunction c d f g -> g
[leftAdjunctN] :: Adjunction c d f g -> Profunctors c d (Costar f) (Star g)
[rightAdjunctN] :: Adjunction c d f g -> Profunctors c d (Star g) (Costar f)

-- | Make an adjunction from the hom-set isomorphism.
mkAdjunction :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b)) -> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b) -> Adjunction c d f g

-- | Make an adjunction from the unit and counit.
mkAdjunctionUnits :: (Functor f, Functor g, 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

-- | Make an adjunction from an initial universal property.
mkAdjunctionInit :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall a. Obj d a -> d a (g :% (f :% a))) -> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b) -> Adjunction c d f g

-- | Make an adjunction from a terminal universal property.
mkAdjunctionTerm :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b)) -> (forall b. Obj c b -> c (f :% (g :% b)) b) -> 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
adjunctionUnit :: Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionCounit :: Adjunction c d f g -> Nat c c (f :.: g) (Id c)
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] :: (Category c, Category d) => Adjunction c d f g -> AdjArrow c d
precomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat c e) (Nat d e) (Precompose g e) (Precompose f e)
postcomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat e c) (Nat e d) (Postcompose f e) (Postcompose g e)
contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r)
instance Data.Category.Category Data.Category.Adjunction.AdjArrow


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 :*%: 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 (u :%*: x) 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

-- | For an adjunction F -| G, each pair (FY, unit_Y) is an initial
--   morphism from Y to G.
adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)

-- | For an adjunction F -| G, each pair (GX, counit_X) is a terminal
--   morphism from F to X.
adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)
initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall y. InitialUniversal y g (f :% y)) -> Adjunction c d f g
terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall x. TerminalUniversal x f (g :% x)) -> Adjunction c d f g


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


module Data.Category.Coproduct
data I1 a
data I2 a
data (:++:) :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type
[I1] :: c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
[I2] :: c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)
data Inj1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type)
Inj1 :: Inj1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type)
data Inj2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type)
Inj2 :: Inj2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type)
data f1 :+++: f2
(:+++:) :: f1 -> f2 -> (:+++:) f1 f2
data CodiagCoprod (k :: Type -> Type -> Type)
CodiagCoprod :: CodiagCoprod (k :: Type -> Type -> Type)
newtype Cotuple1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) a
Cotuple1 :: Obj c1 a -> Cotuple1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) a
newtype Cotuple2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) a
Cotuple2 :: Obj c2 a -> Cotuple2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) a
data Cograph c d f :: Type -> Type -> Type
[I1A] :: c a1 b1 -> Cograph c d f (I1 a1) (I1 b1)
[I2A] :: d a2 b2 -> Cograph c d f (I2 a2) (I2 b2)
[I12] :: Obj c a -> Obj d b -> f -> (f :% (a, b)) -> Cograph c d f (I1 a) (I2 b)

-- | The directed coproduct category of categories <tt>c1</tt> and
--   <tt>c2</tt>.
newtype ( c1 :>>: c2 ) a b
DC :: Cograph c1 c2 (Const (Op c1 :**: c2) (->) ()) a b -> (:>>:) c1 c2 a b
newtype NatAsFunctor f g
NatAsFunctor :: Nat (Dom f) (Cod f) f g -> NatAsFunctor f g
instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Category (c1 Data.Category.Coproduct.:>>: c2)
instance (Data.Category.Functor.Functor f, Data.Category.Functor.Functor g, Data.Category.Functor.Dom f GHC.Types.~ Data.Category.Functor.Dom g, Data.Category.Functor.Cod f GHC.Types.~ Data.Category.Functor.Cod g) => Data.Category.Functor.Functor (Data.Category.Coproduct.NatAsFunctor f g)
instance Data.Category.Functor.ProfunctorOf c d f => Data.Category.Category (Data.Category.Coproduct.Cograph c d f)
instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Coproduct.Cotuple2 c1 c2 a2)
instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Coproduct.Cotuple1 c1 c2 a1)
instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Coproduct.CodiagCoprod k)
instance (Data.Category.Functor.Functor f1, Data.Category.Functor.Functor f2) => Data.Category.Functor.Functor (f1 Data.Category.Coproduct.:+++: f2)
instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Coproduct.Inj2 c1 c2)
instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Coproduct.Inj1 c1 c2)
instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Category (c1 Data.Category.Coproduct.:++: c2)


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


module Data.Category.Limit
data Diag :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type
[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 j k f n = Nat j k (Const j k n) f

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

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

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

-- | 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 where {
    
    -- | 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 LimitFam (j :: Type -> Type -> Type) (k :: Type -> Type -> Type) (f :: Type) :: Type;
}

-- | <a>limit</a> returns the limiting cone for a functor <tt>f</tt>.
limit :: HasLimits j k => Obj (Nat j k) f -> Cone j k f (LimitFam j k f)

-- | <a>limitFactorizer</a> shows that the limiting cone is universal –
--   i.e. any other cone of <tt>f</tt> factors through it by returning the
--   morphism between the vertices of the cones.
limitFactorizer :: HasLimits j k => Cone j k f n -> k n (LimitFam j k f)
type Limit f = LimitFam (Dom f) (Cod f) f
data LimitFunctor (j :: Type -> Type -> Type) (k :: Type -> Type -> Type)
LimitFunctor :: LimitFunctor (j :: Type -> Type -> Type) (k :: Type -> Type -> Type)

-- | The limit functor is right adjoint to the diagonal functor.
limitAdj :: forall j k. HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
adjLimit :: Category k => Adjunction (Nat j k) k (Diag j k) r -> Obj (Nat j k) f -> Cone j k f (r :% f)
adjLimitFactorizer :: Category k => Adjunction (Nat j k) k (Diag j k) r -> Cone j k f n -> k n (r :% f)
rightAdjointPreservesLimits :: (HasLimits j c, HasLimits j d) => Adjunction c d f g -> Obj (Nat j c) t -> d (Limit (g :.: t)) (g :% Limit t)
rightAdjointPreservesLimitsInv :: (HasLimits j c, HasLimits j d) => Obj (Nat c d) g -> Obj (Nat j c) t -> d (g :% LimitFam j c t) (LimitFam j d (g :.: t))

-- | 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 where {
    
    -- | 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 ColimitFam (j :: Type -> Type -> Type) (k :: Type -> Type -> Type) (f :: Type) :: Type;
}

-- | <a>colimit</a> returns the limiting co-cone for a functor <tt>f</tt>.
colimit :: HasColimits j k => Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)

-- | <a>colimitFactorizer</a> shows that the limiting co-cone is universal
--   – i.e. any other co-cone of <tt>f</tt> factors through it by returning
--   the morphism between the vertices of the cones.
colimitFactorizer :: HasColimits j k => Cocone j k f n -> k (ColimitFam j k f) n
type Colimit f = ColimitFam (Dom f) (Cod f) f
data ColimitFunctor (j :: Type -> Type -> Type) (k :: Type -> Type -> Type)
ColimitFunctor :: ColimitFunctor (j :: Type -> Type -> Type) (k :: Type -> Type -> Type)

-- | The colimit functor is left adjoint to the diagonal functor.
colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
adjColimit :: Category k => Adjunction k (Nat j k) l (Diag j k) -> Obj (Nat j k) f -> Cocone j k f (l :% f)
adjColimitFactorizer :: Category k => Adjunction k (Nat j k) l (Diag j k) -> Cocone j k f n -> k (l :% f) n
leftAdjointPreservesColimits :: (HasColimits j c, HasColimits j d) => Adjunction c d f g -> Obj (Nat j d) t -> c (f :% Colimit t) (Colimit (f :.: t))
leftAdjointPreservesColimitsInv :: (HasColimits j c, HasColimits j d) => Obj (Nat d c) f -> Obj (Nat j d) t -> c (ColimitFam j c (f :.: t)) (f :% ColimitFam j d t)
class Category k => HasTerminalObject k where {
    type TerminalObject k :: Kind 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 InitialObject k :: Kind 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 {
    type BinaryProduct k (x :: Kind k) (y :: Kind k) :: Kind k;
}
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)
infixl 3 ***
infixl 3 &&&
data ProductFunctor (k :: Type -> Type -> Type)
ProductFunctor :: ProductFunctor (k :: Type -> Type -> Type)
data p :*: q
[:*:] :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q

-- | A specialisation of the limit adjunction to products.
prodAdj :: HasBinaryProducts k => Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)
newtype x & y
AddConj :: (forall r. Either (x %1 -> r) (y %1 -> r) %1 -> r) -> (&) x y
class Category k => HasBinaryCoproducts k where {
    type BinaryCoproduct k (x :: Kind k) (y :: Kind k) :: Kind k;
}
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)
infixl 2 |||
infixl 2 +++
data CoproductFunctor (k :: Type -> Type -> Type)
CoproductFunctor :: CoproductFunctor (k :: Type -> Type -> Type)
data p :+: q
[:+:] :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q

-- | A specialisation of the colimit adjunction to coproducts.
coprodAdj :: HasBinaryCoproducts k => Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)

-- | The <a>Either</a> type represents values with two possibilities: a
--   value of type <tt><a>Either</a> a b</tt> is either <tt><a>Left</a>
--   a</tt> or <tt><a>Right</a> b</tt>.
--   
--   The <a>Either</a> type is sometimes used to represent a value which is
--   either correct or an error; by convention, the <a>Left</a> constructor
--   is used to hold an error value and the <a>Right</a> constructor is
--   used to hold a correct value (mnemonic: "right" also means "correct").
--   
--   <h4><b>Examples</b></h4>
--   
--   The type <tt><a>Either</a> <a>String</a> <a>Int</a></tt> is the type
--   of values which can be either a <a>String</a> or an <a>Int</a>. The
--   <a>Left</a> constructor can be used only on <a>String</a>s, and the
--   <a>Right</a> constructor can be used only on <a>Int</a>s:
--   
--   <pre>
--   &gt;&gt;&gt; let s = Left "foo" :: Either String Int
--   
--   &gt;&gt;&gt; s
--   Left "foo"
--   
--   &gt;&gt;&gt; let n = Right 3 :: Either String Int
--   
--   &gt;&gt;&gt; n
--   Right 3
--   
--   &gt;&gt;&gt; :type s
--   s :: Either String Int
--   
--   &gt;&gt;&gt; :type n
--   n :: Either String Int
--   </pre>
--   
--   The <a>fmap</a> from our <a>Functor</a> instance will ignore
--   <a>Left</a> values, but will apply the supplied function to values
--   contained in a <a>Right</a>:
--   
--   <pre>
--   &gt;&gt;&gt; let s = Left "foo" :: Either String Int
--   
--   &gt;&gt;&gt; let n = Right 3 :: Either String Int
--   
--   &gt;&gt;&gt; fmap (*2) s
--   Left "foo"
--   
--   &gt;&gt;&gt; fmap (*2) n
--   Right 6
--   </pre>
--   
--   The <a>Monad</a> instance for <a>Either</a> allows us to chain
--   together multiple actions which may fail, and fail overall if any of
--   the individual steps failed. First we'll write a function that can
--   either parse an <a>Int</a> from a <a>Char</a>, or fail.
--   
--   <pre>
--   &gt;&gt;&gt; import Data.Char ( digitToInt, isDigit )
--   
--   &gt;&gt;&gt; :{
--       let parseEither :: Char -&gt; Either String Int
--           parseEither c
--             | isDigit c = Right (digitToInt c)
--             | otherwise = Left "parse error"
--   
--   &gt;&gt;&gt; :}
--   </pre>
--   
--   The following should work, since both <tt>'1'</tt> and <tt>'2'</tt>
--   can be parsed as <a>Int</a>s.
--   
--   <pre>
--   &gt;&gt;&gt; :{
--       let parseMultiple :: Either String Int
--           parseMultiple = do
--             x &lt;- parseEither '1'
--             y &lt;- parseEither '2'
--             return (x + y)
--   
--   &gt;&gt;&gt; :}
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; parseMultiple
--   Right 3
--   </pre>
--   
--   But the following should fail overall, since the first operation where
--   we attempt to parse <tt>'m'</tt> as an <a>Int</a> will fail:
--   
--   <pre>
--   &gt;&gt;&gt; :{
--       let parseMultiple :: Either String Int
--           parseMultiple = do
--             x &lt;- parseEither 'm'
--             y &lt;- parseEither '2'
--             return (x + y)
--   
--   &gt;&gt;&gt; :}
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; parseMultiple
--   Left "parse error"
--   </pre>
data Either a b
Left :: a -> Either a b
Right :: b -> Either a b
instance Data.Category.Limit.HasColimits (->) (->)
instance Data.Category.Limit.HasLimits (->) (->)
instance (Data.Category.Category (Data.Category.Functor.Dom p), Data.Category.Category (Data.Category.Functor.Cod p)) => Data.Category.Functor.Functor (p Data.Category.Limit.:+: q)
instance (Data.Category.Category c, Data.Category.Limit.HasBinaryCoproducts d) => Data.Category.Limit.HasBinaryCoproducts (Data.Category.NaturalTransformation.Nat c d)
instance Data.Category.Limit.HasBinaryCoproducts k => Data.Category.Functor.Functor (Data.Category.Limit.CoproductFunctor k)
instance (Data.Category.Limit.HasColimits i k, Data.Category.Limit.HasColimits j k, Data.Category.Limit.HasBinaryCoproducts k) => Data.Category.Limit.HasColimits (i Data.Category.Coproduct.:++: j) k
instance Data.Category.Limit.HasBinaryCoproducts (->)
instance Data.Category.Limit.HasBinaryCoproducts Data.Category.Functor.Cat
instance Data.Category.Limit.HasBinaryCoproducts Data.Category.Unit.Unit
instance (Data.Category.Limit.HasBinaryCoproducts c1, Data.Category.Limit.HasBinaryCoproducts c2) => Data.Category.Limit.HasBinaryCoproducts (c1 Data.Category.Product.:**: c2)
instance (Data.Category.Limit.HasBinaryCoproducts c1, Data.Category.Limit.HasBinaryCoproducts c2) => Data.Category.Limit.HasBinaryCoproducts (c1 Data.Category.Coproduct.:>>: c2)
instance forall k1 (k2 :: k1 -> k1 -> *). Data.Category.Limit.HasBinaryCoproducts k2 => Data.Category.Limit.HasBinaryProducts (Data.Category.Op k2)
instance forall k1 (k2 :: k1 -> k1 -> *). Data.Category.Limit.HasBinaryProducts k2 => Data.Category.Limit.HasBinaryCoproducts (Data.Category.Op k2)
instance (Data.Category.Category (Data.Category.Functor.Dom p), Data.Category.Category (Data.Category.Functor.Cod p)) => Data.Category.Functor.Functor (p Data.Category.Limit.:*: q)
instance (Data.Category.Category c, Data.Category.Limit.HasBinaryProducts d) => Data.Category.Limit.HasBinaryProducts (Data.Category.NaturalTransformation.Nat c d)
instance Data.Category.Limit.HasBinaryProducts k => Data.Category.Functor.Functor (Data.Category.Limit.ProductFunctor k)
instance Data.Category.Limit.HasBinaryProducts (FUN 'One)
instance (Data.Category.Limit.HasLimits i k, Data.Category.Limit.HasLimits j k, Data.Category.Limit.HasBinaryProducts k) => Data.Category.Limit.HasLimits (i Data.Category.Coproduct.:++: j) k
instance Data.Category.Limit.HasBinaryProducts (->)
instance Data.Category.Limit.HasBinaryProducts Data.Category.Functor.Cat
instance Data.Category.Limit.HasBinaryProducts Data.Category.Unit.Unit
instance (Data.Category.Limit.HasBinaryProducts c1, Data.Category.Limit.HasBinaryProducts c2) => Data.Category.Limit.HasBinaryProducts (c1 Data.Category.Product.:**: c2)
instance (Data.Category.Limit.HasBinaryProducts c1, Data.Category.Limit.HasBinaryProducts c2) => Data.Category.Limit.HasBinaryProducts (c1 Data.Category.Coproduct.:>>: c2)
instance Data.Category.Limit.HasInitialObject (->)
instance (Data.Category.Category k, Data.Category.Limit.HasInitialObject k) => Data.Category.Limit.HasColimits Data.Category.Void.Void k
instance Data.Category.Limit.HasInitialObject Data.Category.Functor.Cat
instance (Data.Category.Category c, Data.Category.Limit.HasInitialObject d) => Data.Category.Limit.HasInitialObject (Data.Category.NaturalTransformation.Nat c d)
instance (Data.Category.Limit.HasInitialObject c1, Data.Category.Limit.HasInitialObject c2) => Data.Category.Limit.HasInitialObject (c1 Data.Category.Product.:**: c2)
instance Data.Category.Limit.HasInitialObject Data.Category.Unit.Unit
instance (Data.Category.Limit.HasInitialObject c1, Data.Category.Category c2) => Data.Category.Limit.HasInitialObject (c1 Data.Category.Coproduct.:>>: c2)
instance forall k1 (k2 :: k1 -> k1 -> *). Data.Category.Limit.HasInitialObject k2 => Data.Category.Limit.HasTerminalObject (Data.Category.Op k2)
instance forall k1 (k2 :: k1 -> k1 -> *). Data.Category.Limit.HasTerminalObject k2 => Data.Category.Limit.HasInitialObject (Data.Category.Op k2)
instance (Data.Category.Limit.HasInitialObject (i Data.Category.Coproduct.:>>: j), Data.Category.Category i, Data.Category.Category j, Data.Category.Category k) => Data.Category.Limit.HasLimits (i Data.Category.Coproduct.:>>: j) k
instance Data.Category.Limit.HasTerminalObject (FUN 'One)
instance (Data.Category.Category k, Data.Category.Limit.HasTerminalObject k) => Data.Category.Limit.HasLimits Data.Category.Void.Void k
instance Data.Category.Limit.HasTerminalObject (->)
instance Data.Category.Limit.HasTerminalObject Data.Category.Functor.Cat
instance (Data.Category.Category c, Data.Category.Limit.HasTerminalObject d) => Data.Category.Limit.HasTerminalObject (Data.Category.NaturalTransformation.Nat c d)
instance Data.Category.Limit.HasTerminalObject Data.Category.Unit.Unit
instance (Data.Category.Limit.HasTerminalObject c1, Data.Category.Limit.HasTerminalObject c2) => Data.Category.Limit.HasTerminalObject (c1 Data.Category.Product.:**: c2)
instance (Data.Category.Category c1, Data.Category.Limit.HasTerminalObject c2) => Data.Category.Limit.HasTerminalObject (c1 Data.Category.Coproduct.:>>: c2)
instance (Data.Category.Limit.HasTerminalObject (i Data.Category.Coproduct.:>>: j), Data.Category.Category i, Data.Category.Category j, Data.Category.Category k) => Data.Category.Limit.HasColimits (i Data.Category.Coproduct.:>>: j) k
instance Data.Category.Limit.HasColimits j k => Data.Category.Functor.Functor (Data.Category.Limit.ColimitFunctor j k)
instance Data.Category.Category k => Data.Category.Limit.HasColimits Data.Category.Unit.Unit k
instance Data.Category.Limit.HasLimits j k => Data.Category.Functor.Functor (Data.Category.Limit.LimitFunctor j k)
instance Data.Category.Category k => Data.Category.Limit.HasLimits Data.Category.Unit.Unit k
instance (Data.Category.Category j, Data.Category.Category k) => Data.Category.Functor.Functor (Data.Category.Limit.Diag j k)


module Data.Category.KanExtension

-- | An instance of <tt>HasRightKan p k</tt> says there are right Kan
--   extensions for all functors with codomain <tt>k</tt>.
class (Functor p, Category k) => HasRightKan p k where {
    
    -- | The right Kan extension of a functor <tt>p</tt> for functors
    --   <tt>f</tt> with codomain <tt>k</tt>.
    type RanFam p k (f :: Type) :: Type;
}

-- | <a>ran</a> gives the defining natural transformation of the right Kan
--   extension of <tt>f</tt> along <tt>p</tt>.
ran :: HasRightKan p k => p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k (RanFam p k f :.: p) f

-- | <a>ranFactorizer</a> shows that this extension is universal.
ranFactorizer :: HasRightKan p k => Nat (Dom p) k (h :.: p) f -> Nat (Cod p) k h (RanFam p k f)
type Ran p f = RanFam p (Cod f) f
ranF :: HasRightKan p k => p -> Obj (Nat (Dom p) k) f -> Obj (Nat (Cod p) k) (RanFam p k f)
ranF' :: Nat (Dom p) k (RanFam p k f :.: p) f -> Obj (Nat (Cod p) k) (RanFam p k f)
newtype RanFunctor (p :: Type) (k :: Type -> Type -> Type)
RanFunctor :: p -> RanFunctor (p :: Type) (k :: Type -> Type -> Type)

-- | The right Kan extension along <tt>p</tt> is right adjoint to
--   precomposition with <tt>p</tt>.
ranAdj :: forall p k. HasRightKan p k => p -> Adjunction (Nat (Dom p) k) (Nat (Cod p) k) (Precompose p k) (RanFunctor p k)

-- | An instance of <tt>HasLeftKan p k</tt> says there are left Kan
--   extensions for all functors with codomain <tt>k</tt>.
class (Functor p, Category k) => HasLeftKan p k where {
    
    -- | The left Kan extension of a functor <tt>p</tt> for functors <tt>f</tt>
    --   with codomain <tt>k</tt>.
    type LanFam (p :: Type) (k :: Type -> Type -> Type) (f :: Type) :: Type;
}

-- | <a>lan</a> gives the defining natural transformation of the left Kan
--   extension of <tt>f</tt> along <tt>p</tt>.
lan :: HasLeftKan p k => p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k f (LanFam p k f :.: p)

-- | <a>lanFactorizer</a> shows that this extension is universal.
lanFactorizer :: HasLeftKan p k => Nat (Dom p) k f (h :.: p) -> Nat (Cod p) k (LanFam p k f) h
type Lan p f = LanFam p (Cod f) f
lanF :: HasLeftKan p k => p -> Obj (Nat (Dom p) k) f -> Obj (Nat (Cod p) k) (LanFam p k f)
lanF' :: Nat (Dom p) k f (LanFam p k f :.: p) -> Obj (Nat (Cod p) k) (LanFam p k f)
newtype LanFunctor (p :: Type) (k :: Type -> Type -> Type)
LanFunctor :: p -> LanFunctor (p :: Type) (k :: Type -> Type -> Type)

-- | The left Kan extension along <tt>p</tt> is left adjoint to
--   precomposition with <tt>p</tt>.
lanAdj :: forall p k. HasLeftKan p k => p -> Adjunction (Nat (Cod p) k) (Nat (Dom p) k) (LanFunctor p k) (Precompose p k)
newtype RanHask p f a
RanHask :: (forall c. Obj (Dom p) c -> Cod p a (p :% c) -> f :% c) -> RanHask p f a
data RanHaskF p f
RanHaskF :: RanHaskF p f
data LanHask p f a
[LanHask] :: Obj (Dom p) c -> Cod p (p :% c) a -> (f :% c) -> LanHask p f a
data LanHaskF p f
LanHaskF :: LanHaskF p f
instance Data.Category.Functor.Functor p => Data.Category.Functor.Functor (Data.Category.KanExtension.LanHaskF p f)
instance Data.Category.Functor.Functor p => Data.Category.KanExtension.HasLeftKan (Data.Category.Functor.Any p) (->)
instance Data.Category.Functor.Functor p => Data.Category.Functor.Functor (Data.Category.KanExtension.RanHaskF p f)
instance Data.Category.Functor.Functor p => Data.Category.KanExtension.HasRightKan (Data.Category.Functor.Any p) (->)
instance Data.Category.KanExtension.HasLeftKan p k => Data.Category.Functor.Functor (Data.Category.KanExtension.LanFunctor p k)
instance Data.Category.Limit.HasColimits j k => Data.Category.KanExtension.HasLeftKan (Data.Category.Functor.Const j Data.Category.Unit.Unit ()) k
instance (Data.Category.Category j, Data.Category.Category k) => Data.Category.KanExtension.HasLeftKan (Data.Category.Functor.Id j) k
instance (Data.Category.KanExtension.HasLeftKan q k, Data.Category.KanExtension.HasLeftKan p k) => Data.Category.KanExtension.HasLeftKan (q Data.Category.Functor.:.: p) k
instance Data.Category.KanExtension.HasRightKan p k => Data.Category.Functor.Functor (Data.Category.KanExtension.RanFunctor p k)
instance Data.Category.Limit.HasLimits j k => Data.Category.KanExtension.HasRightKan (Data.Category.Functor.Const j Data.Category.Unit.Unit ()) k
instance (Data.Category.Category j, Data.Category.Category k) => Data.Category.KanExtension.HasRightKan (Data.Category.Functor.Id j) k
instance (Data.Category.KanExtension.HasRightKan q k, Data.Category.KanExtension.HasRightKan p k) => Data.Category.KanExtension.HasRightKan (q Data.Category.Functor.:.: p) 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 Unit f :: Kind (Cod 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))
class TensorProduct f => SymmetricTensorProduct f
swap :: (SymmetricTensorProduct f, Cod f ~ k) => f -> Obj k a -> Obj k b -> k (f :% (a, b)) (f :% (b, a))
data LinearTensor
LinearTensor :: LinearTensor

-- | Day convolution
data Day t
Day :: t -> Day t

-- | <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 :: Cod f (Unit f) a -> Cod f (f :% (a, a)) a -> MonoidObject f a
[unit] :: MonoidObject f a -> Cod f (Unit f) a
[multiply] :: MonoidObject f a -> Cod f (f :% (a, a)) a
trivialMonoid :: TensorProduct f => f -> MonoidObject f (Unit f)
coproductMonoid :: (HasInitialObject k, HasBinaryCoproducts k) => Obj k a -> MonoidObject (CoproductFunctor k) 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 :: Cod f a (Unit f) -> Cod f a (f :% (a, a)) -> ComonoidObject f a
[counit] :: ComonoidObject f a -> Cod f a (Unit f)
[comultiply] :: ComonoidObject f a -> Cod f a (f :% (a, a))
trivialComonoid :: TensorProduct f => f -> ComonoidObject f (Unit f)
productComonoid :: (HasTerminalObject k, HasBinaryProducts k) => Obj k a -> ComonoidObject (ProductFunctor k) a
data MonoidAsCategory f m a b
[MonoidValue] :: (TensorProduct f, Dom f ~ (k :**: k), Cod f ~ k) => 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 (EndoFunctorCompose (Dom f)) f
mkMonad :: (Functor f, Dom f ~ k, Cod f ~ 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
idMonad :: Category k => Monad (Id k)

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

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

-- | Every adjunction gives rise to an associated monad transformer.
adjunctionMonadT :: Dom m ~ c => Adjunction c d f g -> Monad m -> Monad ((g :.: m) :.: f)

-- | Every adjunction gives rise to an associated comonad.
adjunctionComonad :: Adjunction c d f g -> Comonad (f :.: g)

-- | Every adjunction gives rise to an associated comonad transformer.
adjunctionComonadT :: Dom w ~ d => Adjunction c d f g -> Comonad w -> Comonad ((f :.: w) :.: g)
instance Data.Category.Category (Data.Category.Monoidal.MonoidAsCategory f m)
instance Data.Category.Monoidal.TensorProduct t => Data.Category.Functor.Functor (Data.Category.Monoidal.Day t)
instance Data.Category.Monoidal.TensorProduct t => Data.Category.Monoidal.TensorProduct (Data.Category.Monoidal.Day t)
instance Data.Category.Functor.Functor Data.Category.Monoidal.LinearTensor
instance Data.Category.Monoidal.TensorProduct Data.Category.Monoidal.LinearTensor
instance Data.Category.Monoidal.SymmetricTensorProduct Data.Category.Monoidal.LinearTensor
instance (Data.Category.Limit.HasTerminalObject k, Data.Category.Limit.HasBinaryProducts k) => Data.Category.Monoidal.SymmetricTensorProduct (Data.Category.Limit.ProductFunctor k)
instance (Data.Category.Limit.HasInitialObject k, Data.Category.Limit.HasBinaryCoproducts k) => Data.Category.Monoidal.SymmetricTensorProduct (Data.Category.Limit.CoproductFunctor k)
instance (Data.Category.Limit.HasTerminalObject k, Data.Category.Limit.HasBinaryProducts k) => Data.Category.Monoidal.TensorProduct (Data.Category.Limit.ProductFunctor k)
instance (Data.Category.Limit.HasInitialObject k, Data.Category.Limit.HasBinaryCoproducts k) => Data.Category.Monoidal.TensorProduct (Data.Category.Limit.CoproductFunctor k)
instance Data.Category.Category k => Data.Category.Monoidal.TensorProduct (Data.Category.NaturalTransformation.EndoFunctorCompose k)


-- | The (augmented) simplex category.
module Data.Category.Simplex
data Simplex :: Type -> Type -> Type
[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 :: Type -> Type
[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 Add (S Z)
data Replicate f a
Replicate :: f -> MonoidObject f a -> Replicate f a
instance Data.Category.Category (Data.Category.Functor.Dom f) => Data.Category.Functor.Functor (Data.Category.Simplex.Cobar f d)
instance Data.Category.Monoidal.TensorProduct f => Data.Category.Functor.Functor (Data.Category.Simplex.Replicate f a)
instance Data.Category.Functor.Functor Data.Category.Simplex.Add
instance Data.Category.Monoidal.TensorProduct Data.Category.Simplex.Add
instance Data.Category.Functor.Functor Data.Category.Simplex.Forget
instance Data.Category.Category Data.Category.Simplex.Simplex
instance Data.Category.Limit.HasInitialObject Data.Category.Simplex.Simplex
instance Data.Category.Limit.HasTerminalObject Data.Category.Simplex.Simplex


-- | 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] :: (Functor m, Dom m ~ k, Cod m ~ k) => 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
newtype KleisliFree m
KleisliFree :: Monad m -> KleisliFree m
data KleisliForget m
KleisliForget :: KleisliForget m
kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Adjunction (Kleisli m) k (KleisliFree m) (KleisliForget m)
instance (Data.Category.Functor.Functor m, Data.Category.Functor.Dom m GHC.Types.~ k, Data.Category.Functor.Cod m GHC.Types.~ k) => Data.Category.Functor.Functor (Data.Category.Kleisli.KleisliForget m)
instance (Data.Category.Functor.Functor m, Data.Category.Functor.Dom m GHC.Types.~ k, Data.Category.Functor.Cod m GHC.Types.~ k) => Data.Category.Functor.Functor (Data.Category.Kleisli.KleisliFree m)
instance Data.Category.Category (Data.Category.Kleisli.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] :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) => 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] :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) => 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
newtype FreeAlg m
FreeAlg :: Monad m -> FreeAlg m
freeAlg :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj (Cod m) x -> Algebra m (m :% x)
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 (Data.Category.Functor.Functor m, Data.Category.Functor.Dom m GHC.Types.~ k, Data.Category.Functor.Cod m GHC.Types.~ k) => Data.Category.Functor.Functor (Data.Category.Dialg.ForgetAlg m)
instance (Data.Category.Functor.Functor m, Data.Category.Functor.Dom m GHC.Types.~ k, Data.Category.Functor.Cod m GHC.Types.~ k) => Data.Category.Functor.Functor (Data.Category.Dialg.FreeAlg m)
instance Data.Category.Limit.HasInitialObject (Data.Category.Dialg.Dialg (Data.Category.Functor.Tuple1 (->) (->) ()) (Data.Category.Functor.DiagProd (->)))
instance Data.Category.Category (Data.Category.Dialg.Dialg f g)


-- | The cube category.
module Data.Category.Cube
data Z
data S n
data Sign
M :: Sign
P :: Sign
data Cube :: Type -> Type -> Type
[Z] :: Cube Z Z
[S] :: Cube x y -> Cube (S x) (S y)
[Y] :: Sign -> Cube x y -> Cube x (S y)
[X] :: Cube x y -> Cube (S x) y
data Sign0
SM :: Sign0
S0 :: Sign0
SP :: Sign0
data ACube :: Type -> Type
[Nil] :: ACube Z
[Cons] :: Sign0 -> ACube n -> ACube (S n)
data Forget
Forget :: Forget
data Add
Add :: Add
instance Data.Category.Functor.Functor Data.Category.Cube.Add
instance Data.Category.Monoidal.TensorProduct Data.Category.Cube.Add
instance Data.Category.Functor.Functor Data.Category.Cube.Forget
instance Data.Category.Category Data.Category.Cube.Cube
instance Data.Category.Limit.HasTerminalObject Data.Category.Cube.Cube


-- | Comma categories.
module Data.Category.Comma
data CommaO :: Type -> Type -> Type -> Type
[CommaO] :: (Cod t ~ k, Cod s ~ k) => Obj (Dom t) a -> k (t :% a) (s :% b) -> Obj (Dom s) b -> CommaO t s (a, b)
data (:/\:) :: Type -> Type -> Type -> Type -> Type
[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 f `ObjectsFUnder` a = ConstF f a :/\: f
type f `ObjectsFOver` a = f :/\: ConstF f a
type c `ObjectsUnder` a = Id c `ObjectsFUnder` a
type c `ObjectsOver` a = Id c `ObjectsFOver` a
initialUniversalComma :: forall u x c a a_. (Functor u, c ~ (u `ObjectsFUnder` x), HasInitialObject c, (a_, a) ~ InitialObject c) => u -> InitialUniversal x u a
terminalUniversalComma :: forall u x c a a_. (Functor u, c ~ (u `ObjectsFOver` x), HasTerminalObject c, (a, a_) ~ TerminalObject c) => u -> TerminalUniversal x u a
type Arrows k = Id k :/\: Id k
data IdArrow (k :: Type -> Type -> Type)
IdArrow :: IdArrow (k :: Type -> Type -> Type)
data Src (k :: Type -> Type -> Type)
Src :: Src (k :: Type -> Type -> Type)
data Tgt (k :: Type -> Type -> Type)
Tgt :: Tgt (k :: Type -> Type -> Type)

-- | Taking the target of an arrow is left adjoint to taking the identity
--   of an object
tgtIdAdj :: Category k => Adjunction k (Arrows k) (Tgt k) (IdArrow k)

-- | Taking the source of an arrow is right adjoint to taking the identity
--   of an object
idSrcAdj :: Category k => Adjunction (Arrows k) k (IdArrow k) (Src k)
instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Comma.Tgt k)
instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Comma.Src k)
instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Comma.IdArrow k)
instance (Data.Category.Category (Data.Category.Functor.Dom t), Data.Category.Category (Data.Category.Functor.Dom s)) => Data.Category.Category (t Data.Category.Comma.:/\: s)


module Data.Category.WeightedLimit
type WeightedCone w d e = forall a. Obj (Dom w) a -> w :% a -> Cod d e (d :% a)

-- | <tt>w</tt>-weighted limits in the category <tt>k</tt>.
class (Functor w, Cod w ~ (->), Category k) => HasWLimits k w where {
    type WeightedLimit k w d :: Type;
}
limitObj :: (HasWLimits k w, FunctorOf (Dom w) k d) => w -> d -> Obj k (WLimit w d)
limit :: (HasWLimits k w, FunctorOf (Dom w) k d) => w -> d -> WeightedCone w d (WLimit w d)
limitFactorizer :: (HasWLimits k w, FunctorOf (Dom w) k d) => w -> d -> Obj k e -> WeightedCone w d e -> k e (WLimit w d)
type WLimit w d = WeightedLimit (Cod d) w d
data LimitFunctor (k :: Type -> Type -> Type) w
LimitFunctor :: w -> LimitFunctor (k :: Type -> Type -> Type) w
class Category v => HasEnds v where {
    type End (v :: Type -> Type -> Type) t :: Type;
}
end :: (HasEnds v, FunctorOf (Op k :**: k) v t) => t -> Obj v (End v t)
endCounit :: (HasEnds v, FunctorOf (Op k :**: k) v t) => t -> Obj k a -> v (End v t) (t :% (a, a))
endFactorizer :: (HasEnds v, FunctorOf (Op k :**: k) v t) => t -> (forall a. Obj k a -> v x (t :% (a, a))) -> v x (End v t)
data EndFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type)
EndFunctor :: EndFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type)
newtype HaskEnd t
HaskEnd :: (forall k a. FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> t :% (a, a)) -> HaskEnd t
[getHaskEnd] :: HaskEnd t -> forall k a. FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> t :% (a, a)
type WeightedCocone w d e = forall a. Obj (Dom w) a -> w :% a -> Cod d (d :% a) e

-- | <tt>w</tt>-weighted colimits in the category <tt>k</tt>.
class (Functor w, Cod w ~ (->), Category k) => HasWColimits k w where {
    type WeightedColimit k w d :: Type;
}
colimitObj :: (HasWColimits k w, FunctorOf j k d, Op j ~ Dom w) => w -> d -> Obj k (WColimit w d)
colimit :: (HasWColimits k w, FunctorOf j k d, Op j ~ Dom w) => w -> d -> WeightedCocone w d (WColimit w d)
colimitFactorizer :: (HasWColimits k w, FunctorOf j k d, Op j ~ Dom w) => w -> d -> Obj k e -> WeightedCocone w d e -> k (WColimit w d) e
type WColimit w d = WeightedColimit (Cod d) w d
data ColimitFunctor (k :: Type -> Type -> Type) w
ColimitFunctor :: w -> ColimitFunctor (k :: Type -> Type -> Type) w
class Category v => HasCoends v where {
    type Coend (v :: Type -> Type -> Type) t :: Type;
}
coend :: (HasCoends v, FunctorOf (Op k :**: k) v t) => t -> Obj v (Coend v t)
coendCounit :: (HasCoends v, FunctorOf (Op k :**: k) v t) => t -> Obj k a -> v (t :% (a, a)) (Coend v t)
coendFactorizer :: (HasCoends v, FunctorOf (Op k :**: k) v t) => t -> (forall a. Obj k a -> v (t :% (a, a)) x) -> v (Coend v t) x
data OpHom (k :: Type -> Type -> Type)
OpHom :: OpHom (k :: Type -> Type -> Type)
data CoendFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type)
CoendFunctor :: CoendFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type)
data HaskCoend t
[HaskCoend] :: FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> (t :% (a, a)) -> HaskCoend t
instance Data.Category.WeightedLimit.HasCoends (->)
instance (Data.Category.WeightedLimit.HasCoends v, Data.Category.Category k) => Data.Category.Functor.Functor (Data.Category.WeightedLimit.CoendFunctor k v)
instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.WeightedLimit.OpHom k)
instance Data.Category.WeightedLimit.HasCoends k => Data.Category.WeightedLimit.HasWColimits k (Data.Category.WeightedLimit.OpHom k)
instance (Data.Category.Functor.Functor w, Data.Category.Category k, Data.Category.WeightedLimit.HasWColimits k (w Data.Category.Functor.:.: Data.Category.Functor.OpOp (Data.Category.Functor.Dom w))) => Data.Category.Functor.Functor (Data.Category.WeightedLimit.ColimitFunctor k w)
instance Data.Category.Limit.HasColimits j k => Data.Category.WeightedLimit.HasWColimits k (Data.Category.Functor.Const (Data.Category.Op j) (->) ())
instance Data.Category.WeightedLimit.HasEnds (->)
instance (Data.Category.WeightedLimit.HasEnds v, Data.Category.Category k) => Data.Category.Functor.Functor (Data.Category.WeightedLimit.EndFunctor k v)
instance Data.Category.WeightedLimit.HasEnds k => Data.Category.WeightedLimit.HasWLimits k (Data.Category.Functor.Hom k)
instance Data.Category.WeightedLimit.HasWLimits k w => Data.Category.Functor.Functor (Data.Category.WeightedLimit.LimitFunctor k w)
instance Data.Category.Limit.HasLimits j k => Data.Category.WeightedLimit.HasWLimits k (Data.Category.Functor.Const j (->) ())


module Data.Category.Yoneda
type YonedaEmbedding k = Curry2 (Op k) k (Hom k)

-- | The Yoneda embedding functor, <tt>C -&gt; Set^(C^op)</tt>.
pattern YonedaEmbedding :: Category k => YonedaEmbedding k
data Yoneda (k :: Type -> Type -> Type) f
Yoneda :: Yoneda (k :: Type -> Type -> Type) 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 -> Nat (Op k) (->) (Yoneda k f) f
toYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) f (Yoneda k f)
haskUnit :: Obj (->) ()
data M1
M1 :: M1
haskIsTotal :: Adjunction (->) (Nat (Op (->)) (->)) M1 (YonedaEmbedding (->))
instance Data.Category.Functor.Functor Data.Category.Yoneda.M1
instance (Data.Category.Category k, Data.Category.Functor.Functor f, Data.Category.Functor.Dom f GHC.Types.~ Data.Category.Op k, Data.Category.Functor.Cod f GHC.Types.~ (->)) => Data.Category.Functor.Functor (Data.Category.Yoneda.Yoneda k f)


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 where {
    type Exponential k (y :: Kind k) (z :: Kind k) :: Kind 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 :: Type -> Type -> Type)
ExpFunctor :: ExpFunctor (k :: Type -> Type -> Type)
flip :: CartesianClosed k => Obj k a -> Obj k b -> Obj k c -> k (Exponential k a (Exponential k b c)) (Exponential k b (Exponential k a c))
type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite (ProductFunctor (Presheaves k) :.: Tuple2 (Presheaves k) (Presheaves k) y :.: YonedaEmbedding k)
pattern PshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z

-- | 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, Kind k ~ Type) => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z)
uncurry :: (CartesianClosed k, Kind k ~ Type) => 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, Kind k ~ Type) => Obj k s -> Obj k a -> k a (State k s a)
stateMonadJoin :: (CartesianClosed k, Kind k ~ Type) => 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, Kind k ~ Type) => Obj k s -> Obj k a -> k (Context k s a) a
contextComonadDuplicate :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a))
instance Data.Category.Category k => Data.Category.CartesianClosed.CartesianClosed (Data.Category.NaturalTransformation.Presheaves k)
instance Data.Category.CartesianClosed.CartesianClosed k => Data.Category.Functor.Functor (Data.Category.CartesianClosed.ExpFunctor k)
instance Data.Category.CartesianClosed.CartesianClosed (->)
instance Data.Category.CartesianClosed.CartesianClosed Data.Category.Unit.Unit
instance Data.Category.CartesianClosed.CartesianClosed Data.Category.Functor.Cat


module Data.Category.Fix
newtype Fix f a b
Fix :: f (Fix f) a b -> Fix f a b
data Wrap (f :: Type -> Type -> Type)
Wrap :: Wrap (f :: Type -> Type -> Type)
data Unwrap (f :: Type -> Type -> Type)
Unwrap :: Unwrap (f :: Type -> Type -> Type)
type WrapTensor f t = Wrap f :.: t :.: (Unwrap f :***: Unwrap f)

-- | 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)
type Z = I1 ()
type S n = I2 n
pattern Z :: Obj Omega Z
pattern S :: Omega a b -> Omega (S a) (S b)
z2s :: Obj Omega n -> Omega Z (S n)
instance Data.Category.Category (f (Data.Category.Fix.Fix f)) => Data.Category.Category (Data.Category.Fix.Fix f)
instance (Data.Category.Monoidal.TensorProduct t, Data.Category.Functor.Cod t GHC.Types.~ f (Data.Category.Fix.Fix f)) => Data.Category.Monoidal.TensorProduct (Data.Category.Fix.WrapTensor (Data.Category.Fix.Fix f) t)
instance Data.Category.Category (f (Data.Category.Fix.Fix f)) => Data.Category.Functor.Functor (Data.Category.Fix.Unwrap (Data.Category.Fix.Fix f))
instance Data.Category.Category (f (Data.Category.Fix.Fix f)) => Data.Category.Functor.Functor (Data.Category.Fix.Wrap (Data.Category.Fix.Fix f))
instance Data.Category.Limit.HasInitialObject (f (Data.Category.Fix.Fix f)) => Data.Category.Limit.HasInitialObject (Data.Category.Fix.Fix f)
instance Data.Category.Limit.HasTerminalObject (f (Data.Category.Fix.Fix f)) => Data.Category.Limit.HasTerminalObject (Data.Category.Fix.Fix f)
instance Data.Category.Limit.HasBinaryProducts (f (Data.Category.Fix.Fix f)) => Data.Category.Limit.HasBinaryProducts (Data.Category.Fix.Fix f)
instance Data.Category.Limit.HasBinaryCoproducts (f (Data.Category.Fix.Fix f)) => Data.Category.Limit.HasBinaryCoproducts (Data.Category.Fix.Fix f)
instance Data.Category.CartesianClosed.CartesianClosed (f (Data.Category.Fix.Fix f)) => Data.Category.CartesianClosed.CartesianClosed (Data.Category.Fix.Fix f)


module Data.Category.NNO
class HasTerminalObject k => HasNaturalNumberObject k where {
    type NaturalNumberObject k :: Type;
}
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
instance Data.Category.NNO.HasNaturalNumberObject (->)

module Data.Category.Fin
data Nat
Z :: Nat
S :: Nat -> Nat
data Fin n
[FZ] :: Fin ('S n)
[FS] :: Fin n -> Fin ('S n)
data LTE (n :: Nat) (a :: Fin n) (b :: Fin n)
[ZEQ] :: LTE ('S m) 'FZ 'FZ
[ZLT] :: LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
[SLT] :: LTE ('S m) a b -> LTE ('S ('S m)) ('FS a) ('FS b)
data Proof a n
[Proof] :: (BinaryProduct (LTE ('S n)) 'FZ a ~ 'FZ, BinaryProduct (LTE ('S n)) a 'FZ ~ 'FZ) => Proof a n
proof :: Obj (LTE ('S n)) a -> Proof a n
instance Data.Category.CartesianClosed.CartesianClosed (Data.Category.Fin.LTE ('Data.Category.Fin.S n)) => Data.Category.CartesianClosed.CartesianClosed (Data.Category.Fin.LTE ('Data.Category.Fin.S ('Data.Category.Fin.S n)))
instance Data.Category.Category (Data.Category.Fin.LTE n)
instance Data.Category.Limit.HasInitialObject (Data.Category.Fin.LTE ('Data.Category.Fin.S n))
instance Data.Category.Limit.HasTerminalObject (Data.Category.Fin.LTE ('Data.Category.Fin.S 'Data.Category.Fin.Z))
instance Data.Category.Limit.HasTerminalObject (Data.Category.Fin.LTE ('Data.Category.Fin.S n)) => Data.Category.Limit.HasTerminalObject (Data.Category.Fin.LTE ('Data.Category.Fin.S ('Data.Category.Fin.S n)))
instance Data.Category.Limit.HasBinaryCoproducts (Data.Category.Fin.LTE ('Data.Category.Fin.S 'Data.Category.Fin.Z))
instance Data.Category.Limit.HasBinaryCoproducts (Data.Category.Fin.LTE ('Data.Category.Fin.S n)) => Data.Category.Limit.HasBinaryCoproducts (Data.Category.Fin.LTE ('Data.Category.Fin.S ('Data.Category.Fin.S n)))
instance Data.Category.Limit.HasBinaryProducts (Data.Category.Fin.LTE ('Data.Category.Fin.S 'Data.Category.Fin.Z))
instance Data.Category.Limit.HasBinaryProducts (Data.Category.Fin.LTE ('Data.Category.Fin.S n)) => Data.Category.Limit.HasBinaryProducts (Data.Category.Fin.LTE ('Data.Category.Fin.S ('Data.Category.Fin.S n)))
instance Data.Category.CartesianClosed.CartesianClosed (Data.Category.Fin.LTE ('Data.Category.Fin.S 'Data.Category.Fin.Z))


module Data.Category.Enriched

-- | An enriched category
class CartesianClosed (V k) => ECategory (k :: Type -> Type -> Type) where {
    
    -- | The category V which k is enriched in
    type V k :: Type -> Type -> Type;
    
    -- | The hom object in V from a to b
    type k $ ab :: Type;
}
hom :: ECategory k => Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
id :: ECategory k => Obj k a -> Arr k a a
comp :: ECategory k => Obj k a -> Obj k b -> Obj k c -> V k (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b))) (k $ (a, c))

-- | Arrows as elements of <tt>k</tt>
type Arr k a b = V k (TerminalObject (V k)) (k $ (a, b))
compArr :: ECategory k => Obj k a -> Obj k b -> Obj k c -> Arr k b c -> Arr k a b -> Arr k a c
data Underlying k a b
Underlying :: Obj k a -> Arr k a b -> Obj k b -> Underlying k a b
newtype EOp k a b
EOp :: k b a -> EOp k a b
data (:<>:) :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type
[:<>:] :: V k1 ~ V k2 => Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)
newtype Self v a b
Self :: v a b -> Self v a b
[getSelf] :: Self v a b -> v a b
toSelf :: CartesianClosed v => v a b -> Arr (Self v) a b
fromSelf :: forall v a b. CartesianClosed v => Obj v a -> Obj v b -> Arr (Self v) a b -> v a b
newtype InHask k a b
InHask :: k a b -> InHask k a b
instance Data.Category.Category k => Data.Category.Enriched.ECategory (Data.Category.Enriched.InHask k)
instance Data.Category.CartesianClosed.CartesianClosed v => Data.Category.Enriched.ECategory (Data.Category.Enriched.Self v)
instance (Data.Category.Enriched.ECategory k1, Data.Category.Enriched.ECategory k2, Data.Category.Enriched.V k1 GHC.Types.~ Data.Category.Enriched.V k2) => Data.Category.Enriched.ECategory (k1 Data.Category.Enriched.:<>: k2)
instance Data.Category.Enriched.ECategory k => Data.Category.Enriched.ECategory (Data.Category.Enriched.EOp k)
instance Data.Category.Enriched.ECategory k => Data.Category.Category (Data.Category.Enriched.Underlying k)


module Data.Category.Enriched.Functor

-- | Enriched functors.
class (ECategory (EDom ftag), ECategory (ECod ftag), V (EDom ftag) ~ V (ECod ftag)) => EFunctor ftag where {
    
    -- | The domain, or source category, of the functor.
    type EDom ftag :: Type -> Type -> Type;
    
    -- | The codomain, or target category, of the functor.
    type ECod ftag :: Type -> Type -> Type;
    
    -- | <tt>:%%</tt> maps objects at the type level
    type ftag :%% a :: Type;
}

-- | <tt>%%</tt> maps object at the value level
(%%) :: EFunctor ftag => ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)

-- | <a>map</a> maps arrows.
map :: (EFunctor ftag, EDom ftag ~ k) => ftag -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))
type EFunctorOf a b t = (EFunctor t, EDom t ~ a, ECod t ~ b)
data Id (k :: Type -> Type -> Type)
Id :: Id (k :: Type -> Type -> Type)
data g :.: h
[:.:] :: (EFunctor g, EFunctor h, ECod h ~ EDom g) => g -> h -> g :.: h
data Const (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) x
[Const] :: Obj c2 x -> Const c1 c2 x
data Opposite f
[Opposite] :: EFunctor f => f -> Opposite f
data f1 :<*>: f2
(:<*>:) :: f1 -> f2 -> (:<*>:) f1 f2
data DiagProd (k :: Type -> Type -> Type)
DiagProd :: DiagProd (k :: Type -> Type -> Type)
newtype UnderlyingF f
UnderlyingF :: f -> UnderlyingF f
newtype InHaskF f
InHaskF :: f -> InHaskF f
newtype InHaskToHask f
InHaskToHask :: f -> InHaskToHask f
newtype UnderlyingHask (c :: Type -> Type -> Type) (d :: Type -> Type -> Type) f
UnderlyingHask :: f -> UnderlyingHask (c :: Type -> Type -> Type) (d :: Type -> Type -> Type) f
data EHom (k :: Type -> Type -> Type)
EHom :: EHom (k :: Type -> Type -> Type)

-- | The enriched functor <tt>k(x, -)</tt>
data EHomX_ k x
EHomX_ :: Obj k x -> EHomX_ k x

-- | The enriched functor <tt>k(-, x)</tt>
data EHom_X k x
EHom_X :: Obj (EOp k) x -> EHom_X k x

-- | A V-enrichment on a functor <tt>F: V -&gt; V</tt> is the same thing as
--   tensorial strength <tt>(a, f b) -&gt; f (a, b)</tt>.
strength :: EFunctorOf (Self v) (Self v) f => f -> Obj v a -> Obj v b -> v (BinaryProduct v a (f :%% b)) (f :%% BinaryProduct v a b)

-- | Enriched natural transformations.
data ENat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type
[ENat] :: (EFunctorOf c d f, EFunctorOf c d g) => f -> g -> (forall z. Obj c z -> Arr d (f :%% z) (g :%% z)) -> ENat c d f g
instance Data.Category.Enriched.ECategory k => Data.Category.Enriched.Functor.EFunctor (Data.Category.Enriched.Functor.EHom_X k x)
instance Data.Category.Enriched.ECategory k => Data.Category.Enriched.Functor.EFunctor (Data.Category.Enriched.Functor.EHomX_ k x)
instance Data.Category.Enriched.ECategory k => Data.Category.Enriched.Functor.EFunctor (Data.Category.Enriched.Functor.EHom k)
instance (Data.Category.Enriched.Functor.EFunctor f, Data.Category.Enriched.Functor.EDom f GHC.Types.~ Data.Category.Enriched.InHask c, Data.Category.Enriched.Functor.ECod f GHC.Types.~ Data.Category.Enriched.InHask d, Data.Category.Category c, Data.Category.Category d) => Data.Category.Functor.Functor (Data.Category.Enriched.Functor.UnderlyingHask c d f)
instance (Data.Category.Functor.Functor f, Data.Category.Functor.Cod f GHC.Types.~ (->)) => Data.Category.Enriched.Functor.EFunctor (Data.Category.Enriched.Functor.InHaskToHask f)
instance Data.Category.Functor.Functor f => Data.Category.Enriched.Functor.EFunctor (Data.Category.Enriched.Functor.InHaskF f)
instance Data.Category.Enriched.Functor.EFunctor f => Data.Category.Functor.Functor (Data.Category.Enriched.Functor.UnderlyingF f)
instance Data.Category.Enriched.ECategory k => Data.Category.Enriched.Functor.EFunctor (Data.Category.Enriched.Functor.DiagProd k)
instance (Data.Category.Enriched.Functor.EFunctor f1, Data.Category.Enriched.Functor.EFunctor f2, Data.Category.Enriched.V (Data.Category.Enriched.Functor.ECod f1) GHC.Types.~ Data.Category.Enriched.V (Data.Category.Enriched.Functor.ECod f2)) => Data.Category.Enriched.Functor.EFunctor (f1 Data.Category.Enriched.Functor.:<*>: f2)
instance Data.Category.Enriched.Functor.EFunctor f => Data.Category.Enriched.Functor.EFunctor (Data.Category.Enriched.Functor.Opposite f)
instance (Data.Category.Enriched.ECategory c1, Data.Category.Enriched.ECategory c2, Data.Category.Enriched.V c1 GHC.Types.~ Data.Category.Enriched.V c2) => Data.Category.Enriched.Functor.EFunctor (Data.Category.Enriched.Functor.Const c1 c2 x)
instance (Data.Category.Enriched.ECategory (Data.Category.Enriched.Functor.ECod g), Data.Category.Enriched.ECategory (Data.Category.Enriched.Functor.EDom h), Data.Category.Enriched.V (Data.Category.Enriched.Functor.EDom h) GHC.Types.~ Data.Category.Enriched.V (Data.Category.Enriched.Functor.ECod g), Data.Category.Enriched.Functor.ECod h GHC.Types.~ Data.Category.Enriched.Functor.EDom g) => Data.Category.Enriched.Functor.EFunctor (g Data.Category.Enriched.Functor.:.: h)
instance Data.Category.Enriched.ECategory k => Data.Category.Enriched.Functor.EFunctor (Data.Category.Enriched.Functor.Id k)


module Data.Category.Enriched.Limit
type VProfunctor k l t = EFunctorOf (EOp k :<>: l) (Self (V k)) t
class CartesianClosed v => HasEnds v where {
    type End (v :: Type -> Type -> Type) t :: Type;
}
end :: (HasEnds v, VProfunctor k k t, V k ~ v) => t -> Obj v (End v t)
endCounit :: (HasEnds v, VProfunctor k k t, V k ~ v) => t -> Obj k a -> v (End v t) (t :%% (a, a))
endFactorizer :: (HasEnds v, VProfunctor k k t, V k ~ v) => t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)
newtype HaskEnd t
HaskEnd :: (forall k a. VProfunctor k k t => t -> Obj k a -> t :%% (a, a)) -> HaskEnd t
[getHaskEnd] :: HaskEnd t -> forall k a. VProfunctor k k t => t -> Obj k a -> t :%% (a, a)
data FunCat a b t s
[FArr] :: (EFunctorOf a b t, EFunctorOf a b s) => t -> s -> FunCat a b t s
type t :->>: s = EHom (ECod t) :.: (Opposite t :<*>: s)
(->>) :: (EFunctor t, EFunctor s, ECod t ~ ECod s, V (ECod t) ~ V (ECod s)) => t -> s -> t :->>: s
data EndFunctor (k :: Type -> Type -> Type)
EndFunctor :: EndFunctor (k :: Type -> Type -> Type)
type family WeigtedLimit (k :: Type -> Type -> Type) w d :: Type
type Lim w d = WeigtedLimit (ECod d) w d
class (HasEnds (V k), EFunctor w, ECod w ~ Self (V k)) => HasLimits k w
limitObj :: (HasLimits k w, EFunctorOf (EDom w) k d) => w -> d -> Obj k (Lim w d)
limit :: (HasLimits k w, EFunctorOf (EDom w) k d) => w -> d -> Obj k e -> V k (k $ (e, Lim w d)) (End (V k) (w :->>: (EHomX_ k e :.: d)))
limitInv :: (HasLimits k w, EFunctorOf (EDom w) k d) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHomX_ k e :.: d))) (k $ (e, Lim w d))
type family WeigtedColimit (k :: Type -> Type -> Type) w d :: Type
type Colim w d = WeigtedColimit (ECod d) w d
class (HasEnds (V k), EFunctor w, ECod w ~ Self (V k)) => HasColimits k w
colimitObj :: (HasColimits k w, EFunctorOf j k d, EOp j ~ EDom w) => w -> d -> Obj k (Colim w d)
colimit :: (HasColimits k w, EFunctorOf j k d, EOp j ~ EDom w) => w -> d -> Obj k e -> V k (k $ (Colim w d, e)) (End (V k) (w :->>: (EHom_X k e :.: Opposite d)))
colimitInv :: (HasColimits k w, EFunctorOf j k d, EOp j ~ EDom w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHom_X k e :.: Opposite d))) (k $ (Colim w d, e))
instance (Data.Category.Enriched.Limit.HasEnds v, Data.Category.Enriched.Functor.EFunctor w, Data.Category.Enriched.Functor.ECod w GHC.Types.~ Data.Category.Enriched.Self v) => Data.Category.Enriched.Limit.HasLimits (Data.Category.Enriched.Self v) w
instance Data.Category.WeightedLimit.HasWLimits k w => Data.Category.Enriched.Limit.HasLimits (Data.Category.Enriched.InHask k) (Data.Category.Enriched.Functor.InHaskToHask w)
instance (Data.Category.Enriched.Limit.HasEnds (Data.Category.Enriched.V k), Data.Category.Enriched.ECategory k) => Data.Category.Enriched.Functor.EFunctor (Data.Category.Enriched.Limit.EndFunctor k)
instance (Data.Category.Enriched.Limit.HasEnds (Data.Category.Enriched.V a), Data.Category.CartesianClosed.CartesianClosed (Data.Category.Enriched.V a), Data.Category.Enriched.V a GHC.Types.~ Data.Category.Enriched.V b) => Data.Category.Enriched.ECategory (Data.Category.Enriched.Limit.FunCat a b)
instance Data.Category.Enriched.Limit.HasEnds (->)

module Data.Category.Preorder
data Preorder a x y
[:<=:] :: a -> a -> Preorder a x y
pattern Obj :: a -> Preorder a x y
unObj :: Obj (Preorder a) x -> a

-- | `ordExp a b` is the largest x such that min x a &lt;= b
ordExp :: (Ord a, Bounded a) => a -> a -> a
class Category k => EnumObjs k
enumObjs :: EnumObjs k => (forall a. Obj k a -> r) -> [r]
glb :: (Ord a, Bounded a) => [a] -> a
type End' t = ()
end :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a) => t -> Obj (Preorder a) (End' t)
endCounit :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a) => t -> Obj k b -> Preorder a (End' t) (t :%% (b, b))
endFactorizer :: (VProfunctor k k t, V k ~ Preorder a, EnumObjs k, Ord a, Bounded a) => t -> Obj (Preorder a) x -> (forall b. Obj k b -> Preorder a x (t :%% (b, b))) -> Preorder a x (End' t)
data Floor
Floor :: Floor
data FromInteger
FromInteger :: FromInteger
floorGaloisConnection :: Adjunction (Preorder Double) (Preorder Integer) FromInteger Floor
instance Data.Category.Functor.Functor Data.Category.Preorder.FromInteger
instance Data.Category.Functor.Functor Data.Category.Preorder.Floor
instance GHC.Classes.Eq a => Data.Category.Category (Data.Category.Preorder.Preorder a)
instance (GHC.Classes.Eq a, GHC.Enum.Bounded a) => Data.Category.Limit.HasInitialObject (Data.Category.Preorder.Preorder a)
instance (GHC.Classes.Eq a, GHC.Enum.Bounded a) => Data.Category.Limit.HasTerminalObject (Data.Category.Preorder.Preorder a)
instance GHC.Classes.Ord a => Data.Category.Limit.HasBinaryProducts (Data.Category.Preorder.Preorder a)
instance GHC.Classes.Ord a => Data.Category.Limit.HasBinaryCoproducts (Data.Category.Preorder.Preorder a)
instance (GHC.Classes.Ord a, GHC.Enum.Bounded a) => Data.Category.CartesianClosed.CartesianClosed (Data.Category.Preorder.Preorder a)


module Data.Category.Enriched.Yoneda
yoneda :: forall f k x. (HasEnds (V k), EFunctorOf k (Self (V k)) f) => f -> Obj k x -> V k (End (V k) (EHomX_ k x :->>: f)) (f :%% x)
yonedaInv :: forall f k x. (HasEnds (V k), EFunctor f, EDom f ~ k, ECod f ~ Self (V k)) => f -> Obj k x -> V k (f :%% x) (End (V k) (EHomX_ k x :->>: f))
data Y (k :: Type -> Type -> Type)
Y :: Y (k :: Type -> Type -> Type)
instance (Data.Category.Enriched.ECategory k, Data.Category.Enriched.Limit.HasEnds (Data.Category.Enriched.V k)) => Data.Category.Enriched.Functor.EFunctor (Data.Category.Enriched.Yoneda.Y k)


-- | <i>2</i> a.k.a. the Boolean category a.k.a. the walking arrow. It
--   contains 2 objects, one for false and one for true. 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
newtype Arrow k a b
Arrow :: k a b -> Arrow k a b

-- | The source functor sends arrows (as functors from the Boolean
--   category) to their source.
type SrcFunctor = LimitFunctor Boolean

-- | The target functor sends arrows (as functors from the Boolean
--   category) to their target.
type TgtFunctor = ColimitFunctor Boolean
data Terminator (k :: Type -> Type -> Type)
Terminator :: Terminator (k :: Type -> Type -> Type)

-- | <tt>Terminator</tt> is right adjoint to the source functor.
terminatorLimitAdj :: HasTerminalObject k => Adjunction k (Nat Boolean k) (SrcFunctor k) (Terminator k)
data Initializer (k :: Type -> Type -> Type)
Initializer :: Initializer (k :: Type -> Type -> Type)

-- | <tt>Initializer</tt> is left adjoint to the target functor.
initializerColimitAdj :: HasInitialObject k => Adjunction (Nat Boolean k) k (Initializer k) (TgtFunctor k)
instance Data.Category.Limit.HasInitialObject k => Data.Category.Functor.Functor (Data.Category.Boolean.Initializer k)
instance Data.Category.Limit.HasTerminalObject k => Data.Category.Functor.Functor (Data.Category.Boolean.Terminator k)
instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Boolean.Arrow k a b)
instance Data.Category.Category Data.Category.Boolean.Boolean
instance Data.Category.Limit.HasInitialObject Data.Category.Boolean.Boolean
instance Data.Category.Limit.HasTerminalObject Data.Category.Boolean.Boolean
instance Data.Category.Limit.HasBinaryProducts Data.Category.Boolean.Boolean
instance Data.Category.Limit.HasBinaryCoproducts Data.Category.Boolean.Boolean
instance Data.Category.CartesianClosed.CartesianClosed Data.Category.Boolean.Boolean
instance Data.Category.Category k => Data.Category.Limit.HasLimits Data.Category.Boolean.Boolean k
instance Data.Category.Category k => Data.Category.Limit.HasColimits Data.Category.Boolean.Boolean k


module Data.Category.Enriched.Poset3
data One
data Two
data Three
data PosetTest a b
[One] :: PosetTest One One
[Two] :: PosetTest Two Two
[Three] :: PosetTest Three Three
type family Poset3 a b
instance Data.Category.Enriched.ECategory Data.Category.Enriched.Poset3.PosetTest