∀ {R : Type u_1} [inst : CommRing R] (A : AlgCat R),
  CategoryTheory.CategoryStruct.comp
      (AlgCat.ofHom { toFun := id, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ })
      (AlgCat.ofHom { toFun := id, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (AlgCat R)).obj A)