proposition: Lemma simulation_is_minimal {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: 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.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Colimits.Quotient) HoTT(HSet)