License	BSD-style (see the file LICENSE)
Maintainer	sjoerd@w3future.com
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Category.Limit

Contents

Preliminairies
- Diagonal Functor
- Cones
Limits
Colimits
- Limits of type Void
- Limits of type Pair

Description

Synopsis

data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where
- Diag :: Diag j k
type DiagF f = Diag (Dom f) (Cod f)
type Cone f n = Nat (Dom f) (Cod f) (ConstF f n) f
type Cocone f n = Nat (Dom f) (Cod f) f (ConstF f n)
coneVertex :: Cone f n -> Obj (Cod f) n
coconeVertex :: Cocone f n -> Obj (Cod f) n
type family LimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *
type Limit f = LimitFam (Dom f) (Cod f) f
class (Category j, Category k) => HasLimits j k where
- limit :: Obj (Nat j k) f -> Cone f (Limit f)
- limitFactorizer :: Obj (Nat j k) f -> Cone f n -> k n (Limit f)
data LimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) = LimitFunctor
limitAdj :: forall j k. HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
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 :% Limit t) (Limit (g :.: t))
type family ColimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *
type Colimit f = ColimitFam (Dom f) (Cod f) f
class (Category j, Category k) => HasColimits j k where
- colimit :: Obj (Nat j k) f -> Cocone f (Colimit f)
- colimitFactorizer :: Obj (Nat j k) f -> Cocone f n -> k (Colimit f) n
data ColimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) = ColimitFunctor
colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
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 (Colimit (f :.: t)) (f :% Colimit t)
class Category k => HasTerminalObject k where
- type TerminalObject k :: *
- terminalObject :: Obj k (TerminalObject k)
- terminate :: Obj k a -> k a (TerminalObject k)
class Category k => HasInitialObject k where
- type InitialObject k :: *
- initialObject :: Obj k (InitialObject k)
- initialize :: Obj k a -> k (InitialObject k) a
data Zero
class Category k => HasBinaryProducts k where
- type BinaryProduct (k :: * -> * -> *) x y :: *
- proj1 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) x
- proj2 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) y
- (&&&) :: k a x -> k a y -> k a (BinaryProduct k x y)
- (***) :: k a1 b1 -> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
data ProductFunctor (k :: * -> * -> *) = ProductFunctor
data p :*: q where
- (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q
prodAdj :: HasBinaryProducts k => Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)
class Category k => HasBinaryCoproducts k where
- type BinaryCoproduct (k :: * -> * -> *) x y :: *
- inj1 :: Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
- inj2 :: Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
- (|||) :: k x a -> k y a -> k (BinaryCoproduct k x y) a
- (+++) :: k a1 b1 -> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
data CoproductFunctor (k :: * -> * -> *) = CoproductFunctor
data p :+: q where
- (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q
coprodAdj :: HasBinaryCoproducts k => Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)

Preliminairies

Diagonal Functor

data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where Source #

Constructors

Diag :: Diag j k

Instances

(Category j, Category k) => Functor (Diag j k) Source #	The diagonal functor from (index-) category J to k.
Instance details Defined in Data.Category.Limit Associated Types type Dom (Diag j k) :: Type -> Type -> Type Source # type Cod (Diag j k) :: Type -> Type -> Type Source # type (Diag j k) :% a :: Type Source # Methods (%) :: Diag j k -> Dom (Diag j k) a b -> Cod (Diag j k) (Diag j k :% a) (Diag j k :% b) Source #
type Dom (Diag j k) Source #
Instance details Defined in Data.Category.Limit type Dom (Diag j k) = k
type Cod (Diag j k) Source #
Instance details Defined in Data.Category.Limit type Cod (Diag j k) = Nat j k
type (Diag j k) :% a Source #
Instance details Defined in Data.Category.Limit type (Diag j k) :% a = Const j k a

type DiagF f = Diag (Dom f) (Cod f) Source #

The diagonal functor with the same domain and codomain as f.

Cones

type Cone f n = Nat (Dom f) (Cod f) (ConstF f n) f Source #

A cone from N to F is a natural transformation from the constant functor to N to F.

type Cocone f n = Nat (Dom f) (Cod f) f (ConstF f n) Source #

A co-cone from F to N is a natural transformation from F to the constant functor to N.

coneVertex :: Cone f n -> Obj (Cod f) n Source #

The vertex (or apex) of a cone.

coconeVertex :: Cocone f n -> Obj (Cod f) n Source #

The vertex (or apex) of a co-cone.

Limits

type family LimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: * Source #

Limits in a category k by means of a diagram of type j, which is a functor from j to k.

Instances

type LimitFam Unit k f Source #
Instance details Defined in Data.Category.Limit type LimitFam Unit k f = f :% ()
type LimitFam Void k f Source #
Instance details Defined in Data.Category.Limit type LimitFam Void k f = TerminalObject k
type LimitFam Boolean k f Source #
Instance details Defined in Data.Category.Boolean type LimitFam Boolean k f = f :% Fls
type LimitFam (i :>>: j) k f Source #
Instance details Defined in Data.Category.Limit type LimitFam (i :>>: j) k f = f :% InitialObject (i :>>: j)
type LimitFam (i :++: j) k f Source #
Instance details Defined in Data.Category.Limit type LimitFam (i :++: j) k f = BinaryProduct k (LimitFam i k (f :.: Inj1 i j)) (LimitFam j k (f :.: Inj2 i j))
type LimitFam ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) f Source #
Instance details Defined in Data.Category.Limit type LimitFam ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) f

type Limit f = LimitFam (Dom f) (Cod f) f Source #

class (Category j, Category k) => HasLimits j k where Source #

An instance of HasLimits j k says that k has all limits of type j.

Methods

limit :: Obj (Nat j k) f -> Cone f (Limit f) Source #

limit returns the limiting cone for a functor f.

limitFactorizer :: Obj (Nat j k) f -> Cone f n -> k n (Limit f) Source #

limitFactorizer shows that the limiting cone is universal – i.e. any other cone of f factors through it by returning the morphism between the vertices of the cones.

Instances

Category k => HasLimits Unit k Source #	The limit of a single object is that object.
Instance details Defined in Data.Category.Limit Methods limit :: Obj (Nat Unit k) f -> Cone f (Limit f) Source # limitFactorizer :: Obj (Nat Unit k) f -> Cone f n -> k n (Limit f) Source #
HasTerminalObject k => HasLimits Void k Source #	A terminal object is the limit of the functor from 0 to k.
Instance details Defined in Data.Category.Limit Methods limit :: Obj (Nat Void k) f -> Cone f (Limit f) Source # limitFactorizer :: Obj (Nat Void k) f -> Cone f n -> k n (Limit f) Source #
Category k => HasLimits Boolean k Source #	The limit of a functor from the Boolean category is the source of the arrow it points to.
Instance details Defined in Data.Category.Boolean Methods limit :: Obj (Nat Boolean k) f -> Cone f (Limit f) Source # limitFactorizer :: Obj (Nat Boolean k) f -> Cone f n -> k n (Limit f) Source #
(HasInitialObject (i :>>: j), Category k) => HasLimits (i :>>: j) k Source #	The limit of any diagram with an initial object, has the limit at the initial object.
Instance details Defined in Data.Category.Limit Methods limit :: Obj (Nat (i :>>: j) k) f -> Cone f (Limit f) Source # limitFactorizer :: Obj (Nat (i :>>: j) k) f -> Cone f n -> k n (Limit f) Source #
(HasLimits i k, HasLimits j k, HasBinaryProducts k) => HasLimits (i :++: j) k Source #	If `k` has binary products, we can take the limit of 2 joined diagrams.
Instance details Defined in Data.Category.Limit Methods limit :: Obj (Nat (i :++: j) k) f -> Cone f (Limit f) Source # limitFactorizer :: Obj (Nat (i :++: j) k) f -> Cone f n -> k n (Limit f) Source #
HasLimits ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) Source #
Instance details Defined in Data.Category.Limit Methods limit :: Obj (Nat (->) (->)) f -> Cone f (Limit f) Source # limitFactorizer :: Obj (Nat (->) (->)) f -> Cone f n -> n -> Limit f Source #

data LimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) Source #

Constructors

LimitFunctor

Instances

HasLimits j k => Functor (LimitFunctor j k) Source #	If every diagram of type `j` has a limit in `k` there exists a limit functor. It can be seen as a generalisation of `(***)`.
Instance details Defined in Data.Category.Limit Associated Types type Dom (LimitFunctor j k) :: Type -> Type -> Type Source # type Cod (LimitFunctor j k) :: Type -> Type -> Type Source # type (LimitFunctor j k) :% a :: Type Source # Methods (%) :: LimitFunctor j k -> Dom (LimitFunctor j k) a b -> Cod (LimitFunctor j k) (LimitFunctor j k :% a) (LimitFunctor j k :% b) Source #
type Dom (LimitFunctor j k) Source #
Instance details Defined in Data.Category.Limit type Dom (LimitFunctor j k) = Nat j k
type Cod (LimitFunctor j k) Source #
Instance details Defined in Data.Category.Limit type Cod (LimitFunctor j k) = k
type (LimitFunctor j k) :% f Source #
Instance details Defined in Data.Category.Limit type (LimitFunctor j k) :% f = LimitFam j k f

limitAdj :: forall j k. HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k) Source #

The limit functor is right adjoint to the diagonal functor.

rightAdjointPreservesLimits :: (HasLimits j c, HasLimits j d) => Adjunction c d f g -> Obj (Nat j c) t -> d (Limit (g :.: t)) (g :% Limit t) Source #

rightAdjointPreservesLimitsInv :: (HasLimits j c, HasLimits j d) => Obj (Nat c d) g -> Obj (Nat j c) t -> d (g :% Limit t) (Limit (g :.: t)) Source #

Colimits

type family ColimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: * Source #

Colimits in a category k by means of a diagram of type j, which is a functor from j to k.

Instances

type ColimitFam Unit k f Source #
Instance details Defined in Data.Category.Limit type ColimitFam Unit k f = f :% ()
type ColimitFam Void k f Source #
Instance details Defined in Data.Category.Limit type ColimitFam Void k f = InitialObject k
type ColimitFam Boolean k f Source #
Instance details Defined in Data.Category.Boolean type ColimitFam Boolean k f = f :% Tru
type ColimitFam (i :>>: j) k f Source #
Instance details Defined in Data.Category.Limit type ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j)
type ColimitFam (i :++: j) k f Source #
Instance details Defined in Data.Category.Limit type ColimitFam (i :++: j) k f = BinaryCoproduct k (ColimitFam i k (f :.: Inj1 i j)) (ColimitFam j k (f :.: Inj2 i j))
type ColimitFam ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) f Source #
Instance details Defined in Data.Category.Limit type ColimitFam ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) f

type Colimit f = ColimitFam (Dom f) (Cod f) f Source #

class (Category j, Category k) => HasColimits j k where Source #

An instance of HasColimits j k says that k has all colimits of type j.

Methods

colimit :: Obj (Nat j k) f -> Cocone f (Colimit f) Source #

colimit returns the limiting co-cone for a functor f.

colimitFactorizer :: Obj (Nat j k) f -> Cocone f n -> k (Colimit f) n Source #

colimitFactorizer shows that the limiting co-cone is universal – i.e. any other co-cone of f factors through it by returning the morphism between the vertices of the cones.

Instances

Category k => HasColimits Unit k Source #	The colimit of a single object is that object.
Instance details Defined in Data.Category.Limit Methods colimit :: Obj (Nat Unit k) f -> Cocone f (Colimit f) Source # colimitFactorizer :: Obj (Nat Unit k) f -> Cocone f n -> k (Colimit f) n Source #
HasInitialObject k => HasColimits Void k Source #	An initial object is the colimit of the functor from 0 to k.
Instance details Defined in Data.Category.Limit Methods colimit :: Obj (Nat Void k) f -> Cocone f (Colimit f) Source # colimitFactorizer :: Obj (Nat Void k) f -> Cocone f n -> k (Colimit f) n Source #
Category k => HasColimits Boolean k Source #	The colimit of a functor from the Boolean category is the target of the arrow it points to.
Instance details Defined in Data.Category.Boolean Methods colimit :: Obj (Nat Boolean k) f -> Cocone f (Colimit f) Source # colimitFactorizer :: Obj (Nat Boolean k) f -> Cocone f n -> k (Colimit f) n Source #
(HasTerminalObject (i :>>: j), Category k) => HasColimits (i :>>: j) k Source #	The colimit of any diagram with a terminal object, has the limit at the terminal object.
Instance details Defined in Data.Category.Limit Methods colimit :: Obj (Nat (i :>>: j) k) f -> Cocone f (Colimit f) Source # colimitFactorizer :: Obj (Nat (i :>>: j) k) f -> Cocone f n -> k (Colimit f) n Source #
(HasColimits i k, HasColimits j k, HasBinaryCoproducts k) => HasColimits (i :++: j) k Source #	If `k` has binary coproducts, we can take the colimit of 2 joined diagrams.
Instance details Defined in Data.Category.Limit Methods colimit :: Obj (Nat (i :++: j) k) f -> Cocone f (Colimit f) Source # colimitFactorizer :: Obj (Nat (i :++: j) k) f -> Cocone f n -> k (Colimit f) n Source #
HasColimits ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) Source #
Instance details Defined in Data.Category.Limit Methods colimit :: Obj (Nat (->) (->)) f -> Cocone f (Colimit f) Source # colimitFactorizer :: Obj (Nat (->) (->)) f -> Cocone f n -> Colimit f -> n Source #

data ColimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) Source #

Constructors

ColimitFunctor

Instances

HasColimits j k => Functor (ColimitFunctor j k) Source #	If every diagram of type `j` has a colimit in `k` there exists a colimit functor. It can be seen as a generalisation of `(+++)`.
Instance details Defined in Data.Category.Limit Associated Types type Dom (ColimitFunctor j k) :: Type -> Type -> Type Source # type Cod (ColimitFunctor j k) :: Type -> Type -> Type Source # type (ColimitFunctor j k) :% a :: Type Source # Methods (%) :: ColimitFunctor j k -> Dom (ColimitFunctor j k) a b -> Cod (ColimitFunctor j k) (ColimitFunctor j k :% a) (ColimitFunctor j k :% b) Source #
type Dom (ColimitFunctor j k) Source #
Instance details Defined in Data.Category.Limit type Dom (ColimitFunctor j k) = Nat j k
type Cod (ColimitFunctor j k) Source #
Instance details Defined in Data.Category.Limit type Cod (ColimitFunctor j k) = k
type (ColimitFunctor j k) :% f Source #
Instance details Defined in Data.Category.Limit type (ColimitFunctor j k) :% f = ColimitFam j k f

colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k) Source #

The colimit functor is left adjoint to the diagonal functor.

leftAdjointPreservesColimits :: (HasColimits j c, HasColimits j d) => Adjunction c d f g -> Obj (Nat j d) t -> c (f :% Colimit t) (Colimit (f :.: t)) Source #

leftAdjointPreservesColimitsInv :: (HasColimits j c, HasColimits j d) => Obj (Nat d c) f -> Obj (Nat j d) t -> c (Colimit (f :.: t)) (f :% Colimit t) Source #

Limits of type Void

class Category k => HasTerminalObject k where Source #

Associated Types

type TerminalObject k :: * Source #

Methods

terminalObject :: Obj k (TerminalObject k) Source #

terminate :: Obj k a -> k a (TerminalObject k) Source #

Instances

HasTerminalObject Cat Source #	`Unit` is the terminal category.
Instance details Defined in Data.Category.Limit Associated Types type TerminalObject Cat :: Type Source # Methods terminalObject :: Obj Cat (TerminalObject Cat) Source # terminate :: Obj Cat a -> Cat a (TerminalObject Cat) Source #
HasTerminalObject Unit Source #	The category of one object has that object as terminal object.
Instance details Defined in Data.Category.Limit Associated Types type TerminalObject Unit :: Type Source # Methods terminalObject :: Obj Unit (TerminalObject Unit) Source # terminate :: Obj Unit a -> Unit a (TerminalObject Unit) Source #
HasTerminalObject Simplex Source #	The ordinal `1` is the terminal object of the simplex category.
Instance details Defined in Data.Category.Simplex Associated Types type TerminalObject Simplex :: Type Source # Methods terminalObject :: Obj Simplex (TerminalObject Simplex) Source # terminate :: Obj Simplex a -> Simplex a (TerminalObject Simplex) Source #
HasTerminalObject Cube Source #
Instance details Defined in Data.Category.Cube Associated Types type TerminalObject Cube :: Type Source # Methods terminalObject :: Obj Cube (TerminalObject Cube) Source # terminate :: Obj Cube a -> Cube a (TerminalObject Cube) Source #
HasTerminalObject Boolean Source #	True is the terminal object in the Boolean category.
Instance details Defined in Data.Category.Boolean Associated Types type TerminalObject Boolean :: Type Source # Methods terminalObject :: Obj Boolean (TerminalObject Boolean) Source # terminate :: Obj Boolean a -> Boolean a (TerminalObject Boolean) Source #
HasInitialObject k => HasTerminalObject (Op k) Source #	Terminal objects are the dual of initial objects.
Instance details Defined in Data.Category.Limit Associated Types type TerminalObject (Op k) :: Type Source # Methods terminalObject :: Obj (Op k) (TerminalObject (Op k)) Source # terminate :: Obj (Op k) a -> Op k a (TerminalObject (Op k)) Source #
HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f) Source #
Instance details Defined in Data.Category.Fix Associated Types type TerminalObject (Fix f) :: Type Source # Methods terminalObject :: Obj (Fix f) (TerminalObject (Fix f)) Source # terminate :: Obj (Fix f) a -> Fix f a (TerminalObject (Fix f)) Source #
HasTerminalObject ((->) :: Type -> Type -> Type) Source #	`()` is the terminal object in `Hask`.
Instance details Defined in Data.Category.Limit Associated Types type TerminalObject (->) :: Type Source # Methods terminalObject :: Obj (->) (TerminalObject (->)) Source # terminate :: Obj (->) a -> a -> TerminalObject (->) Source #
(HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (c1 :**: c2) Source #	The terminal object of the product of 2 categories is the product of their terminal objects.
Instance details Defined in Data.Category.Limit Associated Types type TerminalObject (c1 :: c2) :: Type Source # Methods terminalObject :: Obj (c1 :: c2) (TerminalObject (c1 :: c2)) Source # terminate :: Obj (c1 :: c2) a -> (c1 :: c2) a (TerminalObject (c1 :: c2)) Source #
(Category c, HasTerminalObject d) => HasTerminalObject (Nat c d) Source #	The constant functor to the terminal object is itself the terminal object in its functor category.
Instance details Defined in Data.Category.Limit Associated Types type TerminalObject (Nat c d) :: Type Source # Methods terminalObject :: Obj (Nat c d) (TerminalObject (Nat c d)) Source # terminate :: Obj (Nat c d) a -> Nat c d a (TerminalObject (Nat c d)) Source #
(Category c1, HasTerminalObject c2) => HasTerminalObject (c1 :>>: c2) Source #	The terminal object of the direct coproduct of categories is the terminal object of the terminal category.
Instance details Defined in Data.Category.Limit Associated Types type TerminalObject (c1 :>>: c2) :: Type Source # Methods terminalObject :: Obj (c1 :>>: c2) (TerminalObject (c1 :>>: c2)) Source # terminate :: Obj (c1 :>>: c2) a -> (c1 :>>: c2) a (TerminalObject (c1 :>>: c2)) Source #

class Category k => HasInitialObject k where Source #

Associated Types

type InitialObject k :: * Source #

Methods

initialObject :: Obj k (InitialObject k) Source #

initialize :: Obj k a -> k (InitialObject k) a Source #

Instances

HasInitialObject Cat Source #	The empty category is the initial object in `Cat`.
Instance details Defined in Data.Category.Limit Associated Types type InitialObject Cat :: Type Source # Methods initialObject :: Obj Cat (InitialObject Cat) Source # initialize :: Obj Cat a -> Cat (InitialObject Cat) a Source #
HasInitialObject Unit Source #	The category of one object has that object as initial object.
Instance details Defined in Data.Category.Limit Associated Types type InitialObject Unit :: Type Source # Methods initialObject :: Obj Unit (InitialObject Unit) Source # initialize :: Obj Unit a -> Unit (InitialObject Unit) a Source #
HasInitialObject Simplex Source #	The ordinal `0` is the initial object of the simplex category.
Instance details Defined in Data.Category.Simplex Associated Types type InitialObject Simplex :: Type Source # Methods initialObject :: Obj Simplex (InitialObject Simplex) Source # initialize :: Obj Simplex a -> Simplex (InitialObject Simplex) a Source #
HasInitialObject Boolean Source #	False is the initial object in the Boolean category.
Instance details Defined in Data.Category.Boolean Associated Types type InitialObject Boolean :: Type Source # Methods initialObject :: Obj Boolean (InitialObject Boolean) Source # initialize :: Obj Boolean a -> Boolean (InitialObject Boolean) a Source #
HasTerminalObject k => HasInitialObject (Op k) Source #	Terminal objects are the dual of initial objects.
Instance details Defined in Data.Category.Limit Associated Types type InitialObject (Op k) :: Type Source # Methods initialObject :: Obj (Op k) (InitialObject (Op k)) Source # initialize :: Obj (Op k) a -> Op k (InitialObject (Op k)) a Source #
HasInitialObject (f (Fix f)) => HasInitialObject (Fix f) Source #
Instance details Defined in Data.Category.Fix Associated Types type InitialObject (Fix f) :: Type Source # Methods initialObject :: Obj (Fix f) (InitialObject (Fix f)) Source # initialize :: Obj (Fix f) a -> Fix f (InitialObject (Fix f)) a Source #
HasInitialObject ((->) :: Type -> Type -> Type) Source #	Any empty data type is an initial object in `Hask`.
Instance details Defined in Data.Category.Limit Associated Types type InitialObject (->) :: Type Source # Methods initialObject :: Obj (->) (InitialObject (->)) Source # initialize :: Obj (->) a -> InitialObject (->) -> a Source #
(HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2) Source #	The initial object of the product of 2 categories is the product of their initial objects.
Instance details Defined in Data.Category.Limit Associated Types type InitialObject (c1 :: c2) :: Type Source # Methods initialObject :: Obj (c1 :: c2) (InitialObject (c1 :: c2)) Source # initialize :: Obj (c1 :: c2) a -> (c1 :: c2) (InitialObject (c1 :: c2)) a Source #
(Category c, HasInitialObject d) => HasInitialObject (Nat c d) Source #	The constant functor to the initial object is itself the initial object in its functor category.
Instance details Defined in Data.Category.Limit Associated Types type InitialObject (Nat c d) :: Type Source # Methods initialObject :: Obj (Nat c d) (InitialObject (Nat c d)) Source # initialize :: Obj (Nat c d) a -> Nat c d (InitialObject (Nat c d)) a Source #
(HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2) Source #	The initial object of the direct coproduct of categories is the initial object of the initial category.
Instance details Defined in Data.Category.Limit Associated Types type InitialObject (c1 :>>: c2) :: Type Source # Methods initialObject :: Obj (c1 :>>: c2) (InitialObject (c1 :>>: c2)) Source # initialize :: Obj (c1 :>>: c2) a -> (c1 :>>: c2) (InitialObject (c1 :>>: c2)) a Source #
HasInitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) Source #	The category for defining the natural numbers and primitive recursion can be described as `Dialg(F,G)`, with `F(A)=<1,A>` and `G(A)=<A,A>`.
Instance details Defined in Data.Category.Dialg Associated Types type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) :: Type Source # Methods initialObject :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) Source # initialize :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a -> Dialg (Tuple1 (->) (->) ()) (DiagProd (->)) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) a Source #

data Zero Source #

Limits of type Pair

class Category k => HasBinaryProducts k where Source #

Minimal complete definition

proj1, proj2, (&&&)

Associated Types

type BinaryProduct (k :: * -> * -> *) x y :: * Source #

Methods

proj1 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) x Source #

proj2 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) y Source #

(&&&) :: k a x -> k a y -> k a (BinaryProduct k x y) infixl 3 Source #

(***) :: k a1 b1 -> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2) infixl 3 Source #

Instances

HasBinaryProducts Cat Source #	The product of categories `:**:` is the binary product in `Cat`.
Instance details Defined in Data.Category.Limit Associated Types type BinaryProduct Cat x y :: Type Source # Methods proj1 :: Obj Cat x -> Obj Cat y -> Cat (BinaryProduct Cat x y) x Source # proj2 :: Obj Cat x -> Obj Cat y -> Cat (BinaryProduct Cat x y) y Source # (&&&) :: Cat a x -> Cat a y -> Cat a (BinaryProduct Cat x y) Source # (***) :: Cat a1 b1 -> Cat a2 b2 -> Cat (BinaryProduct Cat a1 a2) (BinaryProduct Cat b1 b2) Source #
HasBinaryProducts Unit Source #	In the category of one object that object is its own product.
Instance details Defined in Data.Category.Limit Associated Types type BinaryProduct Unit x y :: Type Source # Methods proj1 :: Obj Unit x -> Obj Unit y -> Unit (BinaryProduct Unit x y) x Source # proj2 :: Obj Unit x -> Obj Unit y -> Unit (BinaryProduct Unit x y) y Source # (&&&) :: Unit a x -> Unit a y -> Unit a (BinaryProduct Unit x y) Source # (***) :: Unit a1 b1 -> Unit a2 b2 -> Unit (BinaryProduct Unit a1 a2) (BinaryProduct Unit b1 b2) Source #
HasBinaryProducts Boolean Source #	Conjunction is the binary product in the Boolean category.
Instance details Defined in Data.Category.Boolean Associated Types type BinaryProduct Boolean x y :: Type Source # Methods proj1 :: Obj Boolean x -> Obj Boolean y -> Boolean (BinaryProduct Boolean x y) x Source # proj2 :: Obj Boolean x -> Obj Boolean y -> Boolean (BinaryProduct Boolean x y) y Source # (&&&) :: Boolean a x -> Boolean a y -> Boolean a (BinaryProduct Boolean x y) Source # (***) :: Boolean a1 b1 -> Boolean a2 b2 -> Boolean (BinaryProduct Boolean a1 a2) (BinaryProduct Boolean b1 b2) Source #
HasBinaryCoproducts k => HasBinaryProducts (Op k) Source #	Binary products are the dual of binary coproducts.
Instance details Defined in Data.Category.Limit Associated Types type BinaryProduct (Op k) x y :: Type Source # Methods proj1 :: Obj (Op k) x -> Obj (Op k) y -> Op k (BinaryProduct (Op k) x y) x Source # proj2 :: Obj (Op k) x -> Obj (Op k) y -> Op k (BinaryProduct (Op k) x y) y Source # (&&&) :: Op k a x -> Op k a y -> Op k a (BinaryProduct (Op k) x y) Source # (***) :: Op k a1 b1 -> Op k a2 b2 -> Op k (BinaryProduct (Op k) a1 a2) (BinaryProduct (Op k) b1 b2) Source #
HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f) Source #
Instance details Defined in Data.Category.Fix Associated Types type BinaryProduct (Fix f) x y :: Type Source # Methods proj1 :: Obj (Fix f) x -> Obj (Fix f) y -> Fix f (BinaryProduct (Fix f) x y) x Source # proj2 :: Obj (Fix f) x -> Obj (Fix f) y -> Fix f (BinaryProduct (Fix f) x y) y Source # (&&&) :: Fix f a x -> Fix f a y -> Fix f a (BinaryProduct (Fix f) x y) Source # (***) :: Fix f a1 b1 -> Fix f a2 b2 -> Fix f (BinaryProduct (Fix f) a1 a2) (BinaryProduct (Fix f) b1 b2) Source #
HasBinaryProducts ((->) :: Type -> Type -> Type) Source #	The tuple is the binary product in `Hask`.
Instance details Defined in Data.Category.Limit Associated Types type BinaryProduct (->) x y :: Type Source # Methods proj1 :: Obj (->) x -> Obj (->) y -> BinaryProduct (->) x y -> x Source # proj2 :: Obj (->) x -> Obj (->) y -> BinaryProduct (->) x y -> y Source # (&&&) :: (a -> x) -> (a -> y) -> a -> BinaryProduct (->) x y Source # (***) :: (a1 -> b1) -> (a2 -> b2) -> BinaryProduct (->) a1 a2 -> BinaryProduct (->) b1 b2 Source #
(HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2) Source #	The binary product of the product of 2 categories is the product of their binary products.
Instance details Defined in Data.Category.Limit Associated Types type BinaryProduct (c1 :: c2) x y :: Type Source # Methods proj1 :: Obj (c1 :: c2) x -> Obj (c1 :: c2) y -> (c1 :: c2) (BinaryProduct (c1 :: c2) x y) x Source # proj2 :: Obj (c1 :: c2) x -> Obj (c1 :: c2) y -> (c1 :: c2) (BinaryProduct (c1 :: c2) x y) y Source # (&&&) :: (c1 :: c2) a x -> (c1 :: c2) a y -> (c1 :: c2) a (BinaryProduct (c1 :: c2) x y) Source # () :: (c1 :: c2) a1 b1 -> (c1 :: c2) a2 b2 -> (c1 :: c2) (BinaryProduct (c1 :: c2) a1 a2) (BinaryProduct (c1 :*: c2) b1 b2) Source #
(Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) Source #	The functor product `:*:` is the binary product in functor categories.
Instance details Defined in Data.Category.Limit Associated Types type BinaryProduct (Nat c d) x y :: Type Source # Methods proj1 :: Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d (BinaryProduct (Nat c d) x y) x Source # proj2 :: Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d (BinaryProduct (Nat c d) x y) y Source # (&&&) :: Nat c d a x -> Nat c d a y -> Nat c d a (BinaryProduct (Nat c d) x y) Source # (***) :: Nat c d a1 b1 -> Nat c d a2 b2 -> Nat c d (BinaryProduct (Nat c d) a1 a2) (BinaryProduct (Nat c d) b1 b2) Source #
(HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :>>: c2) Source #
Instance details Defined in Data.Category.Limit Associated Types type BinaryProduct (c1 :>>: c2) x y :: Type Source # Methods proj1 :: Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) (BinaryProduct (c1 :>>: c2) x y) x Source # proj2 :: Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) (BinaryProduct (c1 :>>: c2) x y) y Source # (&&&) :: (c1 :>>: c2) a x -> (c1 :>>: c2) a y -> (c1 :>>: c2) a (BinaryProduct (c1 :>>: c2) x y) Source # (***) :: (c1 :>>: c2) a1 b1 -> (c1 :>>: c2) a2 b2 -> (c1 :>>: c2) (BinaryProduct (c1 :>>: c2) a1 a2) (BinaryProduct (c1 :>>: c2) b1 b2) Source #

data ProductFunctor (k :: * -> * -> *) Source #

Constructors

ProductFunctor

Instances

HasBinaryProducts k => Functor (ProductFunctor k) Source #	Binary product as a bifunctor.
Instance details Defined in Data.Category.Limit Associated Types type Dom (ProductFunctor k) :: Type -> Type -> Type Source # type Cod (ProductFunctor k) :: Type -> Type -> Type Source # type (ProductFunctor k) :% a :: Type Source # Methods (%) :: ProductFunctor k -> Dom (ProductFunctor k) a b -> Cod (ProductFunctor k) (ProductFunctor k :% a) (ProductFunctor k :% b) Source #
(HasTerminalObject k, HasBinaryProducts k) => SymmetricTensorProduct (ProductFunctor k) Source #
Instance details Defined in Data.Category.Monoidal Methods swap :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> Obj k0 b -> k0 (ProductFunctor k :% (a, b)) (ProductFunctor k :% (b, a)) Source #
(HasTerminalObject k, HasBinaryProducts k) => TensorProduct (ProductFunctor k) Source #	If a category has all products, then the product functor makes it a monoidal category, with the terminal object as unit.
Instance details Defined in Data.Category.Monoidal Associated Types type Unit (ProductFunctor k) :: Type Source # Methods unitObject :: ProductFunctor k -> Obj (Cod (ProductFunctor k)) (Unit (ProductFunctor k)) Source # leftUnitor :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> k0 (ProductFunctor k :% (Unit (ProductFunctor k), a)) a Source # leftUnitorInv :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> k0 a (ProductFunctor k :% (Unit (ProductFunctor k), a)) Source # rightUnitor :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> k0 (ProductFunctor k :% (a, Unit (ProductFunctor k))) a Source # rightUnitorInv :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> k0 a (ProductFunctor k :% (a, Unit (ProductFunctor k))) Source # associator :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> Obj k0 b -> Obj k0 c -> k0 (ProductFunctor k :% (ProductFunctor k :% (a, b), c)) (ProductFunctor k :% (a, ProductFunctor k :% (b, c))) Source # associatorInv :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> Obj k0 b -> Obj k0 c -> k0 (ProductFunctor k :% (a, ProductFunctor k :% (b, c))) (ProductFunctor k :% (ProductFunctor k :% (a, b), c)) Source #
type Dom (ProductFunctor k) Source #
Instance details Defined in Data.Category.Limit type Dom (ProductFunctor k) = k :**: k
type Cod (ProductFunctor k) Source #
Instance details Defined in Data.Category.Limit type Cod (ProductFunctor k) = k
type Unit (ProductFunctor k) Source #
Instance details Defined in Data.Category.Monoidal type Unit (ProductFunctor k) = TerminalObject k
type (ProductFunctor k) :% (a, b) Source #
Instance details Defined in Data.Category.Limit type (ProductFunctor k) :% (a, b) = BinaryProduct k a b

data p :*: q where Source #

Constructors

(:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q

Instances

(Category (Dom p), Category (Cod p)) => Functor (p :*: q) Source #	The product of two functors, passing the same object to both functors and taking the product of the results.
Instance details Defined in Data.Category.Limit Associated Types type Dom (p :: q) :: Type -> Type -> Type Source # type Cod (p :: q) :: Type -> Type -> Type Source # type (p :: q) :% a :: Type Source # Methods (%) :: (p :: q) -> Dom (p :: q) a b -> Cod (p :: q) ((p :: q) :% a) ((p :: q) :% b) Source #
type Dom (p :*: q) Source #
Instance details Defined in Data.Category.Limit type Dom (p :*: q) = Dom p
type Cod (p :*: q) Source #
Instance details Defined in Data.Category.Limit type Cod (p :*: q) = Cod p
type (p :*: q) :% a Source #
Instance details Defined in Data.Category.Limit type (p :*: q) :% a = BinaryProduct (Cod p) (p :% a) (q :% a)

prodAdj :: HasBinaryProducts k => Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k) Source #

A specialisation of the limit adjunction to products.

class Category k => HasBinaryCoproducts k where Source #

Minimal complete definition

inj1, inj2, (|||)

Associated Types

type BinaryCoproduct (k :: * -> * -> *) x y :: * Source #

Methods

inj1 :: Obj k x -> Obj k y -> k x (BinaryCoproduct k x y) Source #

inj2 :: Obj k x -> Obj k y -> k y (BinaryCoproduct k x y) Source #

(|||) :: k x a -> k y a -> k (BinaryCoproduct k x y) a infixl 2 Source #

(+++) :: k a1 b1 -> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2) infixl 2 Source #

Instances

HasBinaryCoproducts Cat Source #	The coproduct of categories `:++:` is the binary coproduct in `Cat`.
Instance details Defined in Data.Category.Limit Associated Types type BinaryCoproduct Cat x y :: Type Source # Methods inj1 :: Obj Cat x -> Obj Cat y -> Cat x (BinaryCoproduct Cat x y) Source # inj2 :: Obj Cat x -> Obj Cat y -> Cat y (BinaryCoproduct Cat x y) Source # (\|\|\|) :: Cat x a -> Cat y a -> Cat (BinaryCoproduct Cat x y) a Source # (+++) :: Cat a1 b1 -> Cat a2 b2 -> Cat (BinaryCoproduct Cat a1 a2) (BinaryCoproduct Cat b1 b2) Source #
HasBinaryCoproducts Unit Source #	In the category of one object that object is its own coproduct.
Instance details Defined in Data.Category.Limit Associated Types type BinaryCoproduct Unit x y :: Type Source # Methods inj1 :: Obj Unit x -> Obj Unit y -> Unit x (BinaryCoproduct Unit x y) Source # inj2 :: Obj Unit x -> Obj Unit y -> Unit y (BinaryCoproduct Unit x y) Source # (\|\|\|) :: Unit x a -> Unit y a -> Unit (BinaryCoproduct Unit x y) a Source # (+++) :: Unit a1 b1 -> Unit a2 b2 -> Unit (BinaryCoproduct Unit a1 a2) (BinaryCoproduct Unit b1 b2) Source #
HasBinaryCoproducts Boolean Source #	Disjunction is the binary coproduct in the Boolean category.
Instance details Defined in Data.Category.Boolean Associated Types type BinaryCoproduct Boolean x y :: Type Source # Methods inj1 :: Obj Boolean x -> Obj Boolean y -> Boolean x (BinaryCoproduct Boolean x y) Source # inj2 :: Obj Boolean x -> Obj Boolean y -> Boolean y (BinaryCoproduct Boolean x y) Source # (\|\|\|) :: Boolean x a -> Boolean y a -> Boolean (BinaryCoproduct Boolean x y) a Source # (+++) :: Boolean a1 b1 -> Boolean a2 b2 -> Boolean (BinaryCoproduct Boolean a1 a2) (BinaryCoproduct Boolean b1 b2) Source #
HasBinaryProducts k => HasBinaryCoproducts (Op k) Source #	Binary products are the dual of binary coproducts.
Instance details Defined in Data.Category.Limit Associated Types type BinaryCoproduct (Op k) x y :: Type Source # Methods inj1 :: Obj (Op k) x -> Obj (Op k) y -> Op k x (BinaryCoproduct (Op k) x y) Source # inj2 :: Obj (Op k) x -> Obj (Op k) y -> Op k y (BinaryCoproduct (Op k) x y) Source # (\|\|\|) :: Op k x a -> Op k y a -> Op k (BinaryCoproduct (Op k) x y) a Source # (+++) :: Op k a1 b1 -> Op k a2 b2 -> Op k (BinaryCoproduct (Op k) a1 a2) (BinaryCoproduct (Op k) b1 b2) Source #
HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f) Source #
Instance details Defined in Data.Category.Fix Associated Types type BinaryCoproduct (Fix f) x y :: Type Source # Methods inj1 :: Obj (Fix f) x -> Obj (Fix f) y -> Fix f x (BinaryCoproduct (Fix f) x y) Source # inj2 :: Obj (Fix f) x -> Obj (Fix f) y -> Fix f y (BinaryCoproduct (Fix f) x y) Source # (\|\|\|) :: Fix f x a -> Fix f y a -> Fix f (BinaryCoproduct (Fix f) x y) a Source # (+++) :: Fix f a1 b1 -> Fix f a2 b2 -> Fix f (BinaryCoproduct (Fix f) a1 a2) (BinaryCoproduct (Fix f) b1 b2) Source #
(HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2) Source #	The binary coproduct of the product of 2 categories is the product of their binary coproducts.
Instance details Defined in Data.Category.Limit Associated Types type BinaryCoproduct (c1 :: c2) x y :: Type Source # Methods inj1 :: Obj (c1 :: c2) x -> Obj (c1 :: c2) y -> (c1 :: c2) x (BinaryCoproduct (c1 :: c2) x y) Source # inj2 :: Obj (c1 :: c2) x -> Obj (c1 :: c2) y -> (c1 :: c2) y (BinaryCoproduct (c1 :: c2) x y) Source # (\|\|\|) :: (c1 :: c2) x a -> (c1 :: c2) y a -> (c1 :: c2) (BinaryCoproduct (c1 :: c2) x y) a Source # (+++) :: (c1 :: c2) a1 b1 -> (c1 :: c2) a2 b2 -> (c1 :: c2) (BinaryCoproduct (c1 :: c2) a1 a2) (BinaryCoproduct (c1 :: c2) b1 b2) Source #
(Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) Source #	The functor coproduct `:+:` is the binary coproduct in functor categories.
Instance details Defined in Data.Category.Limit Associated Types type BinaryCoproduct (Nat c d) x y :: Type Source # Methods inj1 :: Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d x (BinaryCoproduct (Nat c d) x y) Source # inj2 :: Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d y (BinaryCoproduct (Nat c d) x y) Source # (\|\|\|) :: Nat c d x a -> Nat c d y a -> Nat c d (BinaryCoproduct (Nat c d) x y) a Source # (+++) :: Nat c d a1 b1 -> Nat c d a2 b2 -> Nat c d (BinaryCoproduct (Nat c d) a1 a2) (BinaryCoproduct (Nat c d) b1 b2) Source #
(HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :>>: c2) Source #
Instance details Defined in Data.Category.Limit Associated Types type BinaryCoproduct (c1 :>>: c2) x y :: Type Source # Methods inj1 :: Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) x (BinaryCoproduct (c1 :>>: c2) x y) Source # inj2 :: Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) y (BinaryCoproduct (c1 :>>: c2) x y) Source # (\|\|\|) :: (c1 :>>: c2) x a -> (c1 :>>: c2) y a -> (c1 :>>: c2) (BinaryCoproduct (c1 :>>: c2) x y) a Source # (+++) :: (c1 :>>: c2) a1 b1 -> (c1 :>>: c2) a2 b2 -> (c1 :>>: c2) (BinaryCoproduct (c1 :>>: c2) a1 a2) (BinaryCoproduct (c1 :>>: c2) b1 b2) Source #

data CoproductFunctor (k :: * -> * -> *) Source #

Constructors

CoproductFunctor

Instances

HasBinaryCoproducts k => Functor (CoproductFunctor k) Source #	Binary coproduct as a bifunctor.
Instance details Defined in Data.Category.Limit Associated Types type Dom (CoproductFunctor k) :: Type -> Type -> Type Source # type Cod (CoproductFunctor k) :: Type -> Type -> Type Source # type (CoproductFunctor k) :% a :: Type Source # Methods (%) :: CoproductFunctor k -> Dom (CoproductFunctor k) a b -> Cod (CoproductFunctor k) (CoproductFunctor k :% a) (CoproductFunctor k :% b) Source #
(HasInitialObject k, HasBinaryCoproducts k) => SymmetricTensorProduct (CoproductFunctor k) Source #
Instance details Defined in Data.Category.Monoidal Methods swap :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> Obj k0 b -> k0 (CoproductFunctor k :% (a, b)) (CoproductFunctor k :% (b, a)) Source #
(HasInitialObject k, HasBinaryCoproducts k) => TensorProduct (CoproductFunctor k) Source #	If a category has all coproducts, then the coproduct functor makes it a monoidal category, with the initial object as unit.
Instance details Defined in Data.Category.Monoidal Associated Types type Unit (CoproductFunctor k) :: Type Source # Methods unitObject :: CoproductFunctor k -> Obj (Cod (CoproductFunctor k)) (Unit (CoproductFunctor k)) Source # leftUnitor :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> k0 (CoproductFunctor k :% (Unit (CoproductFunctor k), a)) a Source # leftUnitorInv :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> k0 a (CoproductFunctor k :% (Unit (CoproductFunctor k), a)) Source # rightUnitor :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> k0 (CoproductFunctor k :% (a, Unit (CoproductFunctor k))) a Source # rightUnitorInv :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> k0 a (CoproductFunctor k :% (a, Unit (CoproductFunctor k))) Source # associator :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> Obj k0 b -> Obj k0 c -> k0 (CoproductFunctor k :% (CoproductFunctor k :% (a, b), c)) (CoproductFunctor k :% (a, CoproductFunctor k :% (b, c))) Source # associatorInv :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> Obj k0 b -> Obj k0 c -> k0 (CoproductFunctor k :% (a, CoproductFunctor k :% (b, c))) (CoproductFunctor k :% (CoproductFunctor k :% (a, b), c)) Source #
type Dom (CoproductFunctor k) Source #
Instance details Defined in Data.Category.Limit type Dom (CoproductFunctor k) = k :**: k
type Cod (CoproductFunctor k) Source #
Instance details Defined in Data.Category.Limit type Cod (CoproductFunctor k) = k
type Unit (CoproductFunctor k) Source #
Instance details Defined in Data.Category.Monoidal type Unit (CoproductFunctor k) = InitialObject k
type (CoproductFunctor k) :% (a, b) Source #
Instance details Defined in Data.Category.Limit type (CoproductFunctor k) :% (a, b) = BinaryCoproduct k a b

data p :+: q where Source #

Constructors

(:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q

Instances

(Category (Dom p), Category (Cod p)) => Functor (p :+: q) Source #	The coproduct of two functors, passing the same object to both functors and taking the coproduct of the results.
Instance details Defined in Data.Category.Limit Associated Types type Dom (p :+: q) :: Type -> Type -> Type Source # type Cod (p :+: q) :: Type -> Type -> Type Source # type (p :+: q) :% a :: Type Source # Methods (%) :: (p :+: q) -> Dom (p :+: q) a b -> Cod (p :+: q) ((p :+: q) :% a) ((p :+: q) :% b) Source #
type Dom (p :+: q) Source #
Instance details Defined in Data.Category.Limit type Dom (p :+: q) = Dom p
type Cod (p :+: q) Source #
Instance details Defined in Data.Category.Limit type Cod (p :+: q) = Cod p
type (p :+: q) :% a Source #
Instance details Defined in Data.Category.Limit type (p :+: q) :% a = BinaryCoproduct (Cod p) (p :% a) (q :% a)

coprodAdj :: HasBinaryCoproducts k => Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k) Source #

A specialisation of the colimit adjunction to coproducts.