Theorems · Theorem · category theory

HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.BifibrantObject C),
  HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso.inv.app (HomotopicalAlgebra.BifibrantObject.toHoCat.obj X) =
    HomotopicalAlgebra.BifibrantObject.toHoCat.map
      (HomotopicalAlgebra.BifibrantObject.homMk
        (HomotopicalAlgebra.CofibrantObject.mk X.obj).iBifibrantResolutionObj.hom)

Defined in

Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryHomotopicalAlgebra.ModelCategory