@{i j1 j2 k | i < k, j1 <= k, j2 <= k} (n : nat) {A : Type@{j1}} {B : Type@{j2}} (e : A <~> B) (lsA : IsLocallySmall@{i j1 k} n A) : IsLocallySmall@{i j2 k} n B. Proof. revert A B e lsA. simple_induction n n IHn. - exact @issmall_equiv_issmall. - intros A B e lsA b b'. nrapply IHn. * exact (equiv_ap' (e^-1%equiv) b b')^-1%equiv. * apply lsA. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.Trunc Basics.Tactics