{P : Sort u_1} →
  {R : Type u} →
    {A : Type v} →
      {inst : CommSemiring R} →
        {inst_1 : Semiring A} →
          {t : Bialgebra R A} →
            {R' : Type u} →
              {A' : Type v} →
                {inst' : CommSemiring R'} →
                  {inst'_1 : Semiring A'} →
                    {t' : Bialgebra R' A'} →
                      R = R' → A = A' → inst ≍ inst' → inst_1 ≍ inst'_1 → t ≍ t' → Bialgebra.noConfusionType P t t'