proposition: Lemma nat_alg_is_preinitial : is_preinitial nat_alg_z.
proof: Proof. intro X; pose (x := pr2 X). pose (x0 := x (true,, fromempty)). pose (xsucc := (λ y, x (false,, λ _, y)) : pr1 X -> pr1 X). refine ((nat_rect _ x0 (λ _, xsucc)),, _). apply make_nat_functor_algebra_mor; split; reflexivity. Defined.
imports: UniMath.Foundations.Preamble UniMath.Foundations.PartA UniMath.Foundations.PartD UniMath.Foundations.UnivalenceAxiom UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Categories.Type.Core UniMath.Induction.FunctorAlgebras_legacy UniMath.Induction.PolynomialFunctors UniMath.Induction.W.Core UniMath.Induction.W.Fibered