{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {motive : CategoryTheory.Regular C → Sort u_1} →
      ([toHasFiniteLimits : CategoryTheory.Limits.HasFiniteLimits C] →
          (hasCoequalizer_of_isKernelPair :
              ∀ {X Y Z : C} {f : X ⟶ Y} {g₁ g₂ : Z ⟶ X},
                CategoryTheory.IsKernelPair f g₁ g₂ → CategoryTheory.Limits.HasCoequalizer g₁ g₂) →
            (regularEpiIsStableUnderBaseChange :
                (CategoryTheory.MorphismProperty.regularEpi C).IsStableUnderBaseChange) →
              motive ⋯) →
        (t : CategoryTheory.Regular C) → motive t