Theorems · Definition · category theory

HomotopicalAlgebra.bifibrantObjects

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

The property that is satisfied by bifibrant objects, i.e. objects that are both cofibrant and fibrant. (This is only introduced in order to consider the full subcategory BifibrantObject. Otherwise, the typeclasses IsCofibrant and IsFibrant are preferred.)

Defined in

Mathlib.AlgebraicTopology.ModelCategory.Bifibrant

Cited by

37 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryHomotopicalAlgebra.CategoryWithCofibrationsCategoryTheory.Limits.HasInitialHomotopicalAlgebra.CategoryWithFibrationsCategoryTheory.Limits.HasTerminal