文件名称：doc.HoTT:普通凡人的HoTT
文件大小：582KB
文件格式：ZIP
更新时间：2024-06-13 07:24:26
TeX
HoTT类型 普通凡人的同型类型理论。 地位 当前，该文档包括（ ）的简介和第一章，以及一部分注释。 HoTT图书是根据知识共享署名-相同方式共享3.0一样的非端口许可发行的，因此我假设作者实际上是希望人们不仅阅读它，而且还希望自己做些事情，例如创建派生的作品。 或者，在这种情况下，基于它创建混搭。 观点 HoTT书非常出色，但针对的是相当老练的读者。 大部分数学都困扰着我。 并不是说我对数学不感兴趣； 我只是没有时间去研究它。 因此，我对HoTT书的主要兴趣是作为使用依赖类型进行编程的途径。 关于类型，判断等的更基本的知识。我想我理解（我已经阅读了Martin-Lof的论文以及许多其他相关知识），但是我发现简介和第1章中的某些解释有些模糊。 Web上有很多关于依存类型和直觉类型理论的论文，教程等。 为什么选择HoTT书？ 好吧，一方面，它旨在展示数学的基础；另一方面，它旨在为学生提供
【文件预览】：
doc.HoTT-master
----book()
--------main.tex(9KB)
--------misc.tex(15KB)
--------macros.tex(31KB)
--------equality.tex(10KB)
--------curry-howard.tex(9KB)
--------opt-black-white.tex(791B)
--------hotttype.tex(14KB)
--------preliminaries.tex(130KB)
--------hott-letter.tex(553B)
--------pragmatism.tex(3KB)
--------introduction.tex(55KB)
--------lexicon.tex(227B)
--------opt-letter.tex(4KB)
--------hotttypes.tex(10KB)
--------proofassistants.tex(1KB)
--------semantics.tex(1KB)
--------assertion.tex(11KB)
--------brandom.tex(14KB)
--------logics.tex(802B)
--------math.tex(2KB)
--------proof.tex(18KB)
--------foundations.tex(15KB)
--------types.tex(4KB)
--------references.bib(67KB)
--------hotttype.pdf(367KB)
--------hottlang.tex(3KB)
----LICENSE.md(157B)
----README.md(9KB)
----misc()
--------notation.tex(12KB)
--------ideas.tex(33KB)
--------hottmacros.sty(4KB)
--------equality.tex(88KB)
--------unit.tex(18KB)
--------tlambda.txt(5KB)
--------infinity.txt(9KB)
--------inference.tex(33KB)
--------hottz.tex(3KB)
--------blogs.txt(217B)
--------processes.txt(1KB)
----.gitignore(224B)