islocallysmall_islocallysmall_codomain_fibers@{i j k | i < k, j <= k} (n : nat) {X Y : Type@{j}} (f : X -> Y) (sY : IsLocallySmall@{i j k} n Y) (sF : forall y : Y, IsLocallySmall@{i j k} n (hfiber f y)) : IsLocallySmall@{i j k} n X. Proof. nrapply islocallysmall_equiv_islocallysmall. - exact (equiv_fibration_replacement f)^-1%equiv. - apply sigma_closed_islocallysmall; assumption. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.Trunc Basics.Tactics