{P : Sort u} →
  {B : Type u₁} →
    {inst : CategoryTheory.Bicategory B} →
      {C : Type u₂} →
        {inst_1 : CategoryTheory.Bicategory C} →
          {F : CategoryTheory.OplaxFunctor B C} →
            {t : F.PseudoCore} →
              {B' : Type u₁} →
                {inst' : CategoryTheory.Bicategory B'} →
                  {C' : Type u₂} →
                    {inst'_1 : CategoryTheory.Bicategory C'} →
                      {F' : CategoryTheory.OplaxFunctor B' C'} →
                        {t' : F'.PseudoCore} →
                          B = B' →
                            inst ≍ inst' →
                              C = C' →
                                inst_1 ≍ inst'_1 →
                                  F ≍ F' → t ≍ t' → CategoryTheory.OplaxFunctor.PseudoCore.noConfusionType P t t'