Portability	non-portable
Stability	experimental
Maintainer	sjoerd@w3future.com

Data.Category.Pair

Description

Pair, the category with just 2 objects and their identity arrows. The limit and colimit of the functor from Pair to some category provide products and coproducts in that category.

Synopsis

Documentation

data Fst Source

One object of Pair

Constructors

Fst

Instances

Show Fst
CategoryO Pair Fst
Apply Pair Fst Fst
CategoryA Pair Fst Fst Fst
CategoryO ~> x => FunctorA (PairF ~> x y) Fst Fst

data Snd Source

The other object of Pair

Constructors

Snd

Instances

Show Snd
CategoryO Pair Snd
Apply Pair Snd Snd
CategoryA Pair Snd Snd Snd
CategoryO ~> y => FunctorA (PairF ~> x y) Snd Snd

data family Pair a b :: *Source

The arrows of Pair.

data PairF (~>) x y Source

The functor from Pair to (~>), a diagram of 2 objects in (~>).

Constructors

PairF

Instances

CategoryO ~> y => FunctorA (PairF ~> x y) Snd Snd
CategoryO ~> x => FunctorA (PairF ~> x y) Fst Fst

class (CategoryO ~> x, CategoryO ~> y) => PairLimit (~>) x y whereSource

The product of 2 objects is the limit of the functor from Pair to (~>).

Associated Types

type Product x y :: *Source

Methods

pairLimit :: Limit (PairF ~> x y) (Product x y)Source

proj1 :: Product x y ~> xSource

proj2 :: Product x y ~> ySource

Instances

PairLimit (->) x y
PairLimit Boolean Tru Tru
PairLimit Boolean Tru Fls
PairLimit Boolean Fls Tru
PairLimit Boolean Fls Fls
PairLimit Omega Z Z
(Product Z n ~ Z, PairLimit Omega Z n) => PairLimit Omega Z (S n)
(Product n Z ~ Z, PairLimit Omega n Z) => PairLimit Omega (S n) Z
PairLimit Omega a b => PairLimit Omega (S a) (S b)

class (CategoryO ~> x, CategoryO ~> y) => PairColimit (~>) x y whereSource

The coproduct of 2 objects is the colimit of the functor from Pair to (~>).

Associated Types

type Coproduct x y :: *Source

Methods

pairColimit :: Colimit (PairF ~> x y) (Coproduct x y)Source

inj1 :: x ~> Coproduct x ySource

inj2 :: y ~> Coproduct x ySource

Instances

PairColimit (->) x y
PairColimit Boolean Tru Tru
PairColimit Boolean Tru Fls
PairColimit Boolean Fls Tru
PairColimit Boolean Fls Fls
PairColimit Omega Z Z
(Coproduct Z n ~ n, PairColimit Omega Z n) => PairColimit Omega Z (S n)
(Coproduct n Z ~ n, PairColimit Omega n Z) => PairColimit Omega (S n) Z
PairColimit Omega a b => PairColimit Omega (S a) (S b)