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