Lemma issurjective_reindex_carrier_union {X I J : UU} (index : I → hsubtype X) (g : J → I) (gsurjective : issurjective g) : issurjective (reindex_carrier_union index g). Proof. intros [x in_union]. use(hinhfun _ in_union). intros [i index_ix]. use make_hfiber. - exists x. use(hinhfun _ (gsurjective i)). intros [j jpath]. exists j. refine(transportb _ (eqtohomot _ x) index_ix). exact(maponpaths index jpath). - 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.