{A : Type} `{IsHSet A} {R : Lt A} {mere : is_mere_relation _ R} {B : Type} {Q : Lt B} `{IsOrdinal B Q} (f : A -> B) `{IsInjective _ _ f} {is_simulation : IsSimulation f} : IsOrdinal A R. Proof. constructor. - exact _. - exact _. - intros a a' H1. apply (injective f). apply extensionality. intros b. split. + intros b_fa. refine (Trunc_rec _ (simulation_is_merely_minimal b_fa)). intros [a0 [a0_a <-]]. apply (simulation_is_hom f). apply H1. exact a0_a. + intros b_fa'. refine (Trunc_rec _ (simulation_is_merely_minimal b_fa')). intros [a0 [a0_a' <-]]. apply (simulation_is_hom f). apply H1. exact a0_a'. - intros a. remember (f a) as b eqn: fa_b. revert a fa_b. induction (well_foundedness b) as [b _ IH]. intros a <-. constructor; intros a' a'_a. apply (IH (f a')). + apply (simulation_is_hom f). exact a'_a. + reflexivity. - intros a b c a_b b_c. assert (fa_fc : f a < f c). { transitivity (f b). { apply (simulation_is_hom f). exact a_b. } apply (simulation_is_hom f). exact b_c. } refine (Trunc_rec _ (simulation_is_merely_minimal fa_fc)). intros [a' [a'_c fa'_fa]]. apply (injective f) in fa'_fa. subst a'. exact a'_c. 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.