建设性的HoTT 关于HoTT的各种建设性解释的说明,包括路径类型,HIT和统一性原则(代替公理,因为它不再是公理!)。 建造 要构建预印本PDF,您需要TeXLive,它是python软件包Pygments ,Agda的最新版本及其立方库。 安装Pygments: pip install Pygments 或者: pip3 install Pygments 在NixOS上安装TeXLive && Pygments: nix-env -iA nixos.python37Packages.pygments nixos.texlive.combined.scheme-full 如果您使用的是非英语版本的Windows,则安装Agda需要额外的步骤: CHCP 65001 然后您按照的说明进行操作。 不幸的是,该项目无法在Windows上构建。 要在Windows上构建此注释