Definition is_colimit_finite_subsets_cocone (X : hSet) : isColimCocone (finite_subsets_diagram X) X (finite_subsets_cocone X). Proof. set (D := finite_subsets_diagram X). intros Y CC. use unique_exists. - exact(λ (x : X), coconeIn CC (finite_singleton x) singleton_point). - intros A. apply funextfun ; intro a. set (a_in_A := finite_singleton_is_in (A : finite_subset X) a). assert(p : dmor D a_in_A · coconeIn CC A = coconeIn CC (finite_singleton (pr1 a))) by apply coconeInCommutes. apply(eqtohomot (!p)). - intro ; apply isaprop_is_cocone_mor. - intros f fmor. apply funextfun ; intro x. exact(eqtohomot (fmor (finite_singleton x)) singleton_point). 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.