Sort u →
  {C : Type u₁} →
    [inst : CategoryTheory.Category.{v, u₁} C] →
      CategoryTheory.GlueData C →
        {C' : Type u₁} → [inst' : CategoryTheory.Category.{v, u₁} C'] → CategoryTheory.GlueData C' → Sort u