Lemma Terminal_wosetfuncat : Terminal wosetfuncat. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets. Require Import UniMath.OrderTheory.OrderedSets.WellOrderedSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.exponentials.