proposition: Lemma W_carriers_eq : ∏ X Y : W B, (alg_carrier _ X) = (alg_carrier _ Y).
proof: Proof. exact (fun X Y => weqtopaths (W_carriers_iso X Y)). Defined.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.Induction.FunctorAlgebras_legacy UniMath.Induction.PolynomialFunctors UniMath.Induction.W.Core