Structures · Category theory
CategoryTheory.IsMonoidalLeftDistrib
A monoidal category with binary coproducts is left distributive if the left tensor product functor preserves binary coproducts.
- Shape
- One type argument · adds preservesBinaryCoproducts_tensorLeft
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- CategoryTheory.Functor
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- CategoryTheory.leftDistrib
- CategoryTheory.leftDistrib_hom
- CategoryTheory.coprod_inr_leftDistrib_hom
- CategoryTheory.coprod_inl_leftDistrib_hom
- CategoryTheory.whiskerLeft_coprod_inl_leftDistrib_inv
- CategoryTheory.whiskerLeft_coprod_inr_leftDistrib_inv
- CategoryTheory.SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib
- CategoryTheory.leftDistrib.congr_simp
- CategoryTheory.coprod_inl_leftDistrib_hom_assoc
- CategoryTheory.whiskerLeft_coprod_inr_leftDistrib_inv_assoc
- CategoryTheory.IsMonoidalLeftDistrib.preservesBinaryCoproducts_tensorLeft
- CategoryTheory.coprod_inr_leftDistrib_hom_assoc
- CategoryTheory.IsCartesianDistributive.of_isMonoidalLeftDistrib
- CategoryTheory.whiskerLeft_coprod_inl_leftDistrib_inv_assoc
Ancestors0
No ancestors.