Definition ColimCoconeHSET : ColimCocone D. Proof. apply (make_ColimCocone _ colimHSET colimCoconeHSET); intros c cc. exists (ColimHSETArrow _ cc). abstract (intro f; apply subtypePath; [ intro; now apply impred; intro i; apply has_homsets_HSET | apply funextfun; intro x; simpl; apply (surjectionisepitosets (setquotpr eqr)); [now apply issurjsetquotpr | now apply pr2 | ]; intro y; destruct y as [u fu]; destruct f as [f Hf]; now apply (toforallpaths _ _ _ (Hf u) fu)]). 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.