proposition: Lemma isomorphism_to_initial_segment `{PropResizing} `{Univalence} (B : Ordinal@{A _}) : Isomorphism B ↓B.
proof: Proof. srapply exist. - srapply equiv_adjointify. + intros b. exists ↓b. apply equiv_resize_hprop. exists b. reflexivity. + intros [C HC]. eapply (equiv_resize_hprop _)^-1 in HC. exact (bound HC). + cbn. intros [C HC]. apply path_sigma_hprop; cbn. symmetry. apply bound_property. + cbn. intros x. rewrite eissect. reflexivity. - cbn. intros b b'. apply isembedding_initial_segment. Qed.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Colimits.Quotient) HoTT(HSet)