オープンホーン型理論：整合性とギャップを導入した型理論の拡張

本論文は、依存型理論の新しい拡張であるオープンホーン型理論（OHTT）を紹介しています。中心的な革新は、非整合性を表すために、否定とは異なる原始的な判断である「ギャップ」の導入です。これにより、OHTTは、ホモトピー型理論（HoTT）では表現できない障害、特にトポロジーやセマンティクスの分野をモデル化できます。この論文の重要性は、輸送が失敗する微妙な状況を捉える可能性にあり、数学的および計算構造について推論するためのより豊かなフレームワークを提供します。破裂した単体集合とKan複体の使用は、強固な意味論的基盤を提供します。