Lemma BinCoproductsHSET : BinCoproducts HSET. Proof. intros A B. use make_BinCoproduct. - apply (setcoprod A B). - simpl in *; apply ii1. - simpl in *; intros x; apply (ii2 x). - apply (make_isBinCoproduct _ HSET). intros C f g; simpl in *. use tpair. * exists (sumofmaps f g); abstract (split; apply idpath). * abstract (intros h; apply subtypePath; [ intros x; apply isapropdirprod; apply has_homsets_HSET | destruct h as [t [ht1 ht2]]; simpl; apply funextfun; intro x; rewrite <- ht2, <- ht1; unfold compose; simpl; case x; intros; apply idpath]). 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.