Lemma max_common_initial_is_common_initial {X:hSet} (S T : TOSubset X) : common_initial (max_common_initial S T) S T. Proof. exists (pr1 (max_common_initial_is_sub S T)). exists (pr2 (max_common_initial_is_sub S T)). split. { intros x s M Ss le. apply (squash_to_hProp M); intros [B [Bx [BS [BT [BSi [BTi BST]]]]]]. unfold sub_initial in BSi. apply hinhpr. exists B. split. + apply (BSi x s Bx Ss). now apply (h1'' le). + exact (BS,,BT,,BSi,,BTi,,BST). } split. { intros x t M Tt le. apply (squash_to_hProp M); intros [B [Bx [BS [BT [BSi [BTi BST]]]]]]. unfold sub_initial in BSi. apply hinhpr. exists B. split. + apply (BTi x t Bx Tt). now apply (h1'' le). + exact (BS,,BT,,BSi,,BTi,,BST). } intros x y. split. { intros le. induction x as [x xm], y as [y ym]. apply (squash_to_hProp xm); intros [B [Bx [BS [BT [BSi [BTi BST]]]]]]. apply (squash_to_hProp ym); intros [C [Cy [CS [CT [CSi [CTi CST]]]]]]. assert (Cx : C x). { apply (CSi y x Cy (BS x Bx)). now apply (h1'' le). } assert (Q := pr1 (CST (x,,Cx) (y,,Cy))); simpl in Q. assert (E : subtype_inc CS (x,, Cx) ≤ subtype_inc CS (y,, Cy)). { now apply (h1'' le). } clear le. now apply (h1'' (Q E)). } { intros le. induction x as [x xm], y as [y ym]. apply (squash_to_hProp xm); intros [B [Bx [BS [BT [BSi [BTi BST]]]]]]. apply (squash_to_hProp ym); intros [C [Cy [CS [CT [CSi [CTi CST]]]]]]. assert (Cx : C x). { apply (CTi y x Cy (BT x Bx)). now apply (h1'' le). } assert (Q := pr2 (CST (x,,Cx) (y,,Cy))); simpl in Q. assert (E : subtype_inc CT (x,, Cx) ≤ subtype_inc CT (y,, Cy)). { now apply (h1'' le). } clear le. now apply (h1'' (Q E)). } 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.