`{PropResizing} {A : Type@{A}} {R : Lt@{_ R} A} `{IsOrdinal A R} {B : Type@{B}} {Q : Lt@{_ Q} B} `{IsOrdinal B Q} (f : A -> B) {is_simulation : IsSimulation f} (a : A) : Isomorphism ↓(f a) ↓a. Proof. apply isomorphism_inverse. srapply exist. - srapply equiv_adjointify. + intros x. exists (f x.1). apply (equiv_smalltype _)^-1. rapply simulation_is_hom. apply (equiv_smalltype _). exact x.2. + intros x. assert (x_fa : x.1 < f a). { exact ((equiv_smalltype _) x.2). } destruct (simulation_is_minimal f x_fa) as (a' & a'_a & _). exact (a'; (equiv_smalltype _)^-1 a'_a). + cbn. intros x. apply path_sigma_hprop; cbn. transparent assert (x_fa : (x.1 < f a)). { exact (equiv_smalltype _ x.2). } exact (snd (simulation_is_minimal f x_fa).2). + cbn. intros x. apply path_sigma_hprop; cbn. transparent assert (x_a : (x.1 < a)). { exact (equiv_smalltype _ x.2). } apply (injective f). cbn. unfold initial_segment_property. cbn. rewrite eisretr. exact (snd (simulation_is_minimal f (simulation_is_hom f x_a)).2). - cbn. intros [x x_a] [y y_a]; cbn. split. + apply (simulation_is_hom f). + intros fx_fy. destruct (simulation_is_minimal f fx_fy) as (a' & a'_y & p). apply injective in p; try exact _. subst a'. exact a'_y. 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.