We define a category walking_pair, which is the index category for a binary (co)product diagram. A convenience method pair X Y constructs the functor from the walking pair, hitting the given objects.
We define prod X Y and coprod X Y as limits and colimits of such functors.
Typeclasses has_binary_products and has_binary_coproducts assert the existence of (co)limits shaped as walking pairs.
The type of objects for the diagram indexing a binary (co)product.
The braiding isomorphism which swaps a binary product.
The braiding isomorphism is symmetric.
The associator isomorphism for binary products.
The left unitor isomorphism for binary products with the terminal object.
The right unitor isomorphism for binary products with the terminal object.
The braiding isomorphism which swaps a binary coproduct.
The braiding isomorphism is symmetric.
The associator isomorphism for binary coproducts.
The left unitor isomorphism for binary coproducts with the initial object.
The right unitor isomorphism for binary coproducts with the initial object.