proposition: Lemma isaprop_W : isaprop (W B).
proof: Proof. apply invproofirrelevance. intros X Y. apply subtypePath. - exact isaprop_is_initial. - exact (W_alg_eq 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