proposition: Lemma carriers_eq : carrierM = carrierM0.
proof: Proof. apply weqtopaths, carriers_weq. 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