Data.Category.Coproduct

Documentation

data I1 a

Instances

type (CodiagCoprod k) :% (I1 a)

type (CodiagCoprod k) :% (I1 a) = a

type ((:+++:) f1 f2) :% (I1 a)

type ((:+++:) f1 f2) :% (I1 a) = I1 ((:%) f1 a)

type (PrimRec z s) :% (I1 ())

type (PrimRec z s) :% (I1 ()) = (:%) z ()

type BinaryCoproduct ((:>>:) c1 c2) (I1 a) (I1 b)

type BinaryCoproduct ((:>>:) c1 c2) (I1 a) (I1 b) = I1 (BinaryCoproduct c1 a b)

type BinaryCoproduct ((:>>:) c1 c2) (I1 a) (I2 b)

type BinaryCoproduct ((:>>:) c1 c2) (I1 a) (I2 b) = I2 b

type BinaryCoproduct ((:>>:) c1 c2) (I2 a) (I1 b)

type BinaryCoproduct ((:>>:) c1 c2) (I2 a) (I1 b) = I2 a

type BinaryProduct ((:>>:) c1 c2) (I1 a) (I1 b)

type BinaryProduct ((:>>:) c1 c2) (I1 a) (I1 b) = I1 (BinaryProduct c1 a b)

type BinaryProduct ((:>>:) c1 c2) (I1 a) (I2 b)

type BinaryProduct ((:>>:) c1 c2) (I1 a) (I2 b) = I1 a

type BinaryProduct ((:>>:) c1 c2) (I2 a) (I1 b)

type BinaryProduct ((:>>:) c1 c2) (I2 a) (I1 b) = I1 b

type (NatAsFunctor f g) :% (a, I1 ())

type (NatAsFunctor f g) :% (a, I1 ()) = (:%) f a

type (Cotuple2 c1 c2 a2) :% (I1 a)

type (Cotuple2 c1 c2 a2) :% (I1 a) = a2

type (Cotuple1 c1 c2 a1) :% (I1 a)

type (Cotuple1 c1 c2 a1) :% (I1 a) = a

data I2 a

Instances

type (CodiagCoprod k) :% (I2 a)

type (CodiagCoprod k) :% (I2 a) = a

type ((:+++:) f1 f2) :% (I2 a)

type ((:+++:) f1 f2) :% (I2 a) = I2 ((:%) f2 a)

type (PrimRec z s) :% (I2 n)

type (PrimRec z s) :% (I2 n) = (:%) s ((:%) (PrimRec z s) n)

type BinaryCoproduct ((:>>:) c1 c2) (I1 a) (I2 b)

type BinaryCoproduct ((:>>:) c1 c2) (I1 a) (I2 b) = I2 b

type BinaryCoproduct ((:>>:) c1 c2) (I2 a) (I1 b)

type BinaryCoproduct ((:>>:) c1 c2) (I2 a) (I1 b) = I2 a

type BinaryCoproduct ((:>>:) c1 c2) (I2 a) (I2 b)

type BinaryCoproduct ((:>>:) c1 c2) (I2 a) (I2 b) = I2 (BinaryCoproduct c2 a b)

type BinaryProduct ((:>>:) c1 c2) (I1 a) (I2 b)

type BinaryProduct ((:>>:) c1 c2) (I1 a) (I2 b) = I1 a

type BinaryProduct ((:>>:) c1 c2) (I2 a) (I1 b)

type BinaryProduct ((:>>:) c1 c2) (I2 a) (I1 b) = I1 b

type BinaryProduct ((:>>:) c1 c2) (I2 a) (I2 b)

type BinaryProduct ((:>>:) c1 c2) (I2 a) (I2 b) = I2 (BinaryProduct c2 a b)

type (NatAsFunctor f g) :% (a, I2 ())

type (NatAsFunctor f g) :% (a, I2 ()) = (:%) g a

type (Cotuple2 c1 c2 a2) :% (I2 a)

type (Cotuple2 c1 c2 a2) :% (I2 a) = a

type (Cotuple1 c1 c2 a1) :% (I2 a)

type (Cotuple1 c1 c2 a1) :% (I2 a) = a1

data (:++:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where

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.

Methods

src :: (c1 :++: c2) a b -> Obj (c1 :++: c2) a

tgt :: (c1 :++: c2) a b -> Obj (c1 :++: c2) b

(.) :: (c1 :++: c2) b c -> (c1 :++: c2) a b -> (c1 :++: c2) a c

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

Methods

colimit :: Obj (Nat (i :++: j) k) f -> Cocone f (Colimit f)

colimitFactorizer :: Obj (Nat (i :++: j) k) f -> forall n. Cocone f n -> k (Colimit f) n

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

Methods

limit :: Obj (Nat (i :++: j) k) f -> Cone f (Limit f)

limitFactorizer :: Obj (Nat (i :++: j) k) f -> forall n. Cone f n -> k n (Limit f)

type ColimitFam ((:++:) i j) k f

type ColimitFam ((:++:) i j) k f = BinaryCoproduct k (ColimitFam i k ((:.:) f (Inj1 i j))) (ColimitFam j k ((:.:) f (Inj2 i j)))

type LimitFam ((:++:) i j) k f

type LimitFam ((:++:) i j) k f = BinaryProduct k (LimitFam i k ((:.:) f (Inj1 i j))) (LimitFam j k ((:.:) f (Inj2 i j)))

data Inj1 c1 c2

Constructors

Inj1

Instances

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

Inj1 is a functor which injects into the left category.

Associated Types

type Dom (Inj1 c1 c2) :: * -> * -> *

type Cod (Inj1 c1 c2) :: * -> * -> *

type (Inj1 c1 c2) :% a :: *

Methods

(%) :: Inj1 c1 c2 -> Dom (Inj1 c1 c2) a b -> Cod (Inj1 c1 c2) (Inj1 c1 c2 :% a) (Inj1 c1 c2 :% b)

type Dom (Inj1 c1 c2)

type Dom (Inj1 c1 c2) = c1

type Cod (Inj1 c1 c2)

type Cod (Inj1 c1 c2) = (:++:) c1 c2

type (Inj1 c1 c2) :% a

type (Inj1 c1 c2) :% a = I1 a

data Inj2 c1 c2

Constructors

Inj2

Instances

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

Inj2 is a functor which injects into the right category.

Associated Types

type Dom (Inj2 c1 c2) :: * -> * -> *

type Cod (Inj2 c1 c2) :: * -> * -> *

type (Inj2 c1 c2) :% a :: *

Methods

(%) :: Inj2 c1 c2 -> Dom (Inj2 c1 c2) a b -> Cod (Inj2 c1 c2) (Inj2 c1 c2 :% a) (Inj2 c1 c2 :% b)

type Dom (Inj2 c1 c2)

type Dom (Inj2 c1 c2) = c2

type Cod (Inj2 c1 c2)

type Cod (Inj2 c1 c2) = (:++:) c1 c2

type (Inj2 c1 c2) :% a

type (Inj2 c1 c2) :% a = I2 a

data f1 :+++: f2

Constructors

f1 :+++: f2

Instances

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

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

Associated Types

type Dom ((:+++:) f1 f2) :: * -> * -> *

type Cod ((:+++:) f1 f2) :: * -> * -> *

type ((:+++:) f1 f2) :% a :: *

Methods

(%) :: (f1 :+++: f2) -> Dom (f1 :+++: f2) a b -> Cod (f1 :+++: f2) ((f1 :+++: f2) :% a) ((f1 :+++: f2) :% b)

type Dom ((:+++:) f1 f2)

type Dom ((:+++:) f1 f2) = (:++:) (Dom f1) (Dom f2)

type Cod ((:+++:) f1 f2)

type Cod ((:+++:) f1 f2) = (:++:) (Cod f1) (Cod f2)

type ((:+++:) f1 f2) :% (I1 a)

type ((:+++:) f1 f2) :% (I1 a) = I1 ((:%) f1 a)

type ((:+++:) f1 f2) :% (I2 a)

type ((:+++:) f1 f2) :% (I2 a) = I2 ((:%) f2 a)

data CodiagCoprod k

Constructors

CodiagCoprod

Instances

Category k => Functor (CodiagCoprod k)

CodiagCoprod is the codiagonal functor for coproducts.

Associated Types

type Dom (CodiagCoprod k) :: * -> * -> *

type Cod (CodiagCoprod k) :: * -> * -> *

type (CodiagCoprod k) :% a :: *

Methods

(%) :: CodiagCoprod k -> Dom (CodiagCoprod k) a b -> Cod (CodiagCoprod k) (CodiagCoprod k :% a) (CodiagCoprod k :% b)

type Dom (CodiagCoprod k)

type Dom (CodiagCoprod k) = (:++:) k k

type Cod (CodiagCoprod k)

type Cod (CodiagCoprod k) = k

type (CodiagCoprod k) :% (I1 a)

type (CodiagCoprod k) :% (I1 a) = a

type (CodiagCoprod k) :% (I2 a)

type (CodiagCoprod k) :% (I2 a) = a

data Cotuple1 c1 c2 a

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.

Associated Types

type Dom (Cotuple1 c1 c2 a1) :: * -> * -> *

type Cod (Cotuple1 c1 c2 a1) :: * -> * -> *

type (Cotuple1 c1 c2 a1) :% a :: *

Methods

(%) :: Cotuple1 c1 c2 a1 -> Dom (Cotuple1 c1 c2 a1) a b -> Cod (Cotuple1 c1 c2 a1) (Cotuple1 c1 c2 a1 :% a) (Cotuple1 c1 c2 a1 :% b)

type Dom (Cotuple1 c1 c2 a1)

type Dom (Cotuple1 c1 c2 a1) = (:++:) c1 c2

type Cod (Cotuple1 c1 c2 a1)

type Cod (Cotuple1 c1 c2 a1) = c1

type (Cotuple1 c1 c2 a1) :% (I1 a)

type (Cotuple1 c1 c2 a1) :% (I1 a) = a

type (Cotuple1 c1 c2 a1) :% (I2 a)

type (Cotuple1 c1 c2 a1) :% (I2 a) = a1

data Cotuple2 c1 c2 a

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.

Associated Types

type Dom (Cotuple2 c1 c2 a2) :: * -> * -> *

type Cod (Cotuple2 c1 c2 a2) :: * -> * -> *

type (Cotuple2 c1 c2 a2) :% a :: *

Methods

(%) :: Cotuple2 c1 c2 a2 -> Dom (Cotuple2 c1 c2 a2) a b -> Cod (Cotuple2 c1 c2 a2) (Cotuple2 c1 c2 a2 :% a) (Cotuple2 c1 c2 a2 :% b)

type Dom (Cotuple2 c1 c2 a2)

type Dom (Cotuple2 c1 c2 a2) = (:++:) c1 c2

type Cod (Cotuple2 c1 c2 a2)

type Cod (Cotuple2 c1 c2 a2) = c2

type (Cotuple2 c1 c2 a2) :% (I1 a)

type (Cotuple2 c1 c2 a2) :% (I1 a) = a2

type (Cotuple2 c1 c2 a2) :% (I2 a)

type (Cotuple2 c1 c2 a2) :% (I2 a) = a

data (:>>:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where

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.

Methods

src :: (c1 :>>: c2) a b -> Obj (c1 :>>: c2) a

tgt :: (c1 :>>: c2) a b -> Obj (c1 :>>: c2) b

(.) :: (c1 :>>: c2) b c -> (c1 :>>: c2) a b -> (c1 :>>: c2) a c

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

Associated Types

type BinaryCoproduct ((:>>:) c1 c2 :: * -> * -> *) x y :: *

Methods

inj1 :: Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) x (BinaryCoproduct (c1 :>>: c2) x y)

inj2 :: Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) y (BinaryCoproduct (c1 :>>: c2) x y)

(|||) :: (c1 :>>: c2) x a -> (c1 :>>: c2) y a -> (c1 :>>: c2) (BinaryCoproduct (c1 :>>: c2) x y) a

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

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

Associated Types

type BinaryProduct ((:>>:) c1 c2 :: * -> * -> *) x y :: *

Methods

proj1 :: Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) (BinaryProduct (c1 :>>: c2) x y) x

proj2 :: Obj (c1 :>>: c2) x -> Obj (c1 :>>: c2) y -> (c1 :>>: c2) (BinaryProduct (c1 :>>: c2) x y) y

(&&&) :: (c1 :>>: c2) a x -> (c1 :>>: c2) a y -> (c1 :>>: c2) a (BinaryProduct (c1 :>>: c2) x y)

(***) :: (c1 :>>: c2) a1 b1 -> (c1 :>>: c2) a2 b2 -> (c1 :>>: c2) (BinaryProduct (c1 :>>: c2) a1 a2) (BinaryProduct (c1 :>>: c2) b1 b2)

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

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

Associated Types

type InitialObject ((:>>:) c1 c2 :: * -> * -> *) :: *

Methods

initialObject :: Obj (c1 :>>: c2) (InitialObject (c1 :>>: c2))

initialize :: Obj (c1 :>>: c2) a -> (c1 :>>: c2) (InitialObject (c1 :>>: c2)) a

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

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

Associated Types

type TerminalObject ((:>>:) c1 c2 :: * -> * -> *) :: *

Methods

terminalObject :: Obj (c1 :>>: c2) (TerminalObject (c1 :>>: c2))

terminate :: Obj (c1 :>>: c2) a -> (c1 :>>: c2) a (TerminalObject (c1 :>>: c2))

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

Methods

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

colimitFactorizer :: Obj (Nat (i :>>: j) k) f -> forall n. Cocone f n -> k (Colimit f) n

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

Methods

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

limitFactorizer :: Obj (Nat (i :>>: j) k) f -> forall n. Cone f n -> k n (Limit f)

type InitialObject ((:>>:) c1 c2)

type InitialObject ((:>>:) c1 c2) = I1 (InitialObject c1)

type TerminalObject ((:>>:) c1 c2)

type TerminalObject ((:>>:) c1 c2) = I2 (TerminalObject c2)

type ColimitFam ((:>>:) i j) k f

type ColimitFam ((:>>:) i j) k f = (:%) f (TerminalObject ((:>>:) i j))

type LimitFam ((:>>:) i j) k f

type LimitFam ((:>>:) i j) k f = (:%) f (InitialObject ((:>>:) i j))

type BinaryCoproduct ((:>>:) c1 c2) (I1 a) (I1 b)

type BinaryCoproduct ((:>>:) c1 c2) (I1 a) (I1 b) = I1 (BinaryCoproduct c1 a b)

type BinaryCoproduct ((:>>:) c1 c2) (I1 a) (I2 b)

type BinaryCoproduct ((:>>:) c1 c2) (I1 a) (I2 b) = I2 b

type BinaryCoproduct ((:>>:) c1 c2) (I2 a) (I1 b)

type BinaryCoproduct ((:>>:) c1 c2) (I2 a) (I1 b) = I2 a

type BinaryCoproduct ((:>>:) c1 c2) (I2 a) (I2 b)

type BinaryCoproduct ((:>>:) c1 c2) (I2 a) (I2 b) = I2 (BinaryCoproduct c2 a b)

type BinaryProduct ((:>>:) c1 c2) (I1 a) (I1 b)

type BinaryProduct ((:>>:) c1 c2) (I1 a) (I1 b) = I1 (BinaryProduct c1 a b)

type BinaryProduct ((:>>:) c1 c2) (I1 a) (I2 b)

type BinaryProduct ((:>>:) c1 c2) (I1 a) (I2 b) = I1 a

type BinaryProduct ((:>>:) c1 c2) (I2 a) (I1 b)

type BinaryProduct ((:>>:) c1 c2) (I2 a) (I1 b) = I1 b

type BinaryProduct ((:>>:) c1 c2) (I2 a) (I2 b)

type BinaryProduct ((:>>:) c1 c2) (I2 a) (I2 b) = I2 (BinaryProduct c2 a b)

data NatAsFunctor f g

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.

Associated Types

type Dom (NatAsFunctor f g) :: * -> * -> *

type Cod (NatAsFunctor f g) :: * -> * -> *

type (NatAsFunctor f g) :% a :: *

Methods

(%) :: NatAsFunctor f g -> Dom (NatAsFunctor f g) a b -> Cod (NatAsFunctor f g) (NatAsFunctor f g :% a) (NatAsFunctor f g :% b)

type Dom (NatAsFunctor f g)

type Dom (NatAsFunctor f g) = (:**:) (Dom f) ((:>>:) Unit Unit)

type Cod (NatAsFunctor f g)

type Cod (NatAsFunctor f g) = Cod f

type (NatAsFunctor f g) :% (a, I1 ())

type (NatAsFunctor f g) :% (a, I1 ()) = (:%) f a

type (NatAsFunctor f g) :% (a, I2 ())

type (NatAsFunctor f g) :% (a, I2 ()) = (:%) g a