Lemma Initial_wosetfuncat : Initial wosetfuncat. Proof. use make_Initial. - exact empty_woset. - apply make_isInitial; intro a; simpl. use tpair. + exists fromempty. abstract (now split; intros []). + abstract (now intros f; apply wofun_eq, funextfun; intros []). 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.