decomposing-univalence:Agda代码随附论文“分解单价公理”

Agda代码随附论文“分解单价公理” 的代码将本文前面各节中关于将一元性公理分解为其他公理的论证形式化。 主要入口点是 。 的代码形式化了以三次集topos的内部语言执行的构造，以验证新的公理。 主要入口是 。 此开发成功使用Agda 2.5.4进行了类型检查。