Definition kfinstruct_stn_indexed {n : nat} (P : ⟦ n ⟧ → UU) (index : ∏ (k : ⟦ n ⟧), kfinstruct (P k)) : kfinstruct (∑ (k : ⟦ n ⟧), P k). Proof. set (J := λ (j : ⟦ n ⟧), kfinstruct_cardinality (index j)). use(kfinstruct_from_surjection (X:=∑ (k : ⟦n⟧), ⟦J k⟧)). - apply totalfun, index. - apply issurjective_totalfun. intro; apply issurjective_kfinstruct. - apply(kfinstruct_weqb (weqstnsum1 J)). apply kfinstruct_stn. 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.