分类类型
Classifying Types
摘要：
在类型论的语言中，同伦理论现象的研究有时被称为“合成同伦理论”。同伦类型论中的同伦理论只是同伦类型论的众多方面之一，同伦类型论还包括集合论语义的研究（同伦类型论模型和集合或范畴的元理论中的单值性），类型论语义学（同伦类型理论的内模）和计算语义学，以及研究同伦类型理论内部语言中的各种问题，这些问题不一定是由同伦理论激发的，或与基于同伦类型理论的形式化数学库的发展相关的问题。本论文是关于综合同伦理论的发展。
英文摘要：
The study of homotopy theoretic phenomena in the language of type theory is sometimes loosely called `synthetic homotopy theory'. Homotopy theory in type theory is only one of the many aspects of homotopy type theory, which also includes the study of the set theoretic semantics (models of homotopy type theory and univalence in a meta-theory of sets or categories), type theoretic semantics (internal models of homotopy type theory), and computational semantics, as well as the study of various questions in the internal language of homotopy type theory which are not necessarily motivated by homotopy theory, or questions related to the development of formalized libraries of mathematics based on homotopy type theory. This thesis concerns the development of synthetic homotopy theory.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
