Lemma iskfinite_binary_union {X : UU} (A B : hsubtype X) (afinite : iskfinite A) (bfinite : iskfinite B) : iskfinite (A ∪ B). Proof. use(hinhfun2 _ afinite bfinite). intros afinstruct bfinstruct. use make_kfinstruct. - exact(kfinstruct_cardinality afinstruct + kfinstruct_cardinality bfinstruct). - refine(coprod_carrier_binary_union A B ∘ _). refine(coprodf afinstruct bfinstruct ∘ _). apply weqfromcoprodofstn. - apply issurjcomp. apply issurjcomp. * apply issurjectiveweq, isweqinvmap. * apply issurjective_coprodf; apply issurjective_kfinstruct. * exact(issurjective_coprod_carrier_binary_union A B). Qed.
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. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.Combinatorics.KFiniteTypes.