proposition: Lemma Terminal_wosetfuncat : Terminal wosetfuncat.
proof: Proof. use make_Terminal. + exact unit_woset. + apply make_isTerminal; intro a. use tpair. - exists (λ _, tt). abstract (split; [intros x y H|intros x [] []]; apply (WO_isrefl unit_woset)). - abstract (now intros f; apply wofun_eq, funextfun; intros x; induction (pr1 f x)). 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