{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      {motive : HomotopicalAlgebra.PrepathObject A → Sort u_1} →
        (t : HomotopicalAlgebra.PrepathObject A) →
          ((P : C) →
              (p₀ p₁ : P ⟶ A) →
                (ι : A ⟶ P) →
                  (ι_p₀ : CategoryTheory.CategoryStruct.comp ι p₀ = CategoryTheory.CategoryStruct.id A) →
                    (ι_p₁ : CategoryTheory.CategoryStruct.comp ι p₁ = CategoryTheory.CategoryStruct.id A) →
                      motive { P := P, p₀ := p₀, p₁ := p₁, ι := ι, ι_p₀ := ι_p₀, ι_p₁ := ι_p₁ }) →
            motive t