Definition FilteredColimCoconeSET : ColimCocone d. Proof. use make_ColimCocone. - exact FilteredColimitSET. - exact filtered_cocone. - intros Y cc. use unique_exists. + exact(filtered_cocone_morphism cc). + exact(is_cocone_mor_filtered_cocone_morphism cc). + exact(isaprop_is_cocone_mor filtered_cocone cc). + exact(is_unique_filtered_cocone_morphism cc). Defined.
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.