物理

模态HoTT

因为某某原因，帖主准备弱弱的讲一下模态同伦类型论，因为本人只是一个弱弱的高中生

有不懂可以问，如错误欢迎指正

首先涉猎的内容非常广，有：数学，物理学，哲学，逻辑学，生物学，语言学

第一章   马丁-洛夫类型论

1.1哲学和形式系统的基础结构

1.2上下文的形式理论

1.3函数类型的范畴语义视角

1.4依赖类型

1.5恒等类型的同伦解释

1.6归纳类型的一般理论

1.7宇宙层级与类型构造

1.8可判定性与规范化

1.9范畴语义

1.10高阶归纳类型的前置

1.11可计算性理论

1.11.1类型论做为编程语言的元理论

1.11.2强规范化定理

1.11.3类型论的图灵完备性

1.12证明论语义

1.12.1Curry-Howard对应的范畴语义

1.12.2正规化定理的证明论方法

1.12.3焦点化与规范推导

1.13同伦论解释

1.13.1基本形式

1.13.2∞-群胚结构

1.13.3单值公理的深入分析

1.13.4高阶归纳类型的同伦语义

1.13.5截断与同伦层级

1.13.6∞-范畴

1.14综合数学

1.16一致性

第二章   同伦类型论

2.1从类型论到几何直觉

2.1.1传统类型论的局限性

2.1.2单值公理

2.2同伦类型论的核心公理

2.2.1单值化公理

2.2.2高阶归纳类型

2.3路径类型

2.3.1路径作为基本原语

2.3.2高阶路径结构

2.4截断层级：同伦层级的精准控制

2.4.1同伦层级系统

2.4.2截断构造子

2.5高阶归纳类型的举例

2.6单值公理的影响

2.7计算解释新范式

2.8综合数学实现

2.9Agda 

2.10方向

第三章   单值公理的深度分析和模态运算符和主要模态系统

3.1单值公理的范畴语义

正在继续遍制目录