Lemma iskfinite_compact_SET (comp : is_compact X) : iskfinite (X : hSet). 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.
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.