∀ (R : Type u_1) [inst : CommRing R],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id
        ({ obj := fun A => Opposite.op { X := Opposite.op (CommAlgCat.of R ↑A), mon := CommAlgCat.monObjOpOf },
              map := fun {A B} f =>
                Quiver.Hom.op (CategoryTheory.Mon.Hom.mk' (CommAlgCat.ofHom ↑(CommBialgCat.Hom.hom f)).op ⋯ ⋯),
              map_id := ⋯, map_comp := ⋯ }.comp
          { obj := fun A => CommBialgCat.of R ↑(Opposite.unop (Opposite.unop A).X),
            map := fun {A B} f => CommBialgCat.ofHom (BialgHom.ofAlgHom (CommAlgCat.Hom.hom f.unop.hom.unop) ⋯ ⋯),
            map_id := ⋯, map_comp := ⋯ }))
      (CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.id (CommBialgCat R))) =
    CategoryTheory.CategoryStruct.id
      ({ obj := fun A => Opposite.op { X := Opposite.op (CommAlgCat.of R ↑A), mon := CommAlgCat.monObjOpOf },
            map := fun {A B} f =>
              Quiver.Hom.op (CategoryTheory.Mon.Hom.mk' (CommAlgCat.ofHom ↑(CommBialgCat.Hom.hom f)).op ⋯ ⋯),
            map_id := ⋯, map_comp := ⋯ }.comp
        { obj := fun A => CommBialgCat.of R ↑(Opposite.unop (Opposite.unop A).X),
          map := fun {A B} f => CommBialgCat.ofHom (BialgHom.ofAlgHom (CommAlgCat.Hom.hom f.unop.hom.unop) ⋯ ⋯),
          map_id := ⋯, map_comp := ⋯ })