Sort u_1 →
  {B : Type u} →
    [inst : CategoryTheory.Bicategory B] →
      {a b : B} →
        {f g : a ⟶ b} →
          CategoryTheory.BicategoricalCoherence f g →
            {B' : Type u} →
              [inst' : CategoryTheory.Bicategory B'] →
                {a' b' : B'} → {f' g' : a' ⟶ b'} → CategoryTheory.BicategoricalCoherence f' g' → Sort u_1