text: 在數理邏輯與計算機科學中，同倫型別論是一套旨在於同倫論的大框架下構建內涵型別論語義的理論，尤指Quillen模型範疇和弱分解系統。反而言之，內涵型別論則為同倫理論提供了一套邏輯語言。型別論在絕大多數計算機證明輔助系統中被用作集合論的替代理論，因為集合論的語言難以轉化成計算機證明輔助的形式語言。歷史.1908年，恩斯特·策梅洛提出了被稱作策梅洛-弗蘭克爾集合論的公理化集合論。該理論採用了選擇公理，並作為數學的基礎理論存在，因所有的數學物件均可透過集合論中的概念來解釋。而英國哲學家和邏輯學家伯特蘭·羅素則提出了型別論作為集合論的替代理論。同倫理論在2002年菲爾茲獎獲得者、弗拉基米爾·沃埃沃德斯基關於米爾諾猜想的工作中發揮了重要作用。 沃埃沃德斯基近年來致力於使用一價語義構造新數學基礎的理論體系 UniMath，利用證明輔助工具 Coq 實現。普林斯頓高等研究院從2012-2013年間開始致力於同倫型別論的開發，組織者包括 Steve Awodey、Thierry Coquand 和沃埃沃德斯基等人，吸引了大量數學家和計算機科學家加入。目前該領域亟待解決的問題包括同倫型別論的計算釋義，以及開發新的、能夠更好支援同倫型別論的計算機證明輔助系統。定理證明.數學定理的證明必須遵從邏輯的原則，從公理或已證明的命題推導。而數學基礎研究之終極目的是形式化一切公理，從而使所有數學定理能夠精確、無二義性地推導得出。HoTT 簡化了證明輔助工具將數學證明翻譯到計算機程式語言的步驟，這為計算機檢驗複雜的證明提供了一條簡單易行的途徑。HoTT 引入了一價公理，將同倫論與邏輯命題的等價性聯絡起來。該等價性同樣適用於數學和計算機語言的釋義，它在同倫論中能夠更好地被形式化。Homotopy Type Theory.作為該理論研究的產物，一本開放原始碼的書籍 "Homotopy Type Theory: Univalent Foundations of Mathematics" 得以公開發布。作為一部純數學作品，它非常罕見地在 GitHub 上透過社群合作的方式進行創作，並使用 Creative Commons 授權，從而允許任何人免費下載或選擇購買紙質版。
metadata.dataset: erhwenkuo/wikipedia-zhtw
metadata.title: 同倫型別論
metadata.url: https://zh.wikipedia.org/wiki?curid=4234423