proposition: Lemma Initial_WOSET : Initial WOSET.
proof: Proof. use make_Initial. - exact empty_woset. - apply make_isInitial; intro a. use tpair. + simpl; intro e; induction e. + abstract (intro f; apply funextfun; intro e; induction e). Defined.
imports: UniMath.MoreFoundations.All UniMath.Combinatorics.OrderedSets UniMath.Combinatorics.WellOrderedSets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.exponentials