【文件属性】：
文件名称：infinity::infinity:Groupoid无限
文件大小：160KB
文件格式：ZIP
更新时间：2021-05-24 00:18:42
cubical-type-theory base-library cubicaltt
组群无穷大
Groupoid Infinity基础库专用于基于同位间隔[0,1]和MLTT为核心的兼容类型检查器。 该库遵循HoTT基础和数学分区：“ Foundations一章涵盖了立方编程语言的基础知识； “ Mathematics一章涵盖了模型和定理的正式数学库。 该库最好与上的HoTT书籍一起阅读。
学分
南达·汤帕（Namdak Tonpa）
亚当
分段故障
尤金·斯莫兰卡（Eugene Smolanka）
安迪·梅尔尼科夫（Andy Melnikov）
丹尼斯·斯托亚诺夫（Denis Stoyanov）
德米特里·阿斯塔波夫（Dmitry Astapov）
【文件预览】：
infinity-master
----src()
--------int.ctt(3KB)
--------category.ctt(12KB)
--------k_theory.ctt(28KB)
--------sigma.ctt(2KB)
--------cwf.ctt(6KB)
--------pushout.ctt(929B)
--------lambek.ctt(1KB)
--------equiv.ctt(7KB)
--------pullback.ctt(4KB)
--------adj.ctt(5KB)
--------csystem.ctt(33KB)
--------pi.ctt(2KB)
--------cat.ctt(7KB)
--------nat.ctt(3KB)
--------seq.ctt(1KB)
--------quot.ctt(7KB)
--------manifold.ctt(338B)
--------maybe_theory.ctt(1KB)
--------logic.ctt(3KB)
--------set.ctt(1KB)
--------cones.ctt(5KB)
--------stream.ctt(485B)
--------quotient.ctt(5KB)
--------list.ctt(3KB)
--------ump.ctt(21KB)
--------functor.ctt(3KB)
--------eq.ctt(113B)
--------hubspokes.ctt(1KB)
--------homotopy.ctt(4KB)
--------process.ctt(2KB)
--------etale.ctt(675B)
--------univ.ctt(6KB)
--------s1.ctt(4KB)
--------sip.ctt(12KB)
--------model.htt(1KB)
--------vector.ctt(390B)
--------bishop.ctt(2KB)
--------pointed.ctt(3KB)
--------hedberg.ctt(1KB)
--------interval.ctt(1KB)
--------bool.ctt(707B)
--------proto.ctt(3KB)
--------iso_pi.ctt(850B)
--------maybe.ctt(1023B)
--------helix.ctt(15KB)
--------list_theory.ctt(2KB)
--------swaptrans.ctt(10KB)
--------iso_sigma.ctt(4KB)
--------prop.ctt(5KB)
--------bundle.ctt(4KB)
--------fun.ctt(14KB)
--------buddhism.ctt(519B)
--------suspension.ctt(2KB)
--------iso.ctt(5KB)
--------maybe_nat.ctt(2KB)
--------infinity.ctt(2KB)
--------algebra.ctt(36KB)
--------infinitesimal.ctt(2KB)
--------homology.ctt(6KB)
--------recursion.ctt(6KB)
--------path.ctt(13KB)
--------trunc.ctt(10KB)
--------complex.ctt(135B)
--------nat_theory.ctt(5KB)
--------control.ctt(4KB)
--------topos.ctt(4KB)
--------cw.ctt(384B)
--------real.ctt(5KB)
--------stream_theory.ctt(5KB)
--------bool_theory.ctt(9KB)
--------em.ctt(2KB)
--------ordinal.ctt(3KB)
--------subtype.ctt(4KB)
--------impredicative.ctt(3KB)
--------retract.ctt(945B)
--------mltt.ctt(4KB)
--------s2.ctt(1KB)
--------join.ctt(4KB)
----doc()
--------img()
--------ctt.syntax(2KB)
----.travis.yml(678B)
----README.md(980B)