{C : Type u} →
  {inst : CategoryTheory.Groupoid C} →
    {P : Sort u_2} →
      {arrows : (c d : C) → Set (c ⟶ d)} →
        {inv : ∀ {c d : C} {p : c ⟶ d}, p ∈ arrows c d → CategoryTheory.Groupoid.inv p ∈ arrows d c} →
          {mul :
              ∀ {c d e : C} {p : c ⟶ d},
                p ∈ arrows c d → ∀ {q : d ⟶ e}, q ∈ arrows d e → CategoryTheory.CategoryStruct.comp p q ∈ arrows c e} →
            {arrows' : (c d : C) → Set (c ⟶ d)} →
              {inv' : ∀ {c d : C} {p : c ⟶ d}, p ∈ arrows' c d → CategoryTheory.Groupoid.inv p ∈ arrows' d c} →
                {mul' :
                    ∀ {c d e : C} {p : c ⟶ d},
                      p ∈ arrows' c d →
                        ∀ {q : d ⟶ e}, q ∈ arrows' d e → CategoryTheory.CategoryStruct.comp p q ∈ arrows' c e} →
                  { arrows := arrows, inv := inv, mul := mul } = { arrows := arrows', inv := inv', mul := mul' } →
                    (arrows ≍ arrows' → P) → P