{V : Type u_2} →
  {inst : Quiver V} →
    {P : Sort u} →
      {toHasReverse : Quiver.HasReverse V} →
        {inv' : ∀ {a b : V} (f : a ⟶ b), Quiver.reverse (Quiver.reverse f) = f} →
          {toHasReverse' : Quiver.HasReverse V} →
            {inv'' : ∀ {a b : V} (f : a ⟶ b), Quiver.reverse (Quiver.reverse f) = f} →
              { toHasReverse := toHasReverse, inv' := inv' } = { toHasReverse := toHasReverse', inv' := inv'' } →
                (toHasReverse ≍ toHasReverse' → P) → P