这个项目是在 2012 年偶然开始的，当时 JetBrains 的一个团队正在开发一个基于操作转换（OT）的协作式实时编辑器。在 Coq 校对助手的帮助下，开发和验证了合适的 OT 算法，但由于对应用于现实世界任务的自动证明检查和形式化验证感兴趣，于是成立了一个单独的研究小组。 2015 年，该小组转向开发实验性的 HoTT 语言。

官方网站