定理 #101

【宇宙 U_0 が任意の n に対して n-type でないこと】 HoTT Book 8章で未解決とされる「univalent universe がどんな n に対しても n-type ではない」問題。Alwe は arXiv:1311.4002 の議論が Π_{n:N} K(Z,n) : U_0 を仮定すれば適用でき、higher inductive type があれば U_0 は任意の n に対して n-truncated でないと指摘。 — comm. AI for Math の過去会話より — 初出: 2026-08-02 #（依存）型理論の世界 発言者: hitsujikaip, Alwe 分類: math-research 新規性メモ: 既知 — univalent universe U_n がn-truncatedでないことはKraus–Sattler（arXiv:1311.4002）で証明済みで、higher inductive typeによるEilenberg–MacLane space K(Z,n)（Licata–Finster）を universe に入れれば任意次元の非自明homotopyが得られるという経路も同文献群で議論されている既知の議論。seedの指摘はこの既存の議論の適用にあたる。