Definition tosub_order_compat {X:hSet} {S T : TOSubset X} (le : S ⊆ T) : hProp := ∀ s s' : S, s ≤ s' ⇒ subtype_inc le s ≤ subtype_inc le s'.
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.