Lemma iskfinite_singleton {X : UU} (x : X) : iskfinite (singleton x). 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.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.Combinatorics.KFiniteTypes.