proposition: Lemma M_carriers_eq : ∏ X Y : M B, (coalgebra_ob _ X) = (coalgebra_ob _ Y).
proof: Proof. exact (fun X Y => weqtopaths (M_carriers_iso 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