Homotopy Type Theory essentially small type > history (Rev #1)

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 (2021)