Definition TOSubset_plus_point_rel {X:hSet} (S:TOSubset X) (z:X) (nSz : ¬ S z) : hrel (carrier_subset (subtype_plus S z)). Proof. intros [s i] [t j]. unfold subtype_plus in i,j. change hPropset. use (squash_to_hSet_2' _ _ i j); clear i j. { intros [Ss|ezs] [St|ezt]. { exact (TOSrel S (s,,Ss) (t,,St)). } { exact htrue. } { exact hfalse. } { exact htrue. } } { split. { intros [Ss|ezs] [Ss'|ezs'] [St|ezt]. repeat split. - now induction_hProp Ss Ss'. - reflexivity. - apply fromempty. induction ezs'. exact (nSz Ss). - reflexivity. - apply fromempty. induction ezs. exact (nSz Ss'). - reflexivity. - reflexivity. - reflexivity. } { intros [Ss|ezs] [St|ezt] [St'|ezt']. repeat split. - now induction_hProp St St'. - apply fromempty. induction ezt'. exact (nSz St). - apply fromempty. induction ezt. exact (nSz St'). - reflexivity. - reflexivity. - apply fromempty. induction ezt'. exact (nSz St). - apply fromempty. induction ezt. exact (nSz St'). - 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.