{C : Type u} →
  {P : Sort u_1} →
    {I : Type w} →
      {obj : I → C} →
        {I' : Type w} →
          {obj' : I' → C} → { I := I, obj := obj } = { I := I', obj := obj' } → (I = I' → obj ≍ obj' → P) → P