`{PropResizing} `{Univalence} (B : Ordinal@{A _}) : Isomorphism B ↓B. Proof. srapply exist. - srapply equiv_adjointify. + intros b. exists ↓b. apply equiv_smalltype. exists b. reflexivity. + intros [C HC]. eapply equiv_smalltype in HC. exact (bound HC). + cbn. intros [C HC]. apply path_sigma_hprop; cbn. symmetry. apply bound_property. + cbn. intros x. rewrite eisretr. reflexivity. - cbn. intros b b'. apply isembedding_initial_segment. 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.