【文件属性】：
文件名称：Integers
文件大小：47KB
文件格式：ZIP
更新时间：2021-03-17 05:57:39
Coq
同伦类型理论中的等价整数
这是伴随[1]进行形式化的存储库。
该存储库的内容
GrpdHITs/ ：[2]随附的存储库。
Categories/ ：最初尝试直接为ℤh和ℤb创建预Categories/代数。
Prebicategories/ ：与谓词，伪函数和伪变换有关的各种概念，[1]的第4章。
type_prebicat.v ：类型的prebicategory的定义。 [1]的6.1节
signature.v ：多项式代码，路径和同态端点和签名的定义和解释。 [1]的6.2节
Algebra/ ：基于高级归纳类型的签名，根据类型的前二分类构造代数。 [1]的6.3节。
Zh_Zb_sig.v ：ℤh和ℤb的签名。 [1]的6.4节。
WildCategories/ ：野生类别的理论，以至于证明WildCategories/保留初始对象的证据。 [1]的第7章的一部分。
每个
【文件预览】：
Integers-master
----.gitmodules(100B)
----Prebicategories()
--------Unitors.v(4KB)
--------PseudoTransformation.v(8KB)
--------Invertible_2cells.v(7KB)
--------PseudoFunctor.v(13KB)
--------Composition.v(6KB)
--------Algebra.v(2KB)
--------DispPrebicat.v(29KB)
--------FullSub.v(2KB)
--------AddEndpoints.v(6KB)
--------DispDepProd.v(4KB)
--------Projection.v(3KB)
----Categories()
--------point_constructors.v(3KB)
--------total_precat.v(3KB)
--------disp_precat.v(3KB)
--------Zh_paths.v(2KB)
----type_prebicat.v(3KB)
----WildCategories()
--------DispWildCat.v(8KB)
--------Invertible_2cells.v(4KB)
--------Adjunction.v(3KB)
--------Initial.v(1KB)
--------WildNaturalTransformation.v(7KB)
--------WildFunctor.v(5KB)
--------AdjunctionsPreserveInitial.v(2KB)
--------WildCatOfWildCats.v(2KB)
--------WildCat.v(2KB)
--------DispProd.v(2KB)
----Zb_Zh_sig.v(4KB)
----signature.v(12KB)
----.gitignore(525B)
----_CoqProject(929B)
----Algebra()
--------polynomials.v(14KB)
--------endpoints.v(13KB)
--------homotopies.v(10KB)
----README.md(2KB)
----GrpdHITs()