Definition kfinite_subtype_union {X I : UU} (index : I -> kfinite_subtype X) (index_finite : isfinite I) : kfinite_subtype X. Proof. use make_kfinite_subtype. - exact(subtype_union index). - abstract(apply(iskfinite_union index index_finite); intro; apply kfinite_subtype_property). 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.