data-category-0.7.2: Category theory

LicenseBSD-style (see the file LICENSE)
Maintainersjoerd@w3future.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Category.Limit

Contents

Description

 
Synopsis

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

Instances
HasTerminalObject Cat Source #

Unit is the terminal category.

Instance details

Defined in Data.Category.Limit

Associated Types

type TerminalObject Cat :: Type 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 #

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 #

HasTerminalObject Cube Source # 
Instance details

Defined in Data.Category.Cube

Associated Types

type TerminalObject Cube :: Type 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 #

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 #

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 #

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 #

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 #

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 #

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 #

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 #

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 #

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 #

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 #

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

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 #

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

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