∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {T : CategoryTheory.Monad C} (X : T.Algebra)
  (s :
    CategoryTheory.Limits.Cofork (CategoryTheory.Monad.FreeCoequalizer.topMap X)
      (CategoryTheory.Monad.FreeCoequalizer.bottomMap X))
  (h₁ : CategoryTheory.CategoryStruct.comp (T.map X.a) s.π.f = CategoryTheory.CategoryStruct.comp (T.μ.app X.A) s.π.f)
  (h₂ :
    CategoryTheory.CategoryStruct.comp (T.map s.π.f) s.pt.a = CategoryTheory.CategoryStruct.comp (T.μ.app X.A) s.π.f),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Monad.beckAlgebraCofork X).π
        { f := CategoryTheory.CategoryStruct.comp (T.η.app (CategoryTheory.Monad.beckAlgebraCofork X).pt.1) s.π.f,
          h := ⋯ } =
      s.π ∧
    ∀
      {m :
        ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj
                (CategoryTheory.Monad.beckAlgebraCofork X).pt).obj
            CategoryTheory.Limits.WalkingParallelPair.one ⟶
          ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj s.pt).obj
            CategoryTheory.Limits.WalkingParallelPair.one},
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Monad.beckAlgebraCofork X).π m = s.π →
        m =
          { f := CategoryTheory.CategoryStruct.comp (T.η.app (CategoryTheory.Monad.beckAlgebraCofork X).pt.1) s.π.f,
            h := ⋯ }