【文件属性】：
文件名称：cubical, 在多维集中，Univalence的实现.zip
文件大小：79KB
文件格式：ZIP
更新时间：2022-10-30 02:35:11
开源
cubical, 在多维集中，Univalence的实现 立方体for实现一种实验简单型检查器，用univalence实现类型理论，具有闭合术语的评估器。安装要安装立方体，需要使用working和 Cabal 安装。 要构建cubical到主目录并执行cabal install只生成(
【文件预览】：
cubical-master
----cubical.cabal(1KB)
----CTT.hs(26KB)
----TODO(761B)
----LICENSE(1KB)
----Exp.cf(2KB)
----Setup.hs(586B)
----cubical.el(2KB)
----Concrete.hs(10KB)
----Tests.hs(4KB)
----examples()
--------mutual.cub(391B)
--------spector.cub(2KB)
--------swap.cub(4KB)
--------finite.cub(7KB)
--------primitives.cub(3KB)
--------epi.cub(2KB)
--------contr.cub(4KB)
--------axChoice.cub(1KB)
--------cong.cub(3KB)
--------gradLemma.cub(3KB)
--------turn.cub(1KB)
--------univalence.cub(4KB)
--------equivTotal.cub(5KB)
--------swapDisc.cub(6KB)
--------hedberg.cub(2KB)
--------function.cub(2KB)
--------curry.cub(2KB)
--------testInh.cub(1KB)
--------elimEquiv.cub(2KB)
--------involutive.cub(2KB)
--------BoolEqBool.cub(3KB)
--------exists.cub(528B)
--------subset.cub(4KB)
--------heterogeneous.cub(3KB)
--------helix.cub(2KB)
--------lemId.cub(5KB)
--------integer.cub(1009B)
--------nIso.cub(5KB)
--------prelude.cub(10KB)
--------set.cub(2KB)
--------quotient.cub(4KB)
--------equivProp.cub(443B)
--------equivSet.cub(908B)
--------UnotSet.cub(909B)
--------interval.cub(332B)
--------omega.cub(4KB)
--------description.cub(886B)
--------binnat.cub(8KB)
--------Kraus.cub(1KB)
--------swapDisc_old.cub(6KB)
--------opacity_fail.cub(220B)
--------opacity.cub(164B)
----.gitignore(28B)
----Makefile(438B)
----Eval.hs(34KB)
----README.md(10KB)
----Main.hs(6KB)
----notes()
--------allprim.txt(2KB)
----Pretty.hs(711B)
----TypeChecker.hs(7KB)