{P : Sort u} →
  {C : Type uC} →
    {inst : CategoryTheory.Category.{uC', uC} C} →
      {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} →
        {P_1 Q : C} →
          {b : CategoryTheory.Limits.BinaryBicone P_1 Q} →
            {t : b.IsBilimit} →
              {C' : Type uC} →
                {inst' : CategoryTheory.Category.{uC', uC} C'} →
                  {inst'_1 : CategoryTheory.Limits.HasZeroMorphisms C'} →
                    {P' Q' : C'} →
                      {b' : CategoryTheory.Limits.BinaryBicone P' Q'} →
                        {t' : b'.IsBilimit} →
                          C = C' →
                            inst ≍ inst' →
                              inst_1 ≍ inst'_1 →
                                P_1 ≍ P' →
                                  Q ≍ Q' →
                                    b ≍ b' →
                                      t ≍ t' → CategoryTheory.Limits.BinaryBicone.IsBilimit.noConfusionType P t t'