Structures · Category theory
CategoryTheory.IsMonoidalRightDistrib
A monoidal category with binary coproducts is right distributive if the right tensor product functor preserves binary coproducts.
- Shape
- One type argument · adds preservesBinaryCoproducts_tensorRight
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by12
- CategoryTheory.rightDistrib
- CategoryTheory.rightDistrib_hom
- CategoryTheory.coprod_inl_rightDistrib_hom
- CategoryTheory.coprod_inr_rightDistrib_hom
- CategoryTheory.whiskerRight_coprod_inl_rightDistrib_inv
- CategoryTheory.whiskerRight_coprod_inr_rightDistrib_inv
- CategoryTheory.whiskerRight_coprod_inl_rightDistrib_inv_assoc
- CategoryTheory.rightDistrib.congr_simp
- CategoryTheory.coprod_inl_rightDistrib_hom_assoc
- CategoryTheory.IsMonoidalRightDistrib.preservesBinaryCoproducts_tensorRight
- CategoryTheory.whiskerRight_coprod_inr_rightDistrib_inv_assoc
- CategoryTheory.coprod_inr_rightDistrib_hom_assoc
Ancestors0
No ancestors.