proposition: Lemma w_types_are_initial : is_initial WW.
proof: Proof. intro EE. exists (w_eval EE). intro kk. apply (! (pq EE kk)). 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