## Definition ## Given a [[universe]] $\mathcal{U}$, a type $A$ is **essentially $\mathcal{U}$-small** if there exists a term $B:\mathcal{U}$ and a term $p:A \cong \mathcal{T}_\mathcal{U}(B)$. ## See also ## * [[universe]] * [[locally small type]] * [[axiom of replacement]] ## References ## * Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson, [Symmetry book](https://unimath.github.io/SymmetryBook/book.pdf) (2021) category: not redirected to nlab yet