homotopy.io：一个用于有限展示球面$n$-范畴的证明助手
计算机科学中的逻辑
2024-02-21 v1 范畴论
摘要
我们介绍了证明助手homotopy.io，用于处理有限展示的半严格高阶范畴。该工具在浏览器中运行，具有点选式界面，允许通过图形表示直接操作证明对象。我们描述了用户界面并解释了该工具的实际使用方法。我们还描述了该工具的基本子系统，包括折叠、收缩、展开、类型检查和布局，以及关键实现细节，包括数据结构编码、记忆化和渲染。这些技术创新对于在资源受限的环境中实现良好性能至关重要。
引用
@article{arxiv.2402.13179,
title = {homotopy.io: a proof assistant for finitely-presented globular $n$-categories},
author = {Nathan Corbyn and Lukas Heidemann and Nick Hu and Chiara Sarti and Calin Tataru and Jamie Vicary},
journal= {arXiv preprint arXiv:2402.13179},
year = {2024}
}