data-category-0.6.1: Category theory

Portabilitynon-portable
Stabilityexperimental
Maintainersjoerd@w3future.com
Safe HaskellSafe-Inferred

Data.Category.Coproduct

Description

 

Documentation

data I1 a Source

data I2 a Source

data :++: whereSource

Constructors

I1 :: c1 a1 b1 -> :++: c1 c2 (I1 a1) (I1 b1) 
I2 :: c2 a2 b2 -> :++: c1 c2 (I2 a2) (I2 b2) 

Instances

(Category c1, Category c2) => Category (:++: c1 c2)

The coproduct category of categories c1 and c2.

(HasColimits i k, HasColimits j k, HasBinaryCoproducts k) => HasColimits (:++: i j) k

If k has binary coproducts, we can take the colimit of 2 joined diagrams.

(HasLimits i k, HasLimits j k, HasBinaryProducts k) => HasLimits (:++: i j) k

If k has binary products, we can take the limit of 2 joined diagrams.

data Inj1 c1 c2 Source

Constructors

Inj1 

Instances

(Category c1, Category c2) => Functor (Inj1 c1 c2)

Inj1 is a functor which injects into the left category.

data Inj2 c1 c2 Source

Constructors

Inj2 

Instances

(Category c1, Category c2) => Functor (Inj2 c1 c2)

Inj2 is a functor which injects into the right category.

data f1 :+++: f2 Source

Constructors

f1 :+++: f2 

Instances

(Functor f1, Functor f2) => Functor (:+++: f1 f2)

f1 :+++: f2 is the coproduct of the functors f1 and f2.

data CodiagCoprod k Source

Constructors

CodiagCoprod 

Instances

Category k => Functor (CodiagCoprod k)

CodiagCoprod is the codiagonal functor for coproducts.

data Cotuple1 c1 c2 a Source

Constructors

Cotuple1 (Obj c1 a) 

Instances

(Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1)

Cotuple1 projects out to the left category, replacing a value from the right category with a fixed object.

data Cotuple2 c1 c2 a Source

Constructors

Cotuple2 (Obj c2 a) 

Instances

(Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2)

Cotuple2 projects out to the right category, replacing a value from the left category with a fixed object.

data :>>: whereSource

Constructors

I1A :: c1 a1 b1 -> :>>: c1 c2 (I1 a1) (I1 b1) 
I12 :: Obj c1 a -> Obj c2 b -> :>>: c1 c2 (I1 a) (I2 b) 
I2A :: c2 a2 b2 -> :>>: c1 c2 (I2 a2) (I2 b2) 

Instances

(Category c1, Category c2) => Category (:>>: c1 c2)

The directed coproduct category of categories c1 and c2.

(HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (:>>: c1 c2) 
(HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (:>>: c1 c2) 
(HasInitialObject c1, Category c2) => HasInitialObject (:>>: c1 c2)

The initial object of the direct coproduct of categories is the initial object of the initial category.

(Category c1, HasTerminalObject c2) => HasTerminalObject (:>>: c1 c2)

The terminal object of the direct coproduct of categories is the terminal object of the terminal category.

(HasTerminalObject (:>>: i j), Category k) => HasColimits (:>>: i j) k

The colimit of any diagram with a terminal object, has the limit at the terminal object.

(HasInitialObject (:>>: i j), Category k) => HasLimits (:>>: i j) k

The limit of any diagram with an initial object, has the limit at the initial object.

data NatAsFunctor f g Source

Constructors

NatAsFunctor (Nat (Dom f) (Cod f) f g) 

Instances

(Functor f, Functor g, ~ (* -> * -> *) (Dom f) (Dom g), ~ (* -> * -> *) (Cod f) (Cod g)) => Functor (NatAsFunctor f g)

A natural transformation Nat c d is isomorphic to a functor from c :**: 2 to d.