Loogle!

Result

Found 167 declarations mentioning CategoryTheory.Limits.HasBinaryCoproducts.

• CategoryTheory.Limits.HasBinaryCoproducts 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop
• CategoryTheory.Limits.coprod.functor 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Functor C (CategoryTheory.Functor C C)
• CategoryTheory.Limits.hasBinaryCoproducts_of_hasColimit_pair 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [∀ {X Y : C}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pair X Y)] : CategoryTheory.Limits.HasBinaryCoproducts C
• CategoryTheory.Over.coprodObj 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} : CategoryTheory.Over A → CategoryTheory.Functor (CategoryTheory.Over A) (CategoryTheory.Over A)
• CategoryTheory.Limits.coprod.leftUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (P : C) : (⊥_ C) ⨿ P ≅ P
• CategoryTheory.Limits.coprod.rightUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (P : C) : P ⨿ ⊥_ C ≅ P
• CategoryTheory.Limits.coprod.functor_obj_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X Y : C) : (CategoryTheory.Limits.coprod.functor.obj X).obj Y = (X ⨿ Y)
• CategoryTheory.Limits.coprod.braiding 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P Q : C) : P ⨿ Q ≅ Q ⨿ P
• CategoryTheory.Over.coprod 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} : CategoryTheory.Functor (CategoryTheory.Over A) (CategoryTheory.Functor (CategoryTheory.Over A) (CategoryTheory.Over A))
• CategoryTheory.Limits.coprod.leftUnitor_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (P : C) : (CategoryTheory.Limits.coprod.leftUnitor P).inv = CategoryTheory.Limits.coprod.inr
• CategoryTheory.Limits.coprod.rightUnitor_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (P : C) : (CategoryTheory.Limits.coprod.rightUnitor P).inv = CategoryTheory.Limits.coprod.inl
• CategoryTheory.Over.coprod_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} (f : CategoryTheory.Over A) : CategoryTheory.Over.coprod.obj f = f.coprodObj
• CategoryTheory.Limits.coprod.leftUnitor_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (P : C) : (CategoryTheory.Limits.coprod.leftUnitor P).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.initial.to P) (CategoryTheory.CategoryStruct.id P)
• CategoryTheory.Limits.coprod.rightUnitor_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (P : C) : (CategoryTheory.Limits.coprod.rightUnitor P).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id P) (CategoryTheory.Limits.initial.to P)
• CategoryTheory.Limits.coprod.functorLeftComp 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X Y : C) : CategoryTheory.Limits.coprod.functor.obj (X ⨿ Y) ≅ (CategoryTheory.Limits.coprod.functor.obj Y).comp (CategoryTheory.Limits.coprod.functor.obj X)
• CategoryTheory.Over.coprodObj_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} (a✝ g : CategoryTheory.Over A) : a✝.coprodObj.obj g = CategoryTheory.Over.mk (CategoryTheory.Limits.coprod.desc a✝.hom g.hom)
• CategoryTheory.Limits.coprod.functor_obj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) : (CategoryTheory.Limits.coprod.functor.obj X).map g = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) g
• CategoryTheory.Limits.coprod.associator 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P Q R : C) : (P ⨿ Q) ⨿ R ≅ P ⨿ Q ⨿ R
• CategoryTheory.Limits.coprod.braiding_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P Q : C) : (CategoryTheory.Limits.coprod.braiding P Q).hom = CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl
• CategoryTheory.Limits.coprod.braiding_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P Q : C) : (CategoryTheory.Limits.coprod.braiding P Q).inv = CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl
• CategoryTheory.Limits.coprod.functor_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : C) : (CategoryTheory.Limits.coprod.functor.map f).app T = CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id T)
• CategoryTheory.Limits.coprod.symmetry 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P Q : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding P Q).hom (CategoryTheory.Limits.coprod.braiding Q P).hom = CategoryTheory.CategoryStruct.id (P ⨿ Q)
• CategoryTheory.Limits.coprod.leftUnitor_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id (⊥_ C)) f) (CategoryTheory.Limits.coprod.leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.leftUnitor X).hom f
• CategoryTheory.Limits.coprod.rightUnitor_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id (⊥_ C))) (CategoryTheory.Limits.coprod.rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.rightUnitor X).hom f
• CategoryTheory.Limits.coprod.symmetry' 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P Q : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) = CategoryTheory.CategoryStruct.id (P ⨿ Q)
• CategoryTheory.Limits.coprod.symmetry'_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P Q : C) {Z : C} (h : P ⨿ Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) h) = h
• CategoryTheory.Over.coprod_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} {X✝ Y✝ : CategoryTheory.Over A} (k : X✝ ⟶ Y✝) (g : CategoryTheory.Over A) : (CategoryTheory.Over.coprod.map k).app g = CategoryTheory.Over.homMk (CategoryTheory.Limits.coprod.map (CategoryTheory.Over.Hom.left k) (CategoryTheory.CategoryStruct.id g.left)) ⋯
• CategoryTheory.Over.coprodObj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} (a✝ : CategoryTheory.Over A) {X✝ Y✝ : CategoryTheory.Over A} (k : X✝ ⟶ Y✝) : a✝.coprodObj.map k = CategoryTheory.Over.homMk (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id a✝.left) (CategoryTheory.Over.Hom.left k)) ⋯
• CategoryTheory.Limits.coprod.associator_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P Q R : C) : (CategoryTheory.Limits.coprod.associator P Q R).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inr)
• CategoryTheory.Limits.coprod.associator_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P Q R : C) : (CategoryTheory.Limits.coprod.associator P Q R).inv = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inl) (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) CategoryTheory.Limits.coprod.inr)
• CategoryTheory.Limits.coprod.triangle 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.associator X (⊥_ C) Y).hom (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.coprod.leftUnitor Y).hom) = CategoryTheory.Limits.coprod.map (CategoryTheory.Limits.coprod.rightUnitor X).hom (CategoryTheory.CategoryStruct.id Y)
• CategoryTheory.Limits.coprod.associator_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.Limits.coprod.map f₁ f₂) f₃) (CategoryTheory.Limits.coprod.associator Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.associator X₁ X₂ X₃).hom (CategoryTheory.Limits.coprod.map f₁ (CategoryTheory.Limits.coprod.map f₂ f₃))
• CategoryTheory.Limits.coprod.pentagon 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (W X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.Limits.coprod.associator W X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.associator W (X ⨿ Y) Z).hom (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.Limits.coprod.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.associator (W ⨿ X) Y Z).hom (CategoryTheory.Limits.coprod.associator W X (Y ⨿ Z)).hom
• CategoryTheory.Limits.coprodComparisonNatTrans 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.ProdComparison
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (F : CategoryTheory.Functor C D) (A : C) : F.comp (CategoryTheory.Limits.coprod.functor.obj (F.obj A)) ⟶ (CategoryTheory.Limits.coprod.functor.obj A).comp F
• CategoryTheory.Limits.coprodComparisonNatTrans_app 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.ProdComparison
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (F : CategoryTheory.Functor C D) (A B : C) : (CategoryTheory.Limits.coprodComparisonNatTrans F A).app B = CategoryTheory.Limits.coprodComparison F A B
• CategoryTheory.Limits.coprodComparisonNatIso 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.ProdComparison
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] : F.comp (CategoryTheory.Limits.coprod.functor.obj (F.obj A)) ≅ (CategoryTheory.Limits.coprod.functor.obj A).comp F
• CategoryTheory.Limits.coprodComparisonNatIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.ProdComparison
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] : (CategoryTheory.Limits.coprodComparisonNatIso F A).hom = CategoryTheory.Limits.coprodComparisonNatTrans F A
• CategoryTheory.Limits.coprodComparisonNatIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.ProdComparison
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] : (CategoryTheory.Limits.coprodComparisonNatIso F A).inv = (CategoryTheory.asIso { app := fun B => CategoryTheory.Limits.coprodComparison F A B, naturality := ⋯ }).inv
• CategoryTheory.Limits.preservesBinaryCoproducts_of_isIso_coprodComparison 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] [i : ∀ {X Y : C}, CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison G X Y)] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) G
• CategoryTheory.Limits.hasBinaryCoproducts_of_hasBinaryBiproducts 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Limits.HasBinaryCoproducts C
• CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryCoproducts 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Limits.HasBinaryBiproducts C
• hasBinaryCoproducts_of_hasInitial_and_pushouts 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] : CategoryTheory.Limits.HasBinaryCoproducts C
• CategoryTheory.coprodMonad 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Monad C
• CategoryTheory.algebraEquivUnder 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.coprodMonad X).Algebra ≌ CategoryTheory.Under X
• CategoryTheory.algebraToUnder 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Functor (CategoryTheory.coprodMonad X).Algebra (CategoryTheory.Under X)
• CategoryTheory.underToAlgebra 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Functor (CategoryTheory.Under X) (CategoryTheory.coprodMonad X).Algebra
• CategoryTheory.coprodMonad_obj 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (Y : C) : (CategoryTheory.coprodMonad X).obj Y = (X ⨿ Y)
• CategoryTheory.underToAlgebra_obj_A 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (f : CategoryTheory.Under X) : ((CategoryTheory.underToAlgebra X).obj f).A = f.right
• CategoryTheory.algebraEquivUnder_functor 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.algebraEquivUnder X).functor = CategoryTheory.algebraToUnder X
• CategoryTheory.algebraEquivUnder_inverse 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.algebraEquivUnder X).inverse = CategoryTheory.underToAlgebra X
• CategoryTheory.coprodMonad_map 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) : (CategoryTheory.coprodMonad X).map g = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) g
• CategoryTheory.coprodMonad_η_app 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (x✝ : C) : (CategoryTheory.coprodMonad X).η.app x✝ = CategoryTheory.Limits.coprod.inr
• CategoryTheory.underToAlgebra_obj_a 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (f : CategoryTheory.Under X) : ((CategoryTheory.underToAlgebra X).obj f).a = CategoryTheory.Limits.coprod.desc f.hom (CategoryTheory.CategoryStruct.id f.right)
• CategoryTheory.algebraToUnder_obj 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (A : (CategoryTheory.coprodMonad X).Algebra) : (CategoryTheory.algebraToUnder X).obj A = CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl A.a)
• CategoryTheory.coprodMonad_μ_app 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (x✝ : C) : (CategoryTheory.coprodMonad X).μ.app x✝ = CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.id (X ⨿ x✝))
• CategoryTheory.underToAlgebra_map_f 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] {X✝ Y✝ : CategoryTheory.Under X} (g : X✝ ⟶ Y✝) : ((CategoryTheory.underToAlgebra X).map g).f = CategoryTheory.Under.Hom.right g
• CategoryTheory.algebraEquivUnder_counitIso 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.algebraEquivUnder X).counitIso = CategoryTheory.NatIso.ofComponents (fun f => CategoryTheory.Under.isoMk (CategoryTheory.Iso.refl (((CategoryTheory.underToAlgebra X).comp (CategoryTheory.algebraToUnder X)).obj f).right) ⋯) ⋯
• CategoryTheory.algebraToUnder_map 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] {X✝ Y✝ : (CategoryTheory.coprodMonad X).Algebra} (f : X✝ ⟶ Y✝) : (CategoryTheory.algebraToUnder X).map f = CategoryTheory.Under.homMk f.f ⋯
• CategoryTheory.algebraEquivUnder_unitIso 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.algebraEquivUnder X).unitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Monad.Algebra.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.coprodMonad X).Algebra).obj A).A) ⋯) ⋯
• CategoryTheory.Under.costar 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Functor C (CategoryTheory.Under X)
• CategoryTheory.Under.instIsRightAdjointForget 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.Under.forget X).IsRightAdjoint
• CategoryTheory.Under.instIsLeftAdjointCostar 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.Under.costar X).IsLeftAdjoint
• CategoryTheory.Under.costarAdjForget 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Under.costar X ⊣ CategoryTheory.Under.forget X
• CategoryTheory.Under.costar_obj_left 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (X✝ : C) : ((CategoryTheory.Under.costar X).obj X✝).left = { as := PUnit.unit }
• CategoryTheory.Under.costar_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (X✝ : C) : ((CategoryTheory.Under.costar X).obj X✝).hom = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.id (X ⨿ X✝)))
• CategoryTheory.hasFiniteCoproducts_of_has_binary_and_initial 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasFiniteCoproducts C
• CategoryTheory.Limits.hasCoequalizers_of_hasPushouts_and_binary_coproducts 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] : CategoryTheory.Limits.HasCoequalizers C
• CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.constructCoequalizer 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) : C
• CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCocone 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) : CategoryTheory.Limits.Cocone F
• CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCoconeIsColimit 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCocone F)
• CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) : F.obj CategoryTheory.Limits.WalkingParallelPair.one ⟶ CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.constructCoequalizer F
• CategoryTheory.Limits.preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) G] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan G] : CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G
• CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) : CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl F = CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingParallelPair.one)) (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)) (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingParallelPair.one)) (F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
• CategoryTheory.Limits.hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers 📋 Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.HasPushouts C
• CategoryTheory.Subobject.semilatticeSup 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {B : C} : SemilatticeSup (CategoryTheory.Subobject B)
• CategoryTheory.Subobject.instLattice 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {B : C} : Lattice (CategoryTheory.Subobject B)
• CategoryTheory.Subobject.sup_factors_of_factors_left 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A B : C} {X Y : CategoryTheory.Subobject B} {f : A ⟶ B} (P : X.Factors f) : (X ⊔ Y).Factors f
• CategoryTheory.Subobject.sup_factors_of_factors_right 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A B : C} {X Y : CategoryTheory.Subobject B} {f : A ⟶ B} (P : Y.Factors f) : (X ⊔ Y).Factors f
• CategoryTheory.Subobject.finset_sup_factors 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] {I : Type u_1} {A B : C} {s : Finset I} {P : I → CategoryTheory.Subobject B} {f : A ⟶ B} (h : ∃ i ∈ s, (P i).Factors f) : (s.sup P).Factors f
• CategoryTheory.MonoOver.sup 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} : CategoryTheory.Functor (CategoryTheory.MonoOver A) (CategoryTheory.Functor (CategoryTheory.MonoOver A) (CategoryTheory.MonoOver A))
• CategoryTheory.Subobject.sup 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} : CategoryTheory.Functor (CategoryTheory.Subobject A) (CategoryTheory.Functor (CategoryTheory.Subobject A) (CategoryTheory.Subobject A))
• CategoryTheory.MonoOver.leSupLeft 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} (f g : CategoryTheory.MonoOver A) : f ⟶ (CategoryTheory.MonoOver.sup.obj f).obj g
• CategoryTheory.MonoOver.leSupRight 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} (f g : CategoryTheory.MonoOver A) : g ⟶ (CategoryTheory.MonoOver.sup.obj f).obj g
• CategoryTheory.MonoOver.supLe 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} (f g h : CategoryTheory.MonoOver A) : (f ⟶ h) → (g ⟶ h) → ((CategoryTheory.MonoOver.sup.obj f).obj g ⟶ h)
• CategoryTheory.IsSifted.instIsSiftedOrEmptyOfHasBinaryCoproducts 📋 Mathlib.CategoryTheory.Limits.Sifted
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.IsSiftedOrEmpty C
• CategoryTheory.IsSifted.isSifted_of_hasBinaryCoproducts_and_nonempty 📋 Mathlib.CategoryTheory.Limits.Sifted
  {C : Type u} [CategoryTheory.Category.{v, u} C] [Nonempty C] [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.IsSifted C
• CategoryTheory.HasPullbacksOfInclusions 📋 Mathlib.CategoryTheory.Extensive
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] : Prop
• CategoryTheory.HasPullbacksOfInclusions.instOfHasPullbacks 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.HasPullbacksOfInclusions C
• CategoryTheory.PreservesPullbacksOfInclusions 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryCoproducts C] : Prop
• CategoryTheory.PreservesPullbacksOfInclusions.instOfPreservesLimitsOfShapeWalkingCospan 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Limits.HasBinaryCoproducts C] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] : CategoryTheory.PreservesPullbacksOfInclusions F
• CategoryTheory.HasPullbacksOfInclusions.hasPullbackInl 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasBinaryCoproducts C} [self : CategoryTheory.HasPullbacksOfInclusions C] {X Y Z : C} (f : Z ⟶ X ⨿ Y) : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inl f
• CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.HasPullbacksOfInclusions C] {X Y Z : C} (f : Z ⟶ X ⨿ Y) : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inr f
• CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr' 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.HasPullbacksOfInclusions C] {X Y Z : C} (f : Z ⟶ X ⨿ Y) : CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.coprod.inr
• CategoryTheory.HasPullbacksOfInclusions.mk 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [hasPullbackInl : ∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y), CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inl f] : CategoryTheory.HasPullbacksOfInclusions C
• CategoryTheory.HasPullbacksOfInclusions.preservesPullbackInl' 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.HasPullbacksOfInclusions C] {X Y Z : C} (f : Z ⟶ X ⨿ Y) : CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.coprod.inl
• CategoryTheory.PreservesPullbacksOfInclusions.mk 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryCoproducts C] [preservesPullbackInl : ∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan CategoryTheory.Limits.coprod.inl f) F] : CategoryTheory.PreservesPullbacksOfInclusions F
• CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2} {inst✝¹ : CategoryTheory.Category.{v_2, u_2} D} {F : CategoryTheory.Functor C D} {inst✝² : CategoryTheory.Limits.HasBinaryCoproducts C} [self : CategoryTheory.PreservesPullbacksOfInclusions F] {X Y Z : C} (f : Z ⟶ X ⨿ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan CategoryTheory.Limits.coprod.inl f) F
• CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl' 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Limits.HasBinaryCoproducts C] (F : CategoryTheory.Functor C D) [CategoryTheory.PreservesPullbacksOfInclusions F] {X Y Z : C} (f : Z ⟶ X ⨿ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f CategoryTheory.Limits.coprod.inl) F
• CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Limits.HasBinaryCoproducts C] (F : CategoryTheory.Functor C D) [CategoryTheory.PreservesPullbacksOfInclusions F] {X Y Z : C} (f : Z ⟶ X ⨿ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan CategoryTheory.Limits.coprod.inr f) F
• CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr' 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Limits.HasBinaryCoproducts C] (F : CategoryTheory.Functor C D) [CategoryTheory.PreservesPullbacksOfInclusions F] {X Y Z : C} (f : Z ⟶ X ⨿ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f CategoryTheory.Limits.coprod.inr) F
• Preorder.instHasBinaryCoproducts 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [SemilatticeSup C] : CategoryTheory.Limits.HasBinaryCoproducts C
• Preorder.semilatticeSupOfHasBinaryCoproducts 📋 Mathlib.CategoryTheory.Limits.Preorder
  (C : Type u) [PartialOrder C] [CategoryTheory.Limits.HasBinaryCoproducts C] : SemilatticeSup C
• CategoryTheory.Limits.CompleteLattice.instHasBinaryCoproductsOfOrderBot 📋 Mathlib.CategoryTheory.Limits.Lattice
  {α : Type u} [SemilatticeSup α] [OrderBot α] : CategoryTheory.Limits.HasBinaryCoproducts α
• HomotopicalAlgebra.Cylinder.instIsGoodSymmOfRespectsIsoCofibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A) [CategoryTheory.Limits.HasBinaryCoproducts C] [HomotopicalAlgebra.CategoryWithCofibrations C] [P.IsGood] [(HomotopicalAlgebra.cofibrations C).RespectsIso] : P.symm.IsGood
• HomotopicalAlgebra.Cylinder.instIsVeryGoodSymmOfRespectsIsoCofibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A) [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.cofibrations C).RespectsIso] [CategoryTheory.Limits.HasBinaryCoproducts C] [P.IsVeryGood] : P.symm.IsVeryGood
• HomotopicalAlgebra.Precylinder.symm_i 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A) [CategoryTheory.Limits.HasBinaryCoproducts C] : P.symm.i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding A A).hom P.i
• HomotopicalAlgebra.Cylinder.symm_i 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A) [CategoryTheory.Limits.HasBinaryCoproducts C] : P.symm.i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding A A).hom P.i
• HomotopicalAlgebra.Precylinder.symm_i_assoc 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A) [CategoryTheory.Limits.HasBinaryCoproducts C] {Z : C} (h : P.symm.I ⟶ Z) : CategoryTheory.CategoryStruct.comp P.symm.i h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding A A).hom P.i) h
• HomotopicalAlgebra.Cylinder.symm_i_assoc 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A) [CategoryTheory.Limits.HasBinaryCoproducts C] {Z : C} (h : P.symm.I ⟶ Z) : CategoryTheory.CategoryStruct.comp P.symm.i h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding A A).hom P.i) h
• CategoryTheory.Adhesive.instHasBinaryCoproductsSubobject 📋 Mathlib.CategoryTheory.Adhesive.Subobject
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Adhesive C] {X : C} : CategoryTheory.Limits.HasBinaryCoproducts (CategoryTheory.Subobject X)
• CategoryTheory.IsMonoidalDistrib 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] : Prop
• CategoryTheory.IsMonoidalLeftDistrib 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] : Prop
• CategoryTheory.IsMonoidalRightDistrib 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] : Prop
• CategoryTheory.MonoidalClosed.isMonoidalLeftDistrib 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.MonoidalClosed C] : CategoryTheory.IsMonoidalLeftDistrib C
• CategoryTheory.IsMonoidalDistrib.toIsMonoidalLeftDistrib 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.Limits.HasBinaryCoproducts C} [self : CategoryTheory.IsMonoidalDistrib C] : CategoryTheory.IsMonoidalLeftDistrib C
• CategoryTheory.IsMonoidalDistrib.toIsMonoidalRightDistrib 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.Limits.HasBinaryCoproducts C} [self : CategoryTheory.IsMonoidalDistrib C] : CategoryTheory.IsMonoidalRightDistrib C
• CategoryTheory.IsMonoidalDistrib.of_MonoidalPreadditive_with_binary_coproducts 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] : CategoryTheory.IsMonoidalDistrib C
• CategoryTheory.isMonoidalDistrib.of_symmetric_monoidal_closed 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.MonoidalClosed C] : CategoryTheory.IsMonoidalDistrib C
• CategoryTheory.SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.IsMonoidalLeftDistrib C] : CategoryTheory.IsMonoidalDistrib C
• CategoryTheory.IsMonoidalDistrib.mk 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [toIsMonoidalLeftDistrib : CategoryTheory.IsMonoidalLeftDistrib C] [toIsMonoidalRightDistrib : CategoryTheory.IsMonoidalRightDistrib C] : CategoryTheory.IsMonoidalDistrib C
• CategoryTheory.IsMonoidalLeftDistrib.preservesBinaryCoproducts_tensorLeft 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.Limits.HasBinaryCoproducts C} [self : CategoryTheory.IsMonoidalLeftDistrib C] (X : C) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (CategoryTheory.MonoidalCategory.tensorLeft X)
• CategoryTheory.IsMonoidalRightDistrib.preservesBinaryCoproducts_tensorRight 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.Limits.HasBinaryCoproducts C} [self : CategoryTheory.IsMonoidalRightDistrib C] (X : C) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (CategoryTheory.MonoidalCategory.tensorRight X)
• CategoryTheory.isMonoidalLeftDistrib.of_endofunctors 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.IsMonoidalLeftDistrib (CategoryTheory.Functor C C)
• CategoryTheory.IsMonoidalLeftDistrib.mk 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] (preservesBinaryCoproducts_tensorLeft : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (CategoryTheory.MonoidalCategory.tensorLeft X) := by infer_instance) : CategoryTheory.IsMonoidalLeftDistrib C
• CategoryTheory.IsMonoidalRightDistrib.mk 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] (preservesBinaryCoproducts_tensorRight : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (CategoryTheory.MonoidalCategory.tensorRight X) := by infer_instance) : CategoryTheory.IsMonoidalRightDistrib C
• CategoryTheory.leftDistrib 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalLeftDistrib C] (X Y Z : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj X (Y ⨿ Z)
• CategoryTheory.rightDistrib 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalRightDistrib C] (X Y Z : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj Z X ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (Y ⨿ Z) X
• CategoryTheory.IsMonoidalLeftDistrib.of_isIso_coprodComparisonTensorLeft 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [i : ∀ {X Y Z : C}, CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft X) Y Z)] : CategoryTheory.IsMonoidalLeftDistrib C
• CategoryTheory.IsMonoidalRightDistrib.of_isIso_coprodComparisonTensorRight 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [i : ∀ {X Y Z : C}, CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorRight X) Y Z)] : CategoryTheory.IsMonoidalRightDistrib C
• CategoryTheory.coprod_inl_leftDistrib_hom 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalLeftDistrib C] {X Y Z : C} : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.leftDistrib X Y Z).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inl
• CategoryTheory.coprod_inl_rightDistrib_hom 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalRightDistrib C] {X Y Z : C} : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (∂R X Y Z).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inl X
• CategoryTheory.coprod_inr_leftDistrib_hom 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalLeftDistrib C] {X Y Z : C} : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.leftDistrib X Y Z).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inr
• CategoryTheory.coprod_inr_rightDistrib_hom 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalRightDistrib C] {X Y Z : C} : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (∂R X Y Z).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inr X
• CategoryTheory.leftDistrib_hom 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalLeftDistrib C] {X Y Z : C} : (CategoryTheory.leftDistrib X Y Z).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inl) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inr)
• CategoryTheory.rightDistrib_hom 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalRightDistrib C] {X Y Z : C} : (∂R X Y Z).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inl X) (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inr X)
• CategoryTheory.whiskerLeft_coprod_inl_leftDistrib_inv 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalLeftDistrib C] {X Y Z : C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inl) (CategoryTheory.leftDistrib X Y Z).inv = CategoryTheory.Limits.coprod.inl
• CategoryTheory.whiskerLeft_coprod_inr_leftDistrib_inv 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalLeftDistrib C] {X Y Z : C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inr) (CategoryTheory.leftDistrib X Y Z).inv = CategoryTheory.Limits.coprod.inr
• CategoryTheory.whiskerRight_coprod_inl_rightDistrib_inv 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalRightDistrib C] {X Y Z : C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inl X) (∂R X Y Z).inv = CategoryTheory.Limits.coprod.inl
• CategoryTheory.whiskerRight_coprod_inr_rightDistrib_inv 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalRightDistrib C] {X Y Z : C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inr X) (∂R X Y Z).inv = CategoryTheory.Limits.coprod.inr
• CategoryTheory.coprod_inl_leftDistrib_hom_assoc 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalLeftDistrib C] {X Y Z Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (Y ⨿ Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistrib X Y Z).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inl) h
• CategoryTheory.coprod_inl_rightDistrib_hom_assoc 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalRightDistrib C] {X Y Z Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (Y ⨿ Z) X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (∂R X Y Z).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inl X) h
• CategoryTheory.coprod_inr_leftDistrib_hom_assoc 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalLeftDistrib C] {X Y Z Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (Y ⨿ Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistrib X Y Z).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inr) h
• CategoryTheory.coprod_inr_rightDistrib_hom_assoc 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalRightDistrib C] {X Y Z Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (Y ⨿ Z) X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (∂R X Y Z).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inr X) h
• CategoryTheory.whiskerLeft_coprod_inl_leftDistrib_inv_assoc 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalLeftDistrib C] {X Y Z Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inl) (CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistrib X Y Z).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h
• CategoryTheory.whiskerLeft_coprod_inr_leftDistrib_inv_assoc 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalLeftDistrib C] {X Y Z Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inr) (CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistrib X Y Z).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h
• CategoryTheory.whiskerRight_coprod_inl_rightDistrib_inv_assoc 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalRightDistrib C] {X Y Z Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj Z X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inl X) (CategoryTheory.CategoryStruct.comp (∂R X Y Z).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h
• CategoryTheory.whiskerRight_coprod_inr_rightDistrib_inv_assoc 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalRightDistrib C] {X Y Z Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj Z X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inr X) (CategoryTheory.CategoryStruct.comp (∂R X Y Z).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h
• CategoryTheory.SymmetricCategory.rightDistrib_of_leftDistrib 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.IsMonoidalDistrib C] {X Y Z : C} : ∂R X Y Z = CategoryTheory.Limits.coprod.mapIso (β_ Y X) (β_ Z X) ≪≫ CategoryTheory.leftDistrib X Y Z ≪≫ β_ X (Y ⨿ Z)
• CategoryTheory.MonoidalClosed.leftDistrib_inv 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.MonoidalClosed C] {X Y Z : C} : (CategoryTheory.leftDistrib X Y Z).inv = CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.Limits.coprod.desc (CategoryTheory.MonoidalClosed.curry CategoryTheory.Limits.coprod.inl) (CategoryTheory.MonoidalClosed.curry CategoryTheory.Limits.coprod.inr))
• CategoryTheory.coprodComparison_tensorLeft_braiding_hom 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.BraidedCategory C] {X Y Z : C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft X) Y Z) (β_ X (Y ⨿ Z)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (β_ X Y).hom (β_ X Z).hom) (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorRight X) Y Z)
• CategoryTheory.coprodComparison_tensorRight_braiding_hom 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.SymmetricCategory C] {X Y Z : C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorRight X) Y Z) (β_ (Y ⨿ Z) X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (β_ Y X).hom (β_ Z X).hom) (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft X) Y Z)
• CategoryTheory.IsCartesianDistributive 📋 Mathlib.CategoryTheory.Distributive.Cartesian
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] : Prop
• CategoryTheory.IsCartesianDistributive.monoCoprod 📋 Mathlib.CategoryTheory.Distributive.Cartesian
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsCartesianDistributive C] : CategoryTheory.Limits.MonoCoprod C
• CategoryTheory.IsCartesianDistributive.of_isMonoidalLeftDistrib 📋 Mathlib.CategoryTheory.Distributive.Cartesian
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalLeftDistrib C] : CategoryTheory.IsCartesianDistributive C
• CategoryTheory.monoidalOfHasFiniteCoproducts 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.MonoidalCategory C
• CategoryTheory.symmetricOfHasFiniteCoproducts 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.SymmetricCategory C
• CategoryTheory.monoidalOfHasFiniteCoproducts.tensorObj 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X Y : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y = (X ⨿ Y)
• CategoryTheory.symmetricOfHasFiniteCoproducts_braiding 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P Q : C) : β_ P Q = CategoryTheory.Limits.coprod.braiding P Q
• CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerLeft 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) {Y Z : C} (f : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) f
• CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerRight 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] {X Y : C} (f : X ⟶ Y) (Z : C) : CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z = CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id Z)
• CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_inv 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv = CategoryTheory.Limits.coprod.inr
• CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_inv 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv = CategoryTheory.Limits.coprod.inl
• CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_hom 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.initial.to X) (CategoryTheory.CategoryStruct.id X)
• CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_hom 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.initial.to X)
• CategoryTheory.monoidalOfHasFiniteCoproducts.tensorHom 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.tensorHom f g = CategoryTheory.Limits.coprod.map f g
• CategoryTheory.monoidalOfHasFiniteCoproducts.associator_hom 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X Y Z : C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inr)
• CategoryTheory.monoidalOfHasFiniteCoproducts.associator_inv 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X Y Z : C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inl) (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) CategoryTheory.Limits.coprod.inr)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c