data-category-0.8.1: Category theory

Data.Category.Limit

Description

Synopsis

# Preliminairies

## Diagonal Functor

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

Constructors

 Diag :: Diag j k

#### Instances

Instances details
 (Category j, Category k) => Functor (Diag j k) Source # The diagonal functor from (index-) category J to k. Instance detailsDefined in Data.Category.Limit Associated Typestype Dom (Diag j k) :: Type -> Type -> Type Source #type Cod (Diag j k) :: Type -> Type -> Type Source #type (Diag j k) :% a 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 detailsDefined in Data.Category.Limit type Dom (Diag j k) = k type Cod (Diag j k) Source # Instance detailsDefined in Data.Category.Limit type Cod (Diag j k) = Nat j k type (Diag j k) :% a Source # Instance detailsDefined 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 j k f n = Nat j k (Const j k n) f Source #

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

type Cocone j k f n = Nat j k f (Const j k n) Source #

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

coneVertex :: Cone j k f n -> Obj k n Source #

The vertex (or apex) of a cone.

coconeVertex :: Cocone j k f n -> Obj k 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

Instances details
 type LimitFam Unit k f Source # Instance detailsDefined in Data.Category.Limit type LimitFam Unit k f = f :% () type LimitFam Void k f Source # Instance detailsDefined in Data.Category.Limit type LimitFam Void k f = TerminalObject k type LimitFam Boolean k f Source # Instance detailsDefined in Data.Category.Boolean type LimitFam Boolean k f = f :% Fls type LimitFam (i :>>: j) k f Source # Instance detailsDefined in Data.Category.Limit type LimitFam (i :>>: j) k f = f :% InitialObject (i :>>: j) type LimitFam (i :++: j) k f Source # Instance detailsDefined 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 detailsDefined 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 j k f (LimitFam j k f) Source #

limit returns the limiting cone for a functor f.

limitFactorizer :: Cone j k f n -> k n (LimitFam j k 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

Instances details
 Source # The limit of a single object is that object. Instance detailsDefined in Data.Category.Limit Methodslimit :: Obj (Nat Unit k) f -> Cone Unit k f (LimitFam Unit k f) Source #limitFactorizer :: Cone Unit k f n -> k n (LimitFam Unit k f) Source # Source # A terminal object is the limit of the functor from 0 to k. Instance detailsDefined in Data.Category.Limit Methodslimit :: Obj (Nat Void k) f -> Cone Void k f (LimitFam Void k f) Source #limitFactorizer :: Cone Void k f n -> k n (LimitFam Void k f) Source # Source # The limit of a functor from the Boolean category is the source of the arrow it points to. Instance detailsDefined in Data.Category.Boolean Methodslimit :: Obj (Nat Boolean k) f -> Cone Boolean k f (LimitFam Boolean k f) Source #limitFactorizer :: Cone Boolean k f n -> k n (LimitFam Boolean k f) Source # (HasInitialObject (i :>>: j), Category i, Category 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 detailsDefined in Data.Category.Limit Methodslimit :: Obj (Nat (i :>>: j) k) f -> Cone (i :>>: j) k f (LimitFam (i :>>: j) k f) Source #limitFactorizer :: Cone (i :>>: j) k f n -> k n (LimitFam (i :>>: j) k 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 detailsDefined in Data.Category.Limit Methodslimit :: Obj (Nat (i :++: j) k) f -> Cone (i :++: j) k f (LimitFam (i :++: j) k f) Source #limitFactorizer :: Cone (i :++: j) k f n -> k n (LimitFam (i :++: j) k f) Source # HasLimits ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) Source # Instance detailsDefined in Data.Category.Limit Methodslimit :: Obj (Nat (->) (->)) f -> Cone (->) (->) f (LimitFam (->) (->) f) Source #limitFactorizer :: Cone (->) (->) f n -> n -> LimitFam (->) (->) f Source #

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

Constructors

 LimitFunctor

#### Instances

Instances details
 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 detailsDefined in Data.Category.Limit Associated Typestype Dom (LimitFunctor j k) :: Type -> Type -> Type Source #type Cod (LimitFunctor j k) :: Type -> Type -> Type Source #type (LimitFunctor j k) :% a 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 detailsDefined in Data.Category.Limit type Dom (LimitFunctor j k) = Nat j k type Cod (LimitFunctor j k) Source # Instance detailsDefined in Data.Category.Limit type Cod (LimitFunctor j k) = k type (LimitFunctor j k) :% f Source # Instance detailsDefined 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.

adjLimit :: Category k => Adjunction (Nat j k) k (Diag j k) r -> Obj (Nat j k) f -> Cone j k f (r :% f) Source #

adjLimitFactorizer :: Category k => Adjunction (Nat j k) k (Diag j k) r -> Cone j k f n -> k n (r :% f) Source #

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 :% LimitFam j c t) (LimitFam j d (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

Instances details
 type ColimitFam Unit k f Source # Instance detailsDefined in Data.Category.Limit type ColimitFam Unit k f = f :% () type ColimitFam Void k f Source # Instance detailsDefined in Data.Category.Limit type ColimitFam Void k f = InitialObject k type ColimitFam Boolean k f Source # Instance detailsDefined in Data.Category.Boolean type ColimitFam Boolean k f = f :% Tru type ColimitFam (i :>>: j) k f Source # Instance detailsDefined in Data.Category.Limit type ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j) type ColimitFam (i :++: j) k f Source # Instance detailsDefined 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 detailsDefined 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 j k f (ColimitFam j k f) Source #

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

colimitFactorizer :: Cocone j k f n -> k (ColimitFam j k 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

Instances details
 Source # The colimit of a single object is that object. Instance detailsDefined in Data.Category.Limit Methodscolimit :: Obj (Nat Unit k) f -> Cocone Unit k f (ColimitFam Unit k f) Source #colimitFactorizer :: Cocone Unit k f n -> k (ColimitFam Unit k f) n Source # Source # An initial object is the colimit of the functor from 0 to k. Instance detailsDefined in Data.Category.Limit Methodscolimit :: Obj (Nat Void k) f -> Cocone Void k f (ColimitFam Void k f) Source #colimitFactorizer :: Cocone Void k f n -> k (ColimitFam Void k f) n Source # Source # The colimit of a functor from the Boolean category is the target of the arrow it points to. Instance detailsDefined in Data.Category.Boolean Methodscolimit :: Obj (Nat Boolean k) f -> Cocone Boolean k f (ColimitFam Boolean k f) Source #colimitFactorizer :: Cocone Boolean k f n -> k (ColimitFam Boolean k f) n Source # (HasTerminalObject (i :>>: j), Category i, Category 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 detailsDefined in Data.Category.Limit Methodscolimit :: Obj (Nat (i :>>: j) k) f -> Cocone (i :>>: j) k f (ColimitFam (i :>>: j) k f) Source #colimitFactorizer :: Cocone (i :>>: j) k f n -> k (ColimitFam (i :>>: j) k 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 detailsDefined in Data.Category.Limit Methodscolimit :: Obj (Nat (i :++: j) k) f -> Cocone (i :++: j) k f (ColimitFam (i :++: j) k f) Source #colimitFactorizer :: Cocone (i :++: j) k f n -> k (ColimitFam (i :++: j) k f) n Source # HasColimits ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) Source # Instance detailsDefined in Data.Category.Limit Methodscolimit :: Obj (Nat (->) (->)) f -> Cocone (->) (->) f (ColimitFam (->) (->) f) Source #colimitFactorizer :: Cocone (->) (->) f n -> ColimitFam (->) (->) f -> n Source #

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

Constructors

 ColimitFunctor

#### Instances

Instances details
 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 detailsDefined in Data.Category.Limit Associated Typestype Dom (ColimitFunctor j k) :: Type -> Type -> Type Source #type Cod (ColimitFunctor j k) :: Type -> Type -> Type Source #type (ColimitFunctor j k) :% a 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 detailsDefined in Data.Category.Limit type Dom (ColimitFunctor j k) = Nat j k type Cod (ColimitFunctor j k) Source # Instance detailsDefined in Data.Category.Limit type Cod (ColimitFunctor j k) = k type (ColimitFunctor j k) :% f Source # Instance detailsDefined 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.

adjColimit :: Category k => Adjunction k (Nat j k) l (Diag j k) -> Obj (Nat j k) f -> Cocone j k f (l :% f) Source #

adjColimitFactorizer :: Category k => Adjunction k (Nat j k) l (Diag j k) -> Cocone j k f n -> k (l :% f) n Source #

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 (ColimitFam j c (f :.: t)) (f :% ColimitFam j d t) Source #

## Limits of type Void

class Category k => HasTerminalObject k where Source #

Associated Types

type TerminalObject k :: Kind k Source #

Methods

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

#### Instances

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

class Category k => HasInitialObject k where Source #

Associated Types

type InitialObject k :: Kind k Source #

Methods

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

#### Instances

Instances details
 HasTerminalObject k2 => HasInitialObject (Op k2 :: k1 -> k1 -> Type) Source # Terminal objects are the dual of initial objects. Instance detailsDefined in Data.Category.Limit Associated Typestype InitialObject (Op k2) :: Kind k Source # MethodsinitialObject :: Obj (Op k2) (InitialObject (Op k2)) Source #initialize :: forall (a :: k). Obj (Op k2) a -> Op k2 (InitialObject (Op k2)) a Source # Source # The category of one object has that object as initial object. Instance detailsDefined in Data.Category.Limit Associated Typestype InitialObject Unit :: Kind k Source # Methodsinitialize :: forall (a :: k). Obj Unit a -> Unit (InitialObject Unit) a Source # Source # The ordinal 0 is the initial object of the simplex category. Instance detailsDefined in Data.Category.Simplex Associated Types Methodsinitialize :: forall (a :: k). Obj Simplex a -> Simplex (InitialObject Simplex) a Source # Source # False is the initial object in the Boolean category. Instance detailsDefined in Data.Category.Boolean Associated Types Methodsinitialize :: forall (a :: k). Obj Boolean a -> Boolean (InitialObject Boolean) a Source # HasInitialObject (f (Fix f)) => HasInitialObject (Fix f :: Type -> Type -> Type) Source # Fix f inherits its (co)limits from f (Fix f). Instance detailsDefined in Data.Category.Fix Associated Typestype InitialObject (Fix f) :: Kind k Source # MethodsinitialObject :: Obj (Fix f) (InitialObject (Fix f)) Source #initialize :: forall (a :: k). 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 detailsDefined in Data.Category.Limit Associated Typestype InitialObject (->) :: Kind k Source # MethodsinitialObject :: Obj (->) (InitialObject (->)) Source #initialize :: forall (a :: k). Obj (->) a -> InitialObject (->) -> a Source # (HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2 :: Type -> Type -> Type) Source # The initial object of the product of 2 categories is the product of their initial objects. Instance detailsDefined in Data.Category.Limit Associated Typestype InitialObject (c1 :**: c2) :: Kind k Source # MethodsinitialObject :: Obj (c1 :**: c2) (InitialObject (c1 :**: c2)) Source #initialize :: forall (a :: k). Obj (c1 :**: c2) a -> (c1 :**: c2) (InitialObject (c1 :**: c2)) a Source # (Category c, HasInitialObject d) => HasInitialObject (Nat c d :: Type -> Type -> Type) Source # The constant functor to the initial object is itself the initial object in its functor category. Instance detailsDefined in Data.Category.Limit Associated Typestype InitialObject (Nat c d) :: Kind k Source # MethodsinitialObject :: Obj (Nat c d) (InitialObject (Nat c d)) Source #initialize :: forall (a :: k). Obj (Nat c d) a -> Nat c d (InitialObject (Nat c d)) a Source # (HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2 :: Type -> Type -> Type) Source # The initial object of the direct coproduct of categories is the initial object of the initial category. Instance detailsDefined in Data.Category.Limit Associated Typestype InitialObject (c1 :>>: c2) :: Kind k Source # MethodsinitialObject :: Obj (c1 :>>: c2) (InitialObject (c1 :>>: c2)) Source #initialize :: forall (a :: k). 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)=. Instance detailsDefined in Data.Category.Dialg Associated Typestype InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) :: Kind k Source # MethodsinitialObject :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) Source #initialize :: forall (a :: k). Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a -> Dialg (Tuple1 (->) (->) ()) (DiagProd (->)) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) a Source # Source # The empty category is the initial object in Cat. Instance detailsDefined in Data.Category.Limit Associated Typestype InitialObject Cat :: Kind k Source # Methodsinitialize :: forall (a :: k). Obj Cat a -> Cat (InitialObject Cat) a Source #

## Limits of type Pair

class Category k => HasBinaryProducts k where Source #

Minimal complete definition

Associated Types

type BinaryProduct k (x :: Kind k) (y :: Kind k) :: Kind k 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

Instances details
 HasBinaryCoproducts k2 => HasBinaryProducts (Op k2 :: k1 -> k1 -> Type) Source # Binary products are the dual of binary coproducts. Instance detailsDefined in Data.Category.Limit Associated Typestype BinaryProduct (Op k2) x y :: Kind k Source # Methodsproj1 :: forall (x :: k) (y :: k). Obj (Op k2) x -> Obj (Op k2) y -> Op k2 (BinaryProduct (Op k2) x y) x Source #proj2 :: forall (x :: k) (y :: k). Obj (Op k2) x -> Obj (Op k2) y -> Op k2 (BinaryProduct (Op k2) x y) y Source #(&&&) :: forall (a :: k) (x :: k) (y :: k). Op k2 a x -> Op k2 a y -> Op k2 a (BinaryProduct (Op k2) x y) Source #(***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Op k2 a1 b1 -> Op k2 a2 b2 -> Op k2 (BinaryProduct (Op k2) a1 a2) (BinaryProduct (Op k2) b1 b2) Source # Source # In the category of one object that object is its own product. Instance detailsDefined in Data.Category.Limit Associated Typestype BinaryProduct Unit x y :: Kind k Source # Methodsproj1 :: forall (x :: k) (y :: k). Obj Unit x -> Obj Unit y -> Unit (BinaryProduct Unit x y) x Source #proj2 :: forall (x :: k) (y :: k). Obj Unit x -> Obj Unit y -> Unit (BinaryProduct Unit x y) y Source #(&&&) :: forall (a :: k) (x :: k) (y :: k). Unit a x -> Unit a y -> Unit a (BinaryProduct Unit x y) Source #(***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Unit a1 b1 -> Unit a2 b2 -> Unit (BinaryProduct Unit a1 a2) (BinaryProduct Unit b1 b2) Source # Source # Conjunction is the binary product in the Boolean category. Instance detailsDefined in Data.Category.Boolean Associated Typestype BinaryProduct Boolean x y :: Kind k Source # Methodsproj1 :: forall (x :: k) (y :: k). Obj Boolean x -> Obj Boolean y -> Boolean (BinaryProduct Boolean x y) x Source #proj2 :: forall (x :: k) (y :: k). Obj Boolean x -> Obj Boolean y -> Boolean (BinaryProduct Boolean x y) y Source #(&&&) :: forall (a :: k) (x :: k) (y :: k). Boolean a x -> Boolean a y -> Boolean a (BinaryProduct Boolean x y) Source #(***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Boolean a1 b1 -> Boolean a2 b2 -> Boolean (BinaryProduct Boolean a1 a2) (BinaryProduct Boolean b1 b2) Source # HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f :: Type -> Type -> Type) Source # Fix f inherits its (co)limits from f (Fix f). Instance detailsDefined in Data.Category.Fix Associated Typestype BinaryProduct (Fix f) x y :: Kind k Source # Methodsproj1 :: forall (x :: k) (y :: k). Obj (Fix f) x -> Obj (Fix f) y -> Fix f (BinaryProduct (Fix f) x y) x Source #proj2 :: forall (x :: k) (y :: k). Obj (Fix f) x -> Obj (Fix f) y -> Fix f (BinaryProduct (Fix f) x y) y Source #(&&&) :: forall (a :: k) (x :: k) (y :: k). Fix f a x -> Fix f a y -> Fix f a (BinaryProduct (Fix f) x y) Source #(***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). 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 detailsDefined in Data.Category.Limit Associated Typestype BinaryProduct (->) x y :: Kind k Source # Methodsproj1 :: forall (x :: k) (y :: k). Obj (->) x -> Obj (->) y -> BinaryProduct (->) x y -> x Source #proj2 :: forall (x :: k) (y :: k). Obj (->) x -> Obj (->) y -> BinaryProduct (->) x y -> y Source #(&&&) :: forall (a :: k) (x :: k) (y :: k). (a -> x) -> (a -> y) -> a -> BinaryProduct (->) x y Source #(***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). (a1 -> b1) -> (a2 -> b2) -> BinaryProduct (->) a1 a2 -> BinaryProduct (->) b1 b2 Source # (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2 :: Type -> Type -> Type) Source # The binary product of the product of 2 categories is the product of their binary products. Instance detailsDefined in Data.Category.Limit Associated Typestype BinaryProduct (c1 :**: c2) x y :: Kind k Source # Methodsproj1 :: forall (x :: k) (y :: k). Obj (c1 :**: c2) x -> Obj (c1 :**: c2) y -> (c1 :**: c2) (BinaryProduct (c1 :**: c2) x y) x Source #proj2 :: forall (x :: k) (y :: k). Obj (c1 :**: c2) x -> Obj (c1 :**: c2) y -> (c1 :**: c2) (BinaryProduct (c1 :**: c2) x y) y Source #(&&&) :: forall (a :: k) (x :: k) (y :: k). (c1 :**: c2) a x -> (c1 :**: c2) a y -> (c1 :**: c2) a (BinaryProduct (c1 :**: c2) x y) Source #(***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). (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 :: Type -> Type -> Type) Source # The functor product :*: is the binary product in functor categories. Instance detailsDefined in Data.Category.Limit Associated Typestype BinaryProduct (Nat c d) x y :: Kind k Source # Methodsproj1 :: forall (x :: k) (y :: k). Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d (BinaryProduct (Nat c d) x y) x Source #proj2 :: forall (x :: k) (y :: k). Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d (BinaryProduct (Nat c d) x y) y Source #(&&&) :: forall (a :: k) (x :: k) (y :: k). Nat c d a x -> Nat c d a y -> Nat c d a (BinaryProduct (Nat c d) x y) Source #(***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). 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 :: Type -> Type -> Type) Source # Instance detailsDefined in Data.Category.Limit Associated Typestype BinaryProduct (c1 :>>: c2) x y :: Kind k Source # Methodsproj1 :: forall (x :: k) (y :: k). Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) (BinaryProduct (c1 :>>: c2) x y) x Source #proj2 :: forall (x :: k) (y :: k). Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) (BinaryProduct (c1 :>>: c2) x y) y Source #(&&&) :: forall (a :: k) (x :: k) (y :: k). (c1 :>>: c2) a x -> (c1 :>>: c2) a y -> (c1 :>>: c2) a (BinaryProduct (c1 :>>: c2) x y) Source #(***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). (c1 :>>: c2) a1 b1 -> (c1 :>>: c2) a2 b2 -> (c1 :>>: c2) (BinaryProduct (c1 :>>: c2) a1 a2) (BinaryProduct (c1 :>>: c2) b1 b2) Source # Source # The product of categories :**: is the binary product in Cat. Instance detailsDefined in Data.Category.Limit Associated Typestype BinaryProduct Cat x y :: Kind k Source # Methodsproj1 :: forall (x :: k) (y :: k). Obj Cat x -> Obj Cat y -> Cat (BinaryProduct Cat x y) x Source #proj2 :: forall (x :: k) (y :: k). Obj Cat x -> Obj Cat y -> Cat (BinaryProduct Cat x y) y Source #(&&&) :: forall (a :: k) (x :: k) (y :: k). Cat a x -> Cat a y -> Cat a (BinaryProduct Cat x y) Source #(***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Cat a1 b1 -> Cat a2 b2 -> Cat (BinaryProduct Cat a1 a2) (BinaryProduct Cat b1 b2) Source #

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

Constructors

 ProductFunctor

#### Instances

Instances details
 Source # Binary product as a bifunctor. Instance detailsDefined in Data.Category.Limit Associated Typestype Dom (ProductFunctor k) :: Type -> Type -> Type Source #type Cod (ProductFunctor k) :: Type -> Type -> Type Source #type (ProductFunctor k) :% a Source # Methods(%) :: ProductFunctor k -> Dom (ProductFunctor k) a b -> Cod (ProductFunctor k) (ProductFunctor k :% a) (ProductFunctor k :% b) Source # Source # Instance detailsDefined in Data.Category.Monoidal Methodsswap :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> Obj k0 b -> k0 (ProductFunctor k :% (a, b)) (ProductFunctor k :% (b, a)) Source # Source # If a category has all products, then the product functor makes it a monoidal category, with the terminal object as unit. Instance detailsDefined in Data.Category.Monoidal Associated Typestype Unit (ProductFunctor k) Source # MethodsleftUnitor :: 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 detailsDefined in Data.Category.Limit type Dom (ProductFunctor k) = k :**: k type Cod (ProductFunctor k) Source # Instance detailsDefined in Data.Category.Limit type Cod (ProductFunctor k) = k type Unit (ProductFunctor k) Source # Instance detailsDefined in Data.Category.Monoidal type Unit (ProductFunctor k) = TerminalObject k type (ProductFunctor k) :% (a, b) Source # Instance detailsDefined 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

Instances details
 (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 detailsDefined in Data.Category.Limit Associated Typestype Dom (p :*: q) :: Type -> Type -> Type Source #type Cod (p :*: q) :: Type -> Type -> Type Source #type (p :*: q) :% a 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 detailsDefined in Data.Category.Limit type Dom (p :*: q) = Dom p type Cod (p :*: q) Source # Instance detailsDefined in Data.Category.Limit type Cod (p :*: q) = Cod p type (p :*: q) :% a Source # Instance detailsDefined 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

Associated Types

type BinaryCoproduct k (x :: Kind k) (y :: Kind k) :: Kind k 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

Instances details
 HasBinaryProducts k2 => HasBinaryCoproducts (Op k2 :: k1 -> k1 -> Type) Source # Binary products are the dual of binary coproducts. Instance detailsDefined in Data.Category.Limit Associated Typestype BinaryCoproduct (Op k2) x y :: Kind k Source # Methodsinj1 :: forall (x :: k) (y :: k). Obj (Op k2) x -> Obj (Op k2) y -> Op k2 x (BinaryCoproduct (Op k2) x y) Source #inj2 :: forall (x :: k) (y :: k). Obj (Op k2) x -> Obj (Op k2) y -> Op k2 y (BinaryCoproduct (Op k2) x y) Source #(|||) :: forall (x :: k) (a :: k) (y :: k). Op k2 x a -> Op k2 y a -> Op k2 (BinaryCoproduct (Op k2) x y) a Source #(+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Op k2 a1 b1 -> Op k2 a2 b2 -> Op k2 (BinaryCoproduct (Op k2) a1 a2) (BinaryCoproduct (Op k2) b1 b2) Source # Source # In the category of one object that object is its own coproduct. Instance detailsDefined in Data.Category.Limit Associated Typestype BinaryCoproduct Unit x y :: Kind k Source # Methodsinj1 :: forall (x :: k) (y :: k). Obj Unit x -> Obj Unit y -> Unit x (BinaryCoproduct Unit x y) Source #inj2 :: forall (x :: k) (y :: k). Obj Unit x -> Obj Unit y -> Unit y (BinaryCoproduct Unit x y) Source #(|||) :: forall (x :: k) (a :: k) (y :: k). Unit x a -> Unit y a -> Unit (BinaryCoproduct Unit x y) a Source #(+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Unit a1 b1 -> Unit a2 b2 -> Unit (BinaryCoproduct Unit a1 a2) (BinaryCoproduct Unit b1 b2) Source # Source # Disjunction is the binary coproduct in the Boolean category. Instance detailsDefined in Data.Category.Boolean Associated Typestype BinaryCoproduct Boolean x y :: Kind k Source # Methodsinj1 :: forall (x :: k) (y :: k). Obj Boolean x -> Obj Boolean y -> Boolean x (BinaryCoproduct Boolean x y) Source #inj2 :: forall (x :: k) (y :: k). Obj Boolean x -> Obj Boolean y -> Boolean y (BinaryCoproduct Boolean x y) Source #(|||) :: forall (x :: k) (a :: k) (y :: k). Boolean x a -> Boolean y a -> Boolean (BinaryCoproduct Boolean x y) a Source #(+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Boolean a1 b1 -> Boolean a2 b2 -> Boolean (BinaryCoproduct Boolean a1 a2) (BinaryCoproduct Boolean b1 b2) Source # HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f :: Type -> Type -> Type) Source # Fix f inherits its (co)limits from f (Fix f). Instance detailsDefined in Data.Category.Fix Associated Typestype BinaryCoproduct (Fix f) x y :: Kind k Source # Methodsinj1 :: forall (x :: k) (y :: k). Obj (Fix f) x -> Obj (Fix f) y -> Fix f x (BinaryCoproduct (Fix f) x y) Source #inj2 :: forall (x :: k) (y :: k). Obj (Fix f) x -> Obj (Fix f) y -> Fix f y (BinaryCoproduct (Fix f) x y) Source #(|||) :: forall (x :: k) (a :: k) (y :: k). Fix f x a -> Fix f y a -> Fix f (BinaryCoproduct (Fix f) x y) a Source #(+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). 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 :: Type -> Type -> Type) Source # The binary coproduct of the product of 2 categories is the product of their binary coproducts. Instance detailsDefined in Data.Category.Limit Associated Typestype BinaryCoproduct (c1 :**: c2) x y :: Kind k Source # Methodsinj1 :: forall (x :: k) (y :: k). Obj (c1 :**: c2) x -> Obj (c1 :**: c2) y -> (c1 :**: c2) x (BinaryCoproduct (c1 :**: c2) x y) Source #inj2 :: forall (x :: k) (y :: k). Obj (c1 :**: c2) x -> Obj (c1 :**: c2) y -> (c1 :**: c2) y (BinaryCoproduct (c1 :**: c2) x y) Source #(|||) :: forall (x :: k) (a :: k) (y :: k). (c1 :**: c2) x a -> (c1 :**: c2) y a -> (c1 :**: c2) (BinaryCoproduct (c1 :**: c2) x y) a Source #(+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). (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 :: Type -> Type -> Type) Source # The functor coproduct :+: is the binary coproduct in functor categories. Instance detailsDefined in Data.Category.Limit Associated Typestype BinaryCoproduct (Nat c d) x y :: Kind k Source # Methodsinj1 :: forall (x :: k) (y :: k). Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d x (BinaryCoproduct (Nat c d) x y) Source #inj2 :: forall (x :: k) (y :: k). Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d y (BinaryCoproduct (Nat c d) x y) Source #(|||) :: forall (x :: k) (a :: k) (y :: k). Nat c d x a -> Nat c d y a -> Nat c d (BinaryCoproduct (Nat c d) x y) a Source #(+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). 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 :: Type -> Type -> Type) Source # Instance detailsDefined in Data.Category.Limit Associated Typestype BinaryCoproduct (c1 :>>: c2) x y :: Kind k Source # Methodsinj1 :: forall (x :: k) (y :: k). Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) x (BinaryCoproduct (c1 :>>: c2) x y) Source #inj2 :: forall (x :: k) (y :: k). Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) y (BinaryCoproduct (c1 :>>: c2) x y) Source #(|||) :: forall (x :: k) (a :: k) (y :: k). (c1 :>>: c2) x a -> (c1 :>>: c2) y a -> (c1 :>>: c2) (BinaryCoproduct (c1 :>>: c2) x y) a Source #(+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). (c1 :>>: c2) a1 b1 -> (c1 :>>: c2) a2 b2 -> (c1 :>>: c2) (BinaryCoproduct (c1 :>>: c2) a1 a2) (BinaryCoproduct (c1 :>>: c2) b1 b2) Source # Source # The coproduct of categories :++: is the binary coproduct in Cat. Instance detailsDefined in Data.Category.Limit Associated Typestype BinaryCoproduct Cat x y :: Kind k Source # Methodsinj1 :: forall (x :: k) (y :: k). Obj Cat x -> Obj Cat y -> Cat x (BinaryCoproduct Cat x y) Source #inj2 :: forall (x :: k) (y :: k). Obj Cat x -> Obj Cat y -> Cat y (BinaryCoproduct Cat x y) Source #(|||) :: forall (x :: k) (a :: k) (y :: k). Cat x a -> Cat y a -> Cat (BinaryCoproduct Cat x y) a Source #(+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Cat a1 b1 -> Cat a2 b2 -> Cat (BinaryCoproduct Cat a1 a2) (BinaryCoproduct Cat b1 b2) Source #

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

Constructors

 CoproductFunctor

#### Instances

Instances details
 Source # Binary coproduct as a bifunctor. Instance detailsDefined in Data.Category.Limit Associated Typestype Dom (CoproductFunctor k) :: Type -> Type -> Type Source #type Cod (CoproductFunctor k) :: Type -> Type -> Type Source #type (CoproductFunctor k) :% a Source # Methods(%) :: CoproductFunctor k -> Dom (CoproductFunctor k) a b -> Cod (CoproductFunctor k) (CoproductFunctor k :% a) (CoproductFunctor k :% b) Source # Source # Instance detailsDefined in Data.Category.Monoidal Methodsswap :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> Obj k0 b -> k0 (CoproductFunctor k :% (a, b)) (CoproductFunctor k :% (b, a)) Source # Source # If a category has all coproducts, then the coproduct functor makes it a monoidal category, with the initial object as unit. Instance detailsDefined in Data.Category.Monoidal Associated Typestype Unit (CoproductFunctor k) Source # MethodsleftUnitor :: 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 detailsDefined in Data.Category.Limit type Dom (CoproductFunctor k) = k :**: k type Cod (CoproductFunctor k) Source # Instance detailsDefined in Data.Category.Limit type Cod (CoproductFunctor k) = k type Unit (CoproductFunctor k) Source # Instance detailsDefined in Data.Category.Monoidal type Unit (CoproductFunctor k) = InitialObject k type (CoproductFunctor k) :% (a, b) Source # Instance detailsDefined 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

Instances details
 (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 detailsDefined in Data.Category.Limit Associated Typestype Dom (p :+: q) :: Type -> Type -> Type Source #type Cod (p :+: q) :: Type -> Type -> Type Source #type (p :+: q) :% a 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 detailsDefined in Data.Category.Limit type Dom (p :+: q) = Dom p type Cod (p :+: q) Source # Instance detailsDefined in Data.Category.Limit type Cod (p :+: q) = Cod p type (p :+: q) :% a Source # Instance detailsDefined 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.