proposition: Lemma carriers_weq : carrierM ≃ carrierM0.
proof: Proof. apply (weq_iso pr1 (λ m0, m0,, injectM0 m0)). - intros [m H]. cbn. apply maponpaths, ishinh_irrel. - intros x. cbn. 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