Lemma Terminal_WOSET : Terminal WOSET. Proof. use make_Terminal. - exact unit_woset. - apply make_isTerminal; intro a. exists (λ _, tt). abstract (simpl; intro f; apply funextfun; intro x; case (f x); apply idpath). 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.