Definition reindex_carrier_union {X : UU} {I J : UU} (index : I → hsubtype X) (g : J → I) : (carrier (⋃ (index ∘ g))) → (carrier (⋃ index)). Proof. apply subtype_inc; intro. use hinhfun. use(fpmap g). 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.