Definition is_colimit_homcocone (comp : is_compact X) : isColimCocone homD (hom X X) homcocone. Proof. use comp. - exact(is_filtered_kfinite_subsets X). - exact(is_colimit_kfinite_subsets X). 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.