fact: Definition make_kfinstruct {X : UU} (n : nat) (f : ⟦ n ⟧ -> X) (fsurjective : issurjective f) : kfinstruct X := (n ,, f ,, fsurjective).
imports: UniMath.Foundations.Propositions UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.StandardFiniteSets