Theorems · Definition · category theory

HomotopicalAlgebra.cofibrantObjects

(C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithCofibrations C] →
      [CategoryTheory.Limits.HasInitial C] → CategoryTheory.ObjectProperty C

The property that is satisfied by cofibrant objects. (This is only introduced in order to consider the full subcategory CofibrantObject. Otherwise, the typeclass IsCofibrant is preferred.)

Defined in

Mathlib.AlgebraicTopology.ModelCategory.Bifibrant

Cited by

34 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryHomotopicalAlgebra.CategoryWithCofibrationsCategoryTheory.Limits.HasInitial