{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {motive : HomotopicalAlgebra.CategoryWithCofibrations C → Sort u_1} →
      (t : HomotopicalAlgebra.CategoryWithCofibrations C) →
        ((cofibrations : CategoryTheory.MorphismProperty C) → motive { cofibrations := cofibrations }) → motive t