## Definition ## Given a universe $\mathcal{U}$, a type $A$ is **locally $\mathcal{U}$-small** if for all terms $a:A$ and $b:A$ and identity types $a =_A b$, there exists a term $B:\mathcal{U}$ and a term $p(a, b):(a =_A b) \cong \mathcal{T}_\mathcal{U}(B)$. ## See also ## * [[universe]] * [[essentially 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