Definition kfinstruct_coprod {X Y : UU} : kfinstruct X → kfinstruct Y → kfinstruct (X ⨿ Y). Proof. intros f g. set (n := kfinstruct_cardinality f). set (m := kfinstruct_cardinality g). use make_kfinstruct. - exact(n + m). - exact((coprodf f g) ∘ invweq (weqfromcoprodofstn n m)). - apply issurjcomp. + apply issurjectiveweq. apply weqproperty. + apply issurjective_coprodf ; apply issurjective_kfinstruct. 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.