Definition kfinstruct_union {I X : UU} (index : I → hsubtype X) (g : kfinstruct I) (index_finite : ∏ (i : I), kfinstruct (index i)) : kfinstruct (⋃ index). Proof. apply(kfinstruct_from_surjection (reindex_carrier_union index g)). apply issurjective_reindex_carrier_union. apply issurjective_kfinstruct. apply(kfinstruct_from_surjection (indexed_carrier_to_carrier_union (index ∘ g))). apply issurjective_indexed_carrier_to_union. apply kfinstruct_stn_indexed. intro; apply index_finite. 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. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.Combinatorics.KFiniteTypes.