proposition: Lemma coalgebras_eq : M = M0.
proof: Proof. use total2_paths_f; try apply carriers_eq. apply funextfun. intro m0. rewrite eq1. rewrite eq2. rewrite eq3. cbn. unfold polynomial_functor_obj. rewrite transportf_total2_const. use total2_paths_f; try apply idpath. cbn. apply funextsec. intros b. rewrite <- helper_A. unfold carriers_eq. rewrite weqpath_transport. cbn. rewrite eq_corecM0. apply idpath. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.Induction.FunctorCoalgebras_legacy UniMath.CategoryTheory.Categories.Type.Core UniMath.Induction.PolynomialFunctors UniMath.Induction.M.Core UniMath.Induction.M.Uniqueness