Definition kfinstruct_stn (n : nat) : kfinstruct (⟦ n ⟧). Proof. use make_kfinstruct. - exact n. - exact(idfun (⟦ n ⟧)). - exact(issurjective_idfun (⟦ n ⟧)). Defined.
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.