IsLocallySmall@{i j k | i < k, j <= k} (n : nat) (X : Type@{j}) : Type@{k} := match n with | 0%nat => IsSmall@{i j} X | S m => forall x y : X, IsLocallySmall m (x = y) end. Existing Class IsLocallySmall. Hint Unfold IsLocallySmall : typeclass_instances. Global Instance ishprop_islocallysmall@{i j k | i < k, j <= k} `{Univalence} (n : nat) (X : Type@{j}) : IsHProp@{k} (IsLocallySmall@{i j k} n X). Proof. revert X; simple_induction n n IHn; exact _. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.Trunc Basics.Tactics