Definition max_common_initial {X:hSet} (S T : TOSubset X) : hsubtype X := λ x, ∃ (B : hsubtype X), B x ∧ common_initial B S T.
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.