Loogle!

Result

Found 133 declarations mentioning CategoryTheory.Limits.HasBinaryCoproduct.

• CategoryTheory.Limits.HasBinaryCoproduct 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : Prop
• CategoryTheory.Limits.coprod 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : C
• CategoryTheory.Limits.codiag 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproduct X X] : X ⨿ X ⟶ X
• CategoryTheory.Limits.coprod.inl 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] : X ⟶ X ⨿ Y
• CategoryTheory.Limits.coprod.inr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] : Y ⟶ X ⨿ Y
• CategoryTheory.Limits.coprod.mapIso 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : W ⨿ X ≅ Y ⨿ Z
• CategoryTheory.Limits.coprod.desc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : X ⨿ Y ⟶ W
• CategoryTheory.Limits.coprodIsCoprod 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr)
• CategoryTheory.Limits.coprod.epi_desc_of_epi_left 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [CategoryTheory.Epi f] : CategoryTheory.Epi (CategoryTheory.Limits.coprod.desc f g)
• CategoryTheory.Limits.coprod.epi_desc_of_epi_right 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [CategoryTheory.Epi g] : CategoryTheory.Epi (CategoryTheory.Limits.coprod.desc f g)
• CategoryTheory.Limits.coprod.map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : W ⨿ X ⟶ Y ⨿ Z
• CategoryTheory.Limits.coprod.diag_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X X] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag X) f = CategoryTheory.Limits.coprod.desc f f
• CategoryTheory.Limits.coprod.map_id_id 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (X ⨿ Y)
• CategoryTheory.Limits.coprod.desc_inl_inr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr = CategoryTheory.CategoryStruct.id (X ⨿ Y)
• CategoryTheory.Limits.coprod.inl_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.desc f g) = f
• CategoryTheory.Limits.coprod.inr_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprod.desc f g) = g
• CategoryTheory.Limits.isIso_coprod 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.IsIso f] [CategoryTheory.IsIso g] : CategoryTheory.IsIso (CategoryTheory.Limits.coprod.map f g)
• CategoryTheory.Limits.coprod.map_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Epi f] [CategoryTheory.Epi g] [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] : CategoryTheory.Epi (CategoryTheory.Limits.coprod.map f g)
• CategoryTheory.Limits.coprod.map_codiag 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasBinaryCoproduct X X] [CategoryTheory.Limits.HasBinaryCoproduct Y Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f f) (CategoryTheory.Limits.codiag Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag X) f
• CategoryTheory.Limits.coprod.mapIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (CategoryTheory.Limits.coprod.mapIso f g).hom = CategoryTheory.Limits.coprod.map f.hom g.hom
• CategoryTheory.Limits.coprod.mapIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (CategoryTheory.Limits.coprod.mapIso f g).inv = CategoryTheory.Limits.coprod.map f.inv g.inv
• CategoryTheory.Limits.coprod.inl_desc_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h : W ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc f g) h) = CategoryTheory.CategoryStruct.comp f h
• CategoryTheory.Limits.coprod.inr_desc_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h : W ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc f g) h) = CategoryTheory.CategoryStruct.comp g h
• CategoryTheory.Limits.coprod.desc_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {V W X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : V ⟶ W) (g : X ⟶ V) (h : Y ⟶ V) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc g h) f = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp g f) (CategoryTheory.CategoryStruct.comp h f)
• CategoryTheory.Limits.coprod.inl_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.map f g) = CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.coprod.inl
• CategoryTheory.Limits.coprod.inr_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprod.map f g) = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inr
• CategoryTheory.Limits.coprod.desc_comp_inl_comp_inr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W Y] [CategoryTheory.Limits.HasBinaryCoproduct X Z] (g : W ⟶ X) (g' : Y ⟶ Z) : CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inl) (CategoryTheory.CategoryStruct.comp g' CategoryTheory.Limits.coprod.inr) = CategoryTheory.Limits.coprod.map g g'
• CategoryTheory.Limits.coprod.desc' 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : { l // CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl l = f ∧ CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr l = g }
• CategoryTheory.Limits.coprod.map_codiag_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasBinaryCoproduct X X] [CategoryTheory.Limits.HasBinaryCoproduct Y Y] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag Y) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag X) (CategoryTheory.CategoryStruct.comp f h)
• CategoryTheory.Limits.coprod.map_inl_inr_codiag 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr) (CategoryTheory.Limits.codiag (X ⨿ Y)) = CategoryTheory.CategoryStruct.id (X ⨿ Y)
• CategoryTheory.Limits.coprod.map_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S T U V W : C} [CategoryTheory.Limits.HasBinaryCoproduct U W] [CategoryTheory.Limits.HasBinaryCoproduct T V] (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map h k) (CategoryTheory.Limits.coprod.desc f g) = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp k g)
• CategoryTheory.Limits.coprod.desc_comp_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {V W X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : V ⟶ W) (g : X ⟶ V) (h : Y ⟶ V) {Z : C} (h✝ : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc g h) (CategoryTheory.CategoryStruct.comp f h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp g f) (CategoryTheory.CategoryStruct.comp h f)) h✝
• CategoryTheory.Limits.coprod.inl_map_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⨿ Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h)
• CategoryTheory.Limits.coprod.inr_map_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⨿ Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h)
• CategoryTheory.Limits.coprod.map_comp_id 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasBinaryCoproduct Z W] [CategoryTheory.Limits.HasBinaryCoproduct Y W] [CategoryTheory.Limits.HasBinaryCoproduct X W] : CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id W) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.Limits.coprod.map g (CategoryTheory.CategoryStruct.id W))
• CategoryTheory.Limits.coprod.map_id_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct W Y] [CategoryTheory.Limits.HasBinaryCoproduct W Z] : CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) f) (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) g)
• CategoryTheory.Limits.coprod.map_inl_inr_codiag_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)] {Z : C} (h : X ⨿ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag (X ⨿ Y)) h) = h
• CategoryTheory.Limits.coprod.map_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [CategoryTheory.Limits.HasBinaryCoproduct A₁ B₁] [CategoryTheory.Limits.HasBinaryCoproduct A₂ B₂] [CategoryTheory.Limits.HasBinaryCoproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) (CategoryTheory.Limits.coprod.map h k) = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g k)
• CategoryTheory.Limits.coprod.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] {f g : X ⨿ Y ⟶ W} (h₁ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl g) (h₂ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr g) : f = g
• CategoryTheory.Limits.coprod.hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] {f g : X ⨿ Y ⟶ W} : f = g ↔ CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl g ∧ CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr g
• CategoryTheory.Limits.coprod.map_desc_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S T U V W : C} [CategoryTheory.Limits.HasBinaryCoproduct U W] [CategoryTheory.Limits.HasBinaryCoproduct T V] (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W) {Z : C} (h✝ : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map h k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc f g) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp k g)) h✝
• CategoryTheory.Limits.coprod.map_comp_id_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasBinaryCoproduct Z W] [CategoryTheory.Limits.HasBinaryCoproduct Y W] [CategoryTheory.Limits.HasBinaryCoproduct X W] {Z✝ : C} (h : Z ⨿ W ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id W)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map g (CategoryTheory.CategoryStruct.id W)) h)
• CategoryTheory.Limits.coprod.map_id_comp_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct W Y] [CategoryTheory.Limits.HasBinaryCoproduct W Z] {Z✝ : C} (h : W ⨿ Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) g) h)
• CategoryTheory.Limits.coprod.map_map_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [CategoryTheory.Limits.HasBinaryCoproduct A₁ B₁] [CategoryTheory.Limits.HasBinaryCoproduct A₂ B₂] [CategoryTheory.Limits.HasBinaryCoproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) {Z : C} (h✝ : A₃ ⨿ B₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map h k) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g k)) h✝
• CategoryTheory.Limits.coprodComparison 📋 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) (A B : C) [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] : F.obj A ⨿ F.obj B ⟶ F.obj (A ⨿ B)
• CategoryTheory.Limits.coprodComparison_inl 📋 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) {A B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprodComparison F A B) = F.map CategoryTheory.Limits.coprod.inl
• CategoryTheory.Limits.coprodComparison_inr 📋 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) {A B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprodComparison F A B) = F.map CategoryTheory.Limits.coprod.inr
• CategoryTheory.Limits.coprodComparison_inl_assoc 📋 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) {A B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj (A ⨿ B) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B) h) = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inl) h
• CategoryTheory.Limits.coprodComparison_inr_assoc 📋 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) {A B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj (A ⨿ B) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B) h) = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inr) h
• CategoryTheory.Limits.map_inl_inv_coprodComparison 📋 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) {A B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inl) (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) = CategoryTheory.Limits.coprod.inl
• CategoryTheory.Limits.map_inr_inv_coprodComparison 📋 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) {A B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inr) (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) = CategoryTheory.Limits.coprod.inr
• CategoryTheory.Limits.map_inl_inv_coprodComparison_assoc 📋 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) {A B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] {Z : D} (h : F.obj A ⨿ F.obj B ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inl) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h
• CategoryTheory.Limits.map_inr_inv_coprodComparison_assoc 📋 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) {A B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] {Z : D} (h : F.obj A ⨿ F.obj B ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inr) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h
• CategoryTheory.Limits.coprodComparison_natural 📋 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) {A A' B B' : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct A' B'] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B) (F.map (CategoryTheory.Limits.coprod.map f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) (CategoryTheory.Limits.coprodComparison F A' B')
• CategoryTheory.Limits.coprodComparison_natural_assoc 📋 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) {A A' B B' : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct A' B'] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') {Z : D} (h : F.obj (A' ⨿ B') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.coprod.map f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A' B') h)
• CategoryTheory.Limits.coprodComparison_inv_natural 📋 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) {A A' B B' : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct A' B'] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A' B')] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) (CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.coprod.map f g)) (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A' B'))
• CategoryTheory.Limits.coprodComparison_inv_natural_assoc 📋 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) {A A' B B' : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct A' B'] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A' B')] {Z : D} (h : F.obj A' ⨿ F.obj B' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.coprod.map f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A' B')) h)
• CategoryTheory.Limits.epi_coprod_to_pushout 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] : CategoryTheory.Epi (CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.pushout.inl f g) (CategoryTheory.Limits.pushout.inr f g))
• CategoryTheory.Limits.coprod.fst 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : X ⨿ Y ⟶ X
• CategoryTheory.Limits.coprod.snd 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : X ⨿ Y ⟶ Y
• CategoryTheory.Limits.instEpiFst 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.Epi (CategoryTheory.Limits.coprod.fst X Y)
• CategoryTheory.Limits.instEpiSnd 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.Epi (CategoryTheory.Limits.coprod.snd X Y)
• CategoryTheory.Limits.coprod.inl_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.fst X Y) = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.coprod.inr_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprod.snd X Y) = CategoryTheory.CategoryStruct.id Y
• CategoryTheory.Limits.coprod.inl_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.fst X Y) h) = h
• CategoryTheory.Limits.coprod.inr_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.snd X Y) h) = h
• CategoryTheory.Limits.coprod.inl_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.snd X Y) = 0
• CategoryTheory.Limits.coprod.inr_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprod.fst X Y) = 0
• CategoryTheory.Limits.coprod.inl_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.snd X Y) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Limits.coprod.inr_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.fst X Y) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Limits.PreservesColimitPair.iso 📋 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) (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasBinaryCoproduct (G.obj X) (G.obj Y)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) G] : G.obj X ⨿ G.obj Y ≅ G.obj (X ⨿ Y)
• CategoryTheory.Limits.instIsIsoCoprodComparison 📋 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) (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasBinaryCoproduct (G.obj X) (G.obj Y)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) G] : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison G X Y)
• CategoryTheory.Limits.PreservesColimitPair.of_iso_coprod_comparison 📋 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) (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasBinaryCoproduct (G.obj X) (G.obj Y)] [i : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison G X Y)] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) G
• CategoryTheory.Limits.isColimitOfHasBinaryCoproductOfPreservesColimit 📋 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) (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) G] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (G.map CategoryTheory.Limits.coprod.inl) (G.map CategoryTheory.Limits.coprod.inr))
• CategoryTheory.Limits.PreservesColimitPair.iso_hom 📋 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) (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasBinaryCoproduct (G.obj X) (G.obj Y)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) G] : (CategoryTheory.Limits.PreservesColimitPair.iso G X Y).hom = CategoryTheory.Limits.coprodComparison G X Y
• CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryCoproduct 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.Limits.HasBinaryBiproduct X Y
• coprodIsoPushout 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : X ⨿ Y ≅ CategoryTheory.Limits.pushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)
• inl_coprodIsoPushout_inv 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) (coprodIsoPushout X Y).inv = CategoryTheory.Limits.coprod.inl
• inr_coprodIsoPushout_inv 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) (coprodIsoPushout X Y).inv = CategoryTheory.Limits.coprod.inr
• inl_coprodIsoPushout_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (coprodIsoPushout X Y).hom = CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)
• inr_coprodIsoPushout_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (coprodIsoPushout X Y).hom = CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)
• inl_coprodIsoPushout_inv_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : X ⨿ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h
• inr_coprodIsoPushout_inv_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : X ⨿ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h
• inl_coprodIsoPushout_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) h
• inr_coprodIsoPushout_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) h
• CategoryTheory.IsPushout.of_hasBinaryCoproduct' 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.IsPushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y) CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr
• CategoryTheory.IsPushout.of_coprod_inl_with_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} (f : A ⟶ B) (X : C) [CategoryTheory.Limits.HasBinaryCoproduct A X] [CategoryTheory.Limits.HasBinaryCoproduct B X] : CategoryTheory.IsPushout CategoryTheory.Limits.coprod.inl f (CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id X)) CategoryTheory.Limits.coprod.inl
• CategoryTheory.Projective.instCoprod 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P Q : C} [CategoryTheory.Limits.HasBinaryCoproduct P Q] [CategoryTheory.Projective P] [CategoryTheory.Projective Q] : CategoryTheory.Projective (P ⨿ Q)
• CategoryTheory.Limits.instHasBinaryCoproductOppositeOp 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} [CategoryTheory.Limits.HasBinaryProduct A B] : CategoryTheory.Limits.HasBinaryCoproduct (Opposite.op A) (Opposite.op B)
• CategoryTheory.isSeparator_coprod_of_isSeparator_left 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (G H : C) [CategoryTheory.Limits.HasBinaryCoproduct G H] (hG : CategoryTheory.IsSeparator G) : CategoryTheory.IsSeparator (G ⨿ H)
• CategoryTheory.isSeparator_coprod_of_isSeparator_right 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (G H : C) [CategoryTheory.Limits.HasBinaryCoproduct G H] (hH : CategoryTheory.IsSeparator H) : CategoryTheory.IsSeparator (G ⨿ H)
• CategoryTheory.isSeparator_coprod 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (G H : C) [CategoryTheory.Limits.HasBinaryCoproduct G H] : CategoryTheory.IsSeparator (G ⨿ H) ↔ (CategoryTheory.ObjectProperty.pair G H).IsSeparating
• CategoryTheory.ObjectProperty.prop_coprod 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderBinaryCoproducts] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] (hX : P X) (hY : P Y) : P (X ⨿ Y)
• CategoryTheory.Limits.MonoCoprod.instMonoInl 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B : C} [CategoryTheory.Limits.MonoCoprod C] [CategoryTheory.Limits.HasBinaryCoproduct A B] : CategoryTheory.Mono CategoryTheory.Limits.coprod.inl
• CategoryTheory.Limits.MonoCoprod.instMonoInr 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B : C} [CategoryTheory.Limits.MonoCoprod C] [CategoryTheory.Limits.HasBinaryCoproduct A B] : CategoryTheory.Mono CategoryTheory.Limits.coprod.inr
• CategoryTheory.Mono.inl_of_binaryCoproductDisjoint 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.Mono CategoryTheory.Limits.coprod.inl
• CategoryTheory.Mono.inr_of_binaryCoproductDisjoint 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.Mono CategoryTheory.Limits.coprod.inr
• CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjoint 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr] : CategoryTheory.Limits.IsInitial (CategoryTheory.Limits.pullback CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr)
• CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] [CategoryTheory.Limits.HasBinaryCoproduct X Y] (s : CategoryTheory.Limits.PullbackCone CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr) (hs : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsInitial s.pt
• HomotopicalAlgebra.instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations_1 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] [h₁ : HomotopicalAlgebra.Cofibration f₁] [h₂ : HomotopicalAlgebra.Cofibration f₂] [CategoryTheory.Limits.HasBinaryCoproduct X₁ X₂] [CategoryTheory.Limits.HasBinaryCoproduct Y₁ Y₂] : HomotopicalAlgebra.Cofibration (CategoryTheory.Limits.coprod.map f₁ f₂)
• HomotopicalAlgebra.instCofibrationInlOfIsCofibrant 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X Y : C) [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [CategoryTheory.Limits.HasBinaryCoproduct X Y] [hY : HomotopicalAlgebra.IsCofibrant Y] : HomotopicalAlgebra.Cofibration CategoryTheory.Limits.coprod.inl
• HomotopicalAlgebra.instCofibrationInrOfIsCofibrant 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X Y : C) [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [CategoryTheory.Limits.HasBinaryCoproduct X Y] [hX : HomotopicalAlgebra.IsCofibrant X] : HomotopicalAlgebra.Cofibration CategoryTheory.Limits.coprod.inr
• HomotopicalAlgebra.Cylinder.IsGood 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] [HomotopicalAlgebra.CategoryWithCofibrations C] : Prop
• HomotopicalAlgebra.Cylinder.IsVeryGood 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] : Prop
• HomotopicalAlgebra.Precylinder.i 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] : A ⨿ A ⟶ P.I
• HomotopicalAlgebra.Cylinder.IsVeryGood.toIsGood 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {A : C} {inst✝¹ : HomotopicalAlgebra.CategoryWithWeakEquivalences C} {P : HomotopicalAlgebra.Cylinder A} {inst✝² : CategoryTheory.Limits.HasBinaryCoproduct A A} {inst✝³ : HomotopicalAlgebra.CategoryWithCofibrations C} {inst✝⁴ : HomotopicalAlgebra.CategoryWithFibrations C} [self : P.IsVeryGood] : P.IsGood
• HomotopicalAlgebra.Cylinder.IsVeryGood.fibration_π 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {A : C} {inst✝¹ : HomotopicalAlgebra.CategoryWithWeakEquivalences C} {P : HomotopicalAlgebra.Cylinder A} {inst✝² : CategoryTheory.Limits.HasBinaryCoproduct A A} {inst✝³ : HomotopicalAlgebra.CategoryWithCofibrations C} {inst✝⁴ : HomotopicalAlgebra.CategoryWithFibrations C} [self : P.IsVeryGood] : HomotopicalAlgebra.Fibration P.π
• HomotopicalAlgebra.Cylinder.IsGood.cofibration_i 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {A : C} {inst✝¹ : HomotopicalAlgebra.CategoryWithWeakEquivalences C} {P : HomotopicalAlgebra.Cylinder A} {inst✝² : CategoryTheory.Limits.HasBinaryCoproduct A A} {inst✝³ : HomotopicalAlgebra.CategoryWithCofibrations C} [self : P.IsGood] : HomotopicalAlgebra.Cofibration P.i
• HomotopicalAlgebra.Precylinder.inl_i 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl P.i = P.i₀
• HomotopicalAlgebra.Precylinder.inr_i 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr P.i = P.i₁
• HomotopicalAlgebra.Cylinder.IsGood.mk 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] {P : HomotopicalAlgebra.Cylinder A} [CategoryTheory.Limits.HasBinaryCoproduct A A] [HomotopicalAlgebra.CategoryWithCofibrations C] (cofibration_i : HomotopicalAlgebra.Cofibration P.i := by infer_instance) : P.IsGood
• HomotopicalAlgebra.Cylinder.instIsFibrantIOfIsVeryGood 📋 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.fibrations C).IsStableUnderComposition] [CategoryTheory.Limits.HasBinaryCoproduct A A] [CategoryTheory.Limits.HasTerminal C] [HomotopicalAlgebra.IsFibrant A] [P.IsVeryGood] : HomotopicalAlgebra.IsFibrant P.I
• HomotopicalAlgebra.Cylinder.instIsCofibrantI 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition] [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [HomotopicalAlgebra.IsCofibrant A] [P.IsGood] : HomotopicalAlgebra.IsCofibrant P.I
• HomotopicalAlgebra.Cylinder.IsVeryGood.mk 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] {P : HomotopicalAlgebra.Cylinder A} [CategoryTheory.Limits.HasBinaryCoproduct A A] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [toIsGood : P.IsGood] (fibration_π : HomotopicalAlgebra.Fibration P.π := by infer_instance) : P.IsVeryGood
• HomotopicalAlgebra.Cylinder.instCofibrationI₀ 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition] [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [HomotopicalAlgebra.IsCofibrant A] [P.IsGood] : HomotopicalAlgebra.Cofibration P.i₀
• HomotopicalAlgebra.Cylinder.instCofibrationI₁ 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition] [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [HomotopicalAlgebra.IsCofibrant A] [P.IsGood] : HomotopicalAlgebra.Cofibration P.i₁
• HomotopicalAlgebra.Precylinder.inl_i_assoc 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] {Z : C} (h : P.I ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp P.i h) = CategoryTheory.CategoryStruct.comp P.i₀ h
• HomotopicalAlgebra.Precylinder.inr_i_assoc 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] {Z : C} (h : P.I ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp P.i h) = CategoryTheory.CategoryStruct.comp P.i₁ h
• CategoryTheory.Limits.isPushout_coequalizer_coprod 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasBinaryCoproduct X X] : CategoryTheory.IsPushout (CategoryTheory.Limits.coprod.desc f g) (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)) (CategoryTheory.Limits.coequalizer.π f g) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.coequalizer.π f g))
• CategoryTheory.Limits.hasBinaryCoproduct_zero_left 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.HasBinaryCoproduct 0 X
• CategoryTheory.Limits.hasBinaryCoproduct_zero_right 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.HasBinaryCoproduct X 0
• CategoryTheory.Limits.hasPushout_over_zero 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.Limits.HasPushout 0 0
• CategoryTheory.Limits.pushoutZeroZeroIso 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.Limits.pushout 0 0 ≅ X ⨿ Y
• CategoryTheory.Limits.inl_pushoutZeroZeroIso_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl 0 0) (CategoryTheory.Limits.pushoutZeroZeroIso X Y).hom = CategoryTheory.Limits.coprod.inl
• CategoryTheory.Limits.inr_pushoutZeroZeroIso_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr 0 0) (CategoryTheory.Limits.pushoutZeroZeroIso X Y).hom = CategoryTheory.Limits.coprod.inr
• CategoryTheory.Limits.inl_pushoutZeroZeroIso_inv 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.pushoutZeroZeroIso X Y).inv = CategoryTheory.Limits.pushout.inl 0 0
• CategoryTheory.Limits.inr_pushoutZeroZeroIso_inv 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.pushoutZeroZeroIso X Y).inv = CategoryTheory.Limits.pushout.inr 0 0
• CategoryTheory.Limits.CokernelCofork.mapBifunctor 📋 Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
  {C₁ : Type u_1} {C₂ : Type u_2} {C : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C] {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} (c₁ : CategoryTheory.Limits.CokernelCofork f₁) {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (c₂ : CategoryTheory.Limits.CokernelCofork f₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) [(F.obj c₁.pt).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)] : CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
• CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor 📋 Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
  {C₁ : Type u_1} {C₂ : Type u_2} {C : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C] {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {c₁ : CategoryTheory.Limits.CokernelCofork f₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁) {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {c₂ : CategoryTheory.Limits.CokernelCofork f₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) [(F.obj c₁.pt).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₂ 0) (F.obj c₁.pt)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj Y₂)] [CategoryTheory.Limits.HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj X₂)] : CategoryTheory.Limits.IsColimit (c₁.mapBifunctor c₂ F)
• CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor.exists_desc 📋 Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
  {C₁ : Type u_1} {C₂ : Type u_2} {C : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C] {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {c₁ : CategoryTheory.Limits.CokernelCofork f₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁) {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {c₂ : CategoryTheory.Limits.CokernelCofork f₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) [(F.obj c₁.pt).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₂ 0) (F.obj c₁.pt)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj Y₂)] [CategoryTheory.Limits.HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj X₂)] (s : CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))) : ∃ l, CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.Limits.Cofork.π c₁)).app Y₂) (CategoryTheory.CategoryStruct.comp ((F.obj c₁.pt).map (CategoryTheory.Limits.Cofork.π c₂)) l) = CategoryTheory.Limits.Cofork.π s
• CategoryTheory.IsPushout.of_hasBinaryCoproduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.IsPushout 0 0 CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr
• CategoryTheory.Limits.CokernelCofork.tensor 📋 Mathlib.CategoryTheory.Monoidal.Limits.Cokernels
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {X₁ Y₁ : C} {f₁ : X₁ ⟶ Y₁} (c₁ : CategoryTheory.Limits.CokernelCofork f₁) {X₂ Y₂ : C} {f₂ : X₂ ⟶ Y₂} (c₂ : CategoryTheory.Limits.CokernelCofork f₂) [CategoryTheory.Limits.HasBinaryCoproduct (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ X₂)] : CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.coprod.desc (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₁ Y₂) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y₁ f₂))
• CategoryTheory.Limits.CokernelCofork.isColimitTensor 📋 Mathlib.CategoryTheory.Monoidal.Limits.Cokernels
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {X₁ Y₁ : C} {f₁ : X₁ ⟶ Y₁} {c₁ : CategoryTheory.Limits.CokernelCofork f₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁) {X₂ Y₂ : C} {f₂ : X₂ ⟶ Y₂} {c₂ : CategoryTheory.Limits.CokernelCofork f₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂) [CategoryTheory.Limits.HasBinaryCoproduct (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ X₂)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₂ 0) (CategoryTheory.MonoidalCategory.tensorLeft c₁.pt)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (CategoryTheory.MonoidalCategory.tensorRight Y₂)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (CategoryTheory.MonoidalCategory.tensorRight X₂)] : CategoryTheory.Limits.IsColimit (c₁.tensor c₂)

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