∀ {M : Type v} [inst : Monoid M] (J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u))
  (a : CategoryTheory.Limits.limit J),
  ↑((CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints J) a) =
    CategoryTheory.Limits.limit.π J (CategoryTheory.SingleObj.star M) a