∀ {R : Type u_2} [inst : CommRing R] (X : HopfAlgCat R),
  BialgCat.ofHom (HopfAlgCat.Hom.toBialgHom (CategoryTheory.CategoryStruct.id X)) =
    CategoryTheory.CategoryStruct.id (BialgCat.of R X.carrier)