proposition: Theorem Wtype_is_W {A: UU} {B: A → UU} (W': Wtype A B) : W B.
proof: Proof. exists (w_algebra W'). apply w_types_are_initial. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.PartA UniMath.Induction.W.Wtypes UniMath.Induction.W.Core UniMath.Induction.FunctorAlgebras_legacy UniMath.Induction.PolynomialFunctors UniMath.Induction.PolynomialAlgebras2Cells UniMath.CategoryTheory.Core.Functors