范畴逻辑和类型论

预备

第1章 纤维范畴论导引

第1.1节 纤维

这真正的第一章从纤维范畴论的基本开始; 其为本书的剩余部分提供了基础. 一个纤维, 或者说纤维范畴, 意在捕获范畴${ℂ}_I$的合集${({ℂ}_I)}_{I\in 𝔹}$的概念, 其于一个基范畴$𝔹$上变动, 这推广了诸如集合族${(X_i)}_{i\in I}$的概念, 其于一个基集或者说指标集$I$上变动. 主要的范畴论例子是

第2章 简单类型论

第3章 等式逻辑

第4章 一阶谓词逻辑

第5章 高阶谓词逻辑

第6章 有效topos

第7章 内范畴论

第8章 多态类型论

第9章 高等纤维范畴论

第10章 一阶依赖类型论

第11章 高阶依赖类型论