Homotopy Type Theory locally small type > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Definition

Given a universe 𝒰\mathcal{U}, a type AA is locally 𝒰\mathcal{U}-small if for all terms a:Aa:A and b:Ab:A and identity types a= Aba =_A b, there exists a term B:𝒰B:\mathcal{U} and a term p(a,b):(a= Ab)𝒯 𝒰(B)p(a, b):(a =_A b) \cong \mathcal{T}_\mathcal{U}(B).

See also

References

  • Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson, Symmetry book (2021)

Revision on June 16, 2022 at 10:08:38 by Anonymous?. See the history of this page for a list of all contributions to it.