proposition: Lemma chain_union_rel_hasSmallest {X : hSet} {I : UU} {S : I → WOSubset X} (chain : is_wosubset_chain S) : hasSmallest (chain_union_rel chain).
proof: 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.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets