Definition chain_union_rel {X : hSet} {I : UU} {S : I → WOSubset X} (chain : is_wosubset_chain S) : hrel (carrier_subset (⋃ (λ i, S i))). Proof. intros x y. change (hPropset). simple refine (squash_to_hSet _ _ (common_index2 chain x y)). - intros [i [s t]]. exact (WOSrel (S i) (pr1 x,,s) (pr1 y,,t)). - intros i j. now apply chain_union_prelim_eq0. Defined.
Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets.