Lemma InitialHSET : Initial HSET. Proof. apply (make_Initial emptyHSET). apply make_isInitial; intro a. use tpair. - simpl; intro e; induction e. - abstract (intro f; apply funextfun; intro e; induction e). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Coproducts. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Pushouts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.MoreFoundations.Subtypes.