Theorem wosub_univalence {X:hSet} (S T : WOSubset X) : (S = T) ≃ (S ≣ T). Proof. simple refine (remakeweq _). { unfold wosub_equal. intermediate_weq (S ╝ T). - apply total2_paths_equiv. - intermediate_weq (∑ e : S ≡ T, S ≼ T ∧ T ≼ S)%prop. + apply weqbandf. * apply hsubtype_univalence. * intro p. induction S as [S v], T as [T w]. simpl in p. induction p. change (v=w ≃ (S,, v ≼ S,, w ∧ S,, w ≼ S,, v)). induction v as [v i], w as [w j]. intermediate_weq (v=w)%type. { apply subtypeInjectivity. change (isPredicate (λ R : hrel (carrier_subset S), isWellOrder R)). intros R. apply propproperty. } apply weqimplimpl. { intros p. induction p. split. { use tpair. { intros s. change (S s → S s). exact (idfun _). } { split. { intros s s' le. exact le. } { intros s t Ss St le. exact St. } } } { use tpair. { intros s. change (S s → S s). exact (idfun _). } { split. { intros s s' le. exact le. } { intros s t Ss St le. exact St. } } } } { simpl. unfold WOSrel. simpl. intros [[a [b _]] [d [e _]]]. assert (triv : ∏ (f:∏ x : X, S x → S x) (x:carrier_subset S), subtype_inc f x = x). { intros f s. apply subtypePath_prop. reflexivity. } apply funextfun; intros s. apply funextfun; intros t. apply hPropUnivalence. { intros le. assert (q := b s t le). rewrite 2 triv in q. exact q. } { intros le. assert (q := e s t le). rewrite 2 triv in q. exact q. } } { apply setproperty. } { apply propproperty. } + apply weqimplimpl. { intros k. split ; apply k. } { intros c. split. { intros x. exact (wosub_le_inc (pr1 c) x,,wosub_le_inc (pr2 c) x). } { exact c. } } { apply propproperty. } { apply propproperty. } } { apply wosub_univalence_map. } { intros e. induction e. reflexivity. } 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.