proposition: Lemma equiv_initial_segment_simulation `{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: Proof. apply isomorphism_inverse. srapply exist. - srapply equiv_adjointify. + intros x. exists (f x.1). apply equiv_resize_hprop. rapply simulation_is_hom. apply (equiv_resize_hprop _)^-1. exact x.2. + intros x. assert (x_fa : x.1 < f a). { exact ((equiv_resize_hprop _)^-1 x.2). } destruct (simulation_is_minimal f x_fa) as (a' & a'_a & _). exact (a'; equiv_resize_hprop _ a'_a). + cbn. intros x. apply path_sigma_hprop; cbn. transparent assert (x_fa : (x.1 < f a)). { exact ((equiv_resize_hprop _)^-1 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_resize_hprop _)^-1 x.2). } apply (injective f). cbn. unfold initial_segment_property. cbn. rewrite eissect. 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.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Colimits.Quotient) HoTT(HSet)