`{ExcludedMiddle} {A : Ordinal} (a b : A) : a < b \/ a = b \/ b < a. Proof. revert b. induction (well_foundedness a) as [a _ IHa]. intros b. induction (well_foundedness b) as [b _ IHb]. destruct (LEM (merely (exists b', b' < b /\ (a = b' \/ a < b')))) as [H1 | H1]; try exact _. - revert H1. rapply Trunc_rec. intros [b' [b'_b Hb']]. revert Hb'. rapply Trunc_rec. intros [a_b' | b'_a]. + apply tr. left. rewrite a_b'. exact b'_b. + apply tr. left. transitivity b'; assumption. - destruct (LEM (merely (exists a', a' < a /\ (a' = b \/ b < a')))) as [H2 | H2]; try exact _. + revert H2. rapply Trunc_rec. intros [a' [a'_a Ha']]. revert Ha'. rapply Trunc_rec. intros [a'_b | b_a']. * apply tr. right. apply tr. right. rewrite <- a'_b. exact a'_a. * apply tr. right. apply tr. right. transitivity a'; assumption. + apply tr. right. apply tr. left. apply extensionality. intros c. split. * intros c_a. apply LEM_to_DNE; try exact _. intros not_c_b. apply H2. apply tr. exists c. split. -- exact c_a. -- refine (Trunc_rec _ (IHa c c_a b)). intros [c_b | H3]. ++ apply Empty_rec. exact (not_c_b c_b). ++ exact H3. * intros c_b. apply LEM_to_DNE; try exact _. intros not_c_a. apply H1. apply tr. exists c. split. -- exact c_b. -- refine (Trunc_rec _ (IHb c c_b)). intros [a_c | H3]. ++ apply tr. right. exact a_c. ++ refine (Trunc_rec _ H3). intros [a_c | c_a]. ** apply tr. left. exact a_c. ** apply tr. right. apply Empty_rec. exact (not_c_a c_a). Qed.
From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Colimits.Quotient. From HoTT Require Import HSet.