{𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          {R S : 𝒮} →
            {a b : 𝒳} →
              {f : R ⟶ S} →
                {φ : a ⟶ b} →
                  {motive : p.IsCartesian f φ → Sort u} →
                    ([toIsHomLift : p.IsHomLift f φ] →
                        (universal_property :
                            ∀ {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'],
                              ∃! χ,
                                p.IsHomLift (CategoryTheory.CategoryStruct.id R) χ ∧
                                  CategoryTheory.CategoryStruct.comp χ φ = φ') →
                          motive ⋯) →
                      (t : p.IsCartesian f φ) → motive t