Lemma chain_union_rel_initial {X : hSet} {I : UU} {S : I → WOSubset X} (Schain : is_wosubset_chain S) (i:I) (inc := subtype_inc (subtype_union_containedIn S i)) : (∀ s:S i, ∀ t:⋃ Schain, t ≤ inc s ⇒ t ∈ S i)%tosubset. Proof. intros s t le. apply (squash_to_hProp (common_index Schain i t)). intros [j [[ij [com ini]] tinSj]]. set (t' := (pr1 t,,tinSj) : S j). unfold sub_initial in ini. assert (K := ini (pr1 s) (pr1 t') (pr2 s) (pr2 t')); simpl in K. change (t' ≤ subtype_inc ij s → t ∈ S i) in K. apply K; clear K. unfold tosub_order_compat in com. apply (pr2 (tosub_fidelity (chain_union_tosub_le Schain j) t' (subtype_inc ij s))). clear com ini. assert (p : t = subtype_inc (pr1 (chain_union_tosub_le _ j)) t'). { now apply subtypePath_prop. } induction p. assert (q : inc s = subtype_inc (pr1 (chain_union_tosub_le Schain j)) (subtype_inc ij s)). { now apply subtypePath_prop. } induction q. exact le. 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.