{A : Type} {R : Lt A} `{IsOrdinal A R} {B : Type} {Q : Lt B} `{IsOrdinal B Q} (f : A -> B) {is_simulation : IsSimulation f} : forall {a b}, b < f a -> exists a', a' < a /\ f a' = b. Proof. intros a b H1. refine (Trunc_rec _ (simulation_is_merely_minimal H1)). { apply hprop_allpath. intros (a1 & ? & p) (a2 & ? & <-). apply path_sigma_hprop; cbn. apply (injective f). exact p. } exact idmap. 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.