Definition make_kfinstruct {X : UU} (n : nat) (f : ⟦ n ⟧ -> X) (fsurjective : issurjective f) : kfinstruct X := (n ,, f ,, fsurjective).
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.