Definition kfinstruct_dirprod {X Y : UU} : kfinstruct X -> kfinstruct Y -> kfinstruct (X × Y). Proof. intros f g. set (k := kfinstruct_cardinality f). set (l := kfinstruct_cardinality g). use make_kfinstruct. - exact(k * l). - exact((dirprodf f g) ∘ (invweq (weqfromprodofstn k l))). - apply issurjcomp. + apply issurjectiveweq, weqproperty. + apply issurjective_dirprodf ; 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.