proposition: Lemma Nat_weak_eta (n: Nat) : Nat_rec (C := Nat_as_set) S Z n = n.
proof: Proof. induction n as [n0 H]. use total2_paths_f. - cbn. unfold pre_nat in n0. apply funextsec; intro X. apply funextfun; intro h. apply funextfun; intro x. cbn in H; red in H. apply (H Nat_as_set X Z x S h (fun n => pr1 n X h x)); apply idpath. - cbn. cbn in H; red in H. do 7 (apply funextsec; intro). do 2 (apply funextfun; intro). apply setproperty. Defined.
imports: UniMath.Foundations.Init UniMath.Foundations.Preamble UniMath.Foundations.PartA UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Structures