∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C) {Y Z : C}
  [HomotopicalAlgebra.IsCofibrant X] (g : Y ⟶ Z) [HomotopicalAlgebra.IsFibrant Y] [HomotopicalAlgebra.IsFibrant Z]
  [HomotopicalAlgebra.WeakEquivalence g], Function.Bijective fun f => f.postcomp g