スケッチ #45

【∞-type theory による分類 topos の解析】 HoTT は homotopy を identity type 経由で間接的に扱うため厳密な model は model category に取る必要があるが、∞-type theory は項の間の homotopy を文法(に相当する∞圏)に直接組み込むため ∞-category 自身を model に取れる。よって型理論に対応する ∞-topos や classifying topos を十分強いメタ理論内で解析するには ∞-type theory の方が適する、という主張。coherence theorem の model independent な証明が既に例。 — comm. AI for Math の過去会話より — 初出: 2026-06-18 #∞分類トポス-勉強channel 発言者: haru/57, ¬L 分類: math-research 新規性メモ: 既知 — seedの主張（∞-type theoryはhomotopyを文法に直接組み込むため∞-categoryを直接modelに取れ、coherence theoremのmodel independent証明が既にある）は、Nguyen–Uemuraの∞-type theories (arXiv:2205.00798) とUemuraのnormalization and coherence (arXiv:2212.11764) で展開されている既存プログラムの内容と一致する。classifying ∞-toposへの応用もこのプログラムの明示された動機に含まれる。 関連する芽: 「classifying topos と levels の lattice の ∞ 版」(2026-06-17) / 「∞圏の型理論的形式化と正しい定義」(2026-06-18)