Definition kfinstruct_from_surjection {X Y : UU} (g : X → Y) (gsurjective : issurjective g) : kfinstruct X → kfinstruct Y. Proof. intros f. use make_kfinstruct. - exact(kfinstruct_cardinality f). - exact(g ∘ f). - apply issurjcomp. apply issurjective_kfinstruct. exact gsurjective. 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.