proposition: Lemma nat_alg_func_is_unique : ∏ X, ∏ (mor : algebra_mor _ nat_alg_z X), pr1 mor = pr1 (nat_alg_is_preinitial X).
proof: Proof. intros X mor. induction X as [X x]; induction mor as [mor is_mor]; cbn in x. cbn in mor. apply funextfun; intros n; induction n; cbn. - unfold is_algebra_mor in is_mor; cbn in mor, is_mor. refine ((eqtohomot is_mor (true,, fromempty)) @ _). apply (maponpaths x). apply nat_functor_arr_true. - refine ((eqtohomot is_mor (false,, _)) @ _); cbn. apply (maponpaths x). unfold polynomial_functor_arr; cbn. apply maponpaths. apply funextsec; intros ttt; induction ttt. apply IHn. 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