proposition: Lemma iskfinite_compact_SET (comp : is_compact X) : iskfinite (X : hSet).
proof: Proof. set(φinv := is_z_isomorphism_mor (φiso comp)). set(idX := φinv (identity X)). set(idxx := pr12 idX). use(hinhuniv _ idxx). intros cob. set(xᵢ := pr11 cob : kfinite_subtype (X : hSet)). set(f := pr21 cob : _ --> _). apply(iskfinite_from_surjection (coconeIn (kfinite_subsets_cocone X) xᵢ)). - intro y; apply hinhpr. use make_hfiber. + exact(f y). + enough (Q : colimIn (homXX comp) xᵢ f = identity X) by exact(eqtohomot Q y). assert (z : colimIn filtCC xᵢ · φ = colimIn (homXX comp) xᵢ) by apply colimArrowCommutes. apply(pathscomp0 (eqtohomot (!z) f)). change ((colimIn filtCC xᵢ · φ) f) with (φ (colimIn filtCC xᵢ f)). etrans. { apply maponpaths; exact(setquotl0 _ idX cob). } exact(eqtohomot (is_inverse_in_precat2 (φiso comp)) (identity X)). - exact(kfinite_subtype_property xᵢ). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Sets UniMath.MoreFoundations.QuotientSet UniMath.MoreFoundations.Subtypes UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Filtered UniMath.CategoryTheory.Limits.StandardDiagrams UniMath.CategoryTheory.Categories.HSET.Core UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.KFiniteTypes UniMath.Combinatorics.KFiniteSubtypes