∀ (X : BoolRing),
  BoolAlg.ofHom (BoolRing.Hom.hom (CategoryTheory.CategoryStruct.id X)).asBoolAlg =
    CategoryTheory.CategoryStruct.id { carrier := AsBoolAlg ↑X, str := instBooleanAlgebraAsBoolAlg }