Lemma is_unique_filtered_cocone_morphism {Y : SET} (cc : cocone d Y) (f : SET⟦FilteredColimitSET, Y⟧) (fmor : is_cocone_mor filtered_cocone cc f) : f = filtered_cocone_morphism cc. Proof. apply funextfun; intro x. apply(surjectionisepitosets (setquotpr filtered_eqrel)). - apply issurjsetquotpr. - apply setproperty. - intro b. exact(eqtohomot (fmor b) b). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.QuotientSet. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Filtered. Require Import UniMath.CategoryTheory.Limits.StandardDiagrams. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Combinatorics.KFiniteTypes. Require Import UniMath.Combinatorics.KFiniteSubtypes.