Lemma issurjective_indexed_carrier_to_union {X I : UU} (index : I → hsubtype X) : issurjective (indexed_carrier_to_carrier_union index). Proof. intros [x in_union]. use(hinhfun _ in_union). intros [i in_index]. use make_hfiber. - exact(i ,, x ,, in_index). - now apply subtypePath_prop. 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.