proposition: Lemma isaprop_M : isaprop (M B).
proof: Proof. apply invproofirrelevance. intros X Y. apply subtypePath. - exact isaprop_is_final. - exact (M_coalg_eq X Y). Defined.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.Induction.FunctorCoalgebras_legacy UniMath.CategoryTheory.Categories.Type.Core UniMath.Induction.PolynomialFunctors UniMath.Induction.M.Core