Theorems · Definition · category theory

HomotopicalAlgebra.Precylinder.i

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      (P : HomotopicalAlgebra.Precylinder A) → [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct A A] → A ⨿ A ⟶ P.I

the map from the coproduct of two copies of A to P.I, when P is a cylinder object for A. P shall be a good cylinder object when this morphism is a cofibration.

Defined in

Mathlib.AlgebraicTopology.ModelCategory.Cylinder

Cited by

13 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasBinaryCoproduct