物理

模态HoTT

模态同伦类型论，如错误欢迎指正

为了统一语言方便表述，这里会用大部分应该都是代码语言

首先涉猎的内容非常广，有：数学，物理学，哲学，逻辑学，人工智能(AI)，计算机，生物学，语言学

第一章   马丁-洛夫类型论

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

构造主义数学：证明必须提供明确的构造

直觉主义逻辑：真理通过感觉建立

证明与程序：数学证明可以看作计算程序

基本思想描述：一个数学陈述A为真，当且仅当我可以构造他的证明，一个证明对象p具有类型A，写作p：A

类型论的基本构架：判断形式：A（A是一个类型），A≡B（即A和B是一个相等的类型），a：A（a是类型A的一个项），a≡b：A（a和b是类型A的相等项）

上下文管理:推导规则总是在某个上下文中进行

Γ ctx （Γ是一个良构上下文），那么空上下文（记为•也是良构的）

如果Γ是一个良构的上下文，并且在上下文Γ下，A是一个类型，（即Γ∣－A type），那么将新变量x声明为类型A后形成的扩展上下文Γ，x：A也是良构的

函数类型

非依赖函数类型：形成规则：Γ∣－A type，Γ∣－B type，得Γ∣－A→B type

引入规则（λ-抽象）：Γ，x：A∣－b：B，Γ∣－（λx.b）：A→B

消去规则（函数应用）：Γ∣－f：A→B，Γ∣－a：A，Γ∣－f（a）：B

计算规则（β-规约）：（λx.b）（a）≡b[a／x]

积类型

非依赖积类型：形成规则：Γ∣－A type，Γ∣－B type，Γ∣－A×B type

引入规则（配对）：Γ∣－A type，Γ∣－B type，Γ∣－(a，b）：A×B

消去规则（投影）：Γ∣－p：A×B，Γ∣－p：A×B，Γ∣－π₁（p）：A，Γ∣－π₂（p）：B

计算规则：π₁(a，b）≡a，π₂（a，b）≡b

和类型

不相交并和类型：形成规则：Γ∣－A type，Γ∣－B type，Γ∣－A+B type

引入规则：Γ∣－a：A type，Γ∣－b：B type，Γ∣－inl(a)：A+B，Γ∣－inr(b)：A+B

消去规则（情况分析）：Γ∣－s：A+B       Γ，x：A∣－c：C     Γ。y：B，Γ∣－case(s，λx.c，λy.d)：C

计算规则：case(inl(a)，λx.c，λy.d)≡c[a/x],case(inr(b),λx.c,λy.d)≡d[b/y]

举个例子：布尔类型作为和类型：Bool=Unit+Unit，true=inl(tt)，这里假设tt等于Unit，false=inr(tt)

符号函数：Nat+Nat→Bool，λs.inl(tt)，λn.inr(tt))，这里左注入表示正，右注入表示负

自然数类型：形成规则：Nat type；引入规则：Γ ctx    Γ∣－n：Nat zero：Nat，succ（n):Nat

消去规则（递归）：Γ∣－n:Nat Γ∣-a:A   Γ,x:Nat,y:A∣-b:A,Γ∣-rec(n,a,λx.λy,.b):A

计算规则：rec （zero，a,λx.λy.b)≡a,rec(success(n),a,λx.λy.b)≡b[n,rec(n,a,λx.λy.b)/x,y]

恒等类型：这个类型也是马丁-洛夫类型论最具创新的核心类型之一：形成规则：Γ∣-A type ,Γ∣-a:A.  Γ∣-b:A,Γ∣-Id_A(a,b)type

引入规则（自反性）：Γ∣-a:A,Γ∣-refl(a):Id_A(a,a)

消去规则（路径归纳）：Γ∣-p:Id_A(a,b)      Γ,x:A,y:A,q:Id_A(x,y)∣-C type,Γ∣-d:∏(x:A),C(x,x,refl(x)),Γ∣-J(p,λx.λy.C,λx.d):C[a,b,p/x,y,q]

计算规则：J(reflect(a),λx.λy.λq.C,λx.d)≡d[a/x]

这个东西非常重要，因为它可以表达命题的相等性，作为同伦类型论中路径概念的前身，也支持等式推理和替换

依赖类型：依赖函数类型（∏-类型）：形成规则：Γ∣－A type    Γ,x:A∣-B        type ,Γ∣-∏(x:A).B    type 

引入规则：Γ,x:A∣-b:B,Γ∣-(λx.b):∏(x:A).B

消去规则：Γ∣-f:∏(x:A).B,Γ∣-a:A,Γ∣-f(a):B[a/x]

依赖对类型（Σ-类型）

形成规则：Γ∣-A type      Γ,x:A∣-B   type. Γ∣-Σ(x:A).B    type

引入规则：Γ∣-a:AΓ∣-b:B[a/x],Γ∣-(a,b):Σ(x:A).B

消去规则：Γ∣-p:Σ(x:A).B,Γ∣-π₁(p):A,Γ∣-p::Σ(x:A).B,Γ∣-π₂(p)):;B[π₁(p)/x]

宇宙层级：马丁-洛夫类型论包含一个类型的类型层次：

形成规则：U_i    type

引入规则：A：U_i,A:U_{i+1},典型元素：Nat:U_0;Type:U_1     实际上写作U_1,包含U_0为了避免吉拉尔悖论，宇宙是分层级的

计算性质：马丁-洛夫类型论具有强规范化性质：所有良构的项都会在有限步内规约到规范形式；并保证逻辑一致性；支持计算解释

规约关系如下

(λx.b)(a)→b[a/x],π₁(a,b)→a,π₂(a,b)→b,rec(success(n),a,f)→f(n,rec(n,,a,f))

判断层次结构：马丁-洛夫类型论是一个四层判断系统：

1.预判断

Γ   ctx       (Γ是良构的上下文g）

2.类型形成判断：Γ∣-A    type        (在上下文Γ中，A是一个类型）

3.居留判断：

Γ∣-a:A       (在上下文Γ中，a是类型A的项）

4.定义相等判断：

Γ∣-A≡B   type（在Γ中，A和B是定义相等的类型），Γ∣－a≡b：A（在Γ中，a和b是定义相等的项）

推导规则的形式化表述：

每个推导规则采用推理图即：

J₁      J₂          ...            J_n

............................................(Rule-Name)

             J

这里J_i是前提条件，J是结论，（Rule-Name）是规则名称

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单值公理的范畴语义

3.2单值的计算解释

3.3HIT的通用代数理论

3.4具体HIT的严格构造

3.5同伦层级的归纳定义

3.6集合层级的深入分析

3.7立方类型论初步

3.8路径类型的计算解释

3.9Blakers-Massey定理

3.10序列

3.11数学基础范式

3.12构造主义vs经典数学

3.13同一和结构主义数学

3.14Cubical   Agda的实现

3.15高阶归纳类型的编码

3.16主要技术挑战和未来方向

3.17数学形式化挑战

3.18基础问题

3.19模态运算符的基本哲学

3.20基本模态运算符

3.21可能世界语义学

3.22主要模态系统

3.23直觉主义模态

3.24模态的证明论表述

3.25模态的代数语义

3.36模态的拓扑解释

3.37多模态逻辑

3.38从模态逻辑～模态类型论

3.39模态的认知解释

3.40时间模态逻辑

3.41模态的数学应用

3.42模态的认知论意义

3.43模态逻辑的形式基础

3.44基本模态系统K

3.45系统T：自反模态逻辑

3.46系统D：道义逻辑基础

3.47系统B：对称模态逻辑

3.48系统S4：预序模态逻辑

3.49：等价关系模态逻辑

3.50多模态系统

3.51对应理论

3.52完全性理论

3.53直觉主义模态系统挑战

3.54模态系统元逻辑性质

3.55应用领域

3.56模态逻辑的范畴化表述

3.57系统K深入

3.58模态系统的格论分类

3.59对应理论的深度发展

3.60完全性理论的现代方法

3.61高阶模态系统

3.62直觉模态系统深入

3.63模态系统证明论复杂性

3.64模态系统的代数几何

3.65高阶对应理论

3.67无限维模态逻辑

3.67模态系统的同调代数

3.68模态系统的模型论

3.69模态系统的证明论语义

3.70高阶模态系统

第四章 从模态逻辑到模态类型论

4.1模态类型论

4.2对偶语境方法

4.3模态判断方法

4.4模态类型论的范畴语义

4.5直觉主义模态类型论

4.6模态单子方法

4.7依赖模态类型论

4.8计算解释

4.9模态恒等类型

4.10实现技术

4.11一致性与规范化

4.12应用实例

4.13多模态类型论和高阶模态类型论

第5章    模态类型论的两种主要进路

5.1对偶语境方法

5.2模态判断方法

5.3两种方法的范畴语义对比

5.4计算解释的差异

5.5元理论性质对比

5.6表达能力比较

5.7   首先复杂性分析

5.8 混合方法

5.9 应用场景

5.10前沿发展

第六章  必然性模态的深度理论

6.1  必然性模态的范畴语义

6.2必然性模态的证明论语义

6.3必然性模态的代数理论

6.4必然性模态的类型论规则

6.5必然性模态的强度层次

6.6必然性模态的计算解释

6.7  必然性模态的依赖扩展

6.8必然性模态的同伦扩展

6.9必然性模态的元理论

6.10必然性模态的应用

6.11高级必然性模态

第七章 可能性模态的深入

7.1可能性模态的范畴语义

7.2可能性模态的证明论

7.3可能性模态的代数理论

7.4可能性模态的类型论规则

7.5可能性模态的强度层次

7.6可能性模态的计算解释

7.7可能性模态的依赖扩展

7.8可能性模态的同伦扩展

7.9可能性模态元理论

7.10可能性模态的应用

7.11高级可能性模态

7.12可能性与必然性的交互

第八章   模态的同伦解释

8.1类型作为空间的深层对应

8.2模态作为纤维化操作

8.3必然性模态的同伦解释

8.4可能性模态的同伦解释

8.5模态路径的高阶结构

8.6模态单值化公理

8.7模态高阶归纳类型

8.8模态截断

8.9模态覆盖空间理论

8.10模态局部化理论

8.11序列

8.12模态同调论

8.13模态微分几何

8.14模态稳定同伦论

第九章   模态作为纤维化

9.1纤维化的范畴理论

9.2必然性模态的纤维化解释

9.3可能性模态的纤维化解释

9.4模态伴随的纤维化实现

9.5依赖模态的纤维化理论

9.6模态强度的纤维化特征

9.7模态纤维化的同伦理论

9.8高阶模态纤维化

9.9模态纤维化的模型论应用

9.10模态纤维化的计算解释

9.11模态纤维化的代数几何

9.12模态纤维化的物理应用

9.13模态纤维化的实现技术

第十章   模态单值公理

10.1单值化公理的模态扩展

10.2模态等价的概念

10.3必然单值公理

10.4可能单值公理

10.5模态单值的范畴语义

10.6模态单值化的证明论

10.7模态单值化的计算解释

10.8模态单值化的元理论性质

10.9模态单值化的应用

10.10模态单值化变形

10.11模态单值化的实现

10.12模态单值化的哲学思想

第12章 S4模态类型论

12.1S4模态逻辑回顾

12.2   S4模态类型论的语法系统

12.3  S4模态类型论的范畴语义

12.4  S4模态类型论的计算机解释

12.5  S4的依赖扩展

12.6 S4模态单值化

12.7  S4的高等结构

12.8  S4的拓扑语义

12.9 S4的实现技术

12.10  S4的元理论

12.11  S4的应用

12.12  高级S4模态类型论

第十三章 其他主要模态系统

13.1 S5模态类型论

13.2  直觉主义模态系统

13.3  时间模态逻辑

13.4  认知逻辑

13.5 D逻辑

13.6  动态逻辑

13.7 条件逻辑

13.8  概率模态逻辑

13.9  混合逻辑

13.10  多模态逻辑

13.11非正规模态逻辑

13.12量化模态逻辑

13.13  应用领域

13.14实现挑战

第14章 模态在数学基础中的应用

14.1 内部语言和层语义

14.2  模态选择公理

14.3  模态集合论

14.4 模态在范畴论中的应用

14.5  模态同调代数

14.6  模态数论

14.7  模态微分几何

14.8 模态概率论

14.9  模态在计算机科学中的应用

14.10  模态在物理学中的应用

14.11模态在语言学中的应用

14.12  模态在语言学中的应用

14.13  挑战与解决

第15章  计算解释与实现

15.1模态类型论的操作语义

15.2  模态类型论的元理论

15.3  强规范化证明