Lemma chain_union_rel_hasSmallest {X : hSet} {I : UU} {S : I → WOSubset X} (chain : is_wosubset_chain S) : hasSmallest (chain_union_rel chain). Proof. intros T t'. apply (squash_to_hProp t'); clear t'; intros [[x i] xinT]. apply (squash_to_hProp i); intros [j xinSj]. induction (ishinh_irrel ( j ,, xinSj ) i). set (T' := (λ s, T (subtype_inc (subtype_union_containedIn S j) s))). assert (t' := hinhpr ((x,,xinSj),,xinT) : ∥ carrier T' ∥); clear x xinSj xinT. assert (min := WOS_hasSmallest (S j) T' t'); clear t'. apply (squash_to_hProp min); clear min; intros [t0 [t0inT' t0min]]. set (t0' := subtype_inc (subtype_union_containedIn S j) t0). apply hinhpr. exists t0'. split. - exact t0inT'. - intros t tinT. apply (hdisj_impl_2 (chain_union_rel_istotal chain _ _)); intro tle. set (q := chain_union_rel_initial chain j t0 t tle). set (t' := (pr1 t,,q) : S j). assert (E : subtype_inc (subtype_union_containedIn S j) t' = t). { now apply subtypePath_prop. } rewrite <- E. unfold t0'. apply (pr2 (chain_union_tosub_le chain j) t0 t'). apply (t0min t'). unfold T'. rewrite E. exact tinT. 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.