issmall_issmall_codomain_fibers@{i j | } {X Y : Type@{j}} (f : X -> Y) (sY : IsSmall@{i j} Y) (sF : forall y : Y, IsSmall@{i j} (hfiber f y)) : IsSmall@{i j} X. Proof. nrapply issmall_equiv_issmall. - exact (equiv_fibration_replacement f)^-1%equiv. - apply sigma_closed_issmall; assumption. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.Trunc Basics.Tactics