data-category-0.5.1.0: Category theory

Portability non-portable experimental sjoerd@w3future.com Safe-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`.