resize_ordinal@{i j +} `{PropResizing} (B : Ordinal@{i _}) (C : Type@{j}) (g : C <~> B) : Ordinal@{j _}. Proof. exists C (fun c1 c2 : C => smalltype (g c1 < g c2)). snrapply (isordinal_simulation g). 2, 3, 4, 5: exact _. - apply (istrunc_equiv_istrunc B (equiv_inverse g)). - constructor. + intros a a' a_a'. apply (equiv_smalltype _). exact a_a'. + intros a b b_fa. apply tr. exists (g^-1 b). split. * apply equiv_smalltype. rewrite eisretr. exact b_fa. * apply eisretr. Defined.
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.