`{PropResizing} {ua : Univalence} {C B : Type@{i}} (f : C -> B) : (C -> HProp) -> (B -> HProp). Proof. intros p b. exact (Build_HProp (smalltype (forall a, f a = b -> p a))). Defined.
From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra HSet. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Card. From HoTT.Sets Require Import Ordinals Powers.