proposition: Lemma iskfinite_singleton {X : UU} (x : X) : iskfinite (singleton x).
proof: Proof. apply kfinstruct_iskfinite. use(make_kfinstruct 1). - exact(λ (_ : ⟦ 1 ⟧), (x ,, hinhpr (idpath x))). - intros [z xz]. use(hinhfun _ xz); intro. use(make_hfiber _ (stnpr 0)). now apply subtypePath_prop. Qed.
imports: UniMath.Foundations.Propositions UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.StandardFiniteSets UniMath.MoreFoundations.Subtypes UniMath.Combinatorics.KFiniteTypes