Portability | non-portable |
---|---|
Stability | experimental |
Maintainer | sjoerd@w3future.com |
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.
Documentation
One object of Pair
The other object of Pair
The functor from Pair to (~>), a diagram of 2 objects in (~>).
class (CategoryO ~> x, CategoryO ~> y) => PairLimit (~>) x y whereSource
The product of 2 objects is the limit of the functor from Pair to (~>).
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 (~>).
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) |