1樓：有勇有萌兔
題主可以看看https://
en.m.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence?wprov=sfla1
是不是和你想的問題相關
2樓：Narc
集合論中，乙個物件可以單獨存在，也可以同時在多個集合裡，兩個集合裡的物件都相同那它們是同乙個集合（有外延性）。
型別論中，物件有且僅有乙個型別，兩個型別中物件一一對應（因為物件只有乙個型別，所以不同型別的物件無法相等所以這裡說一一對應）也不能說它們是同乙個型別（沒外延性）。
hott 裡兩個型別有等價關係（物件一一對應）就可以由 ua 說它們相等，所以上面的區別（外延性）不存在了，但 hott 裡型別和集合還是有區別，型別的物件間的相等關係證明要是唯一的（即 h-level=2），這個型別才是集合。
正是因為有了外延性，hott 能夠準確表達數學裡的各種概念（比如集合），有形式化整個數學的潛力。
集合 h-level=2 是沒有錯的，，概念可能有點混，hlevel 和 n-type，n-truncation 差個 2，我貼個圖吧。
3樓：Jason Hu
我從另乙個角度展開回答這個問題吧。
Magma是含有乙個二元函式的代數結構。
可以推導出
Semigroup是在Magma的基礎上加上associativity.
注意，這裡semigroup是magma的基礎上加一條公理定義的，是從magma上擴充套件得來的。這個方法可以繼續下去。
Monoid在semigroup假設乙個特殊的element 。
發現規律了沒有？這個遊戲就是加公理，看看到底會產生什麼樣的代數結構。自然數 是monoid的乙個model.
Group在monoid的基礎上加上inverse。
有意思的是自然數 不是乙個group的model。因為你沒法定義自然數的inverse。但是整數 是group，自然也是乙個monoid。
從這裡，你可以看出，隨著公理的增加，可以符合的model是越來越少的。
Abelian group是在group的基礎上加上commutativity。
整數 是乙個abelian group。但是不是所有的group都是abelian。比方說乙個dihedral group 就不是abelian。model又少了。
簡單地說，axiomatic system的方法，就是在乙個限定的邏輯系統裡通過疊加公理來限定符合公理的模型。ZFC雖然很複雜，百變不離其終，道理是一樣的。所以，就算你不了解set theory，你也會聽到很多標準公理以外的公理，而set theorist之間會爭論到底哪個公理才是對的。
比方說continuum hypothesis(CH), generalized continuum hypothesis(GCH), axiom of determinacy(AD), axiom of constructibility, etc。
type theory和set theory最不一樣的地方是，type theory是一步到位的。type theory裡研究的，是每個不同的type。在metatheory，每個type必然包含下面3種rule（另外後2種可選）。
formation rule。規定這個type在什麼時候合法。
introduction rule。規定這個type的element是怎麼被構造的。
elimination rule。規定這個type的element是怎麼被使用的。
computation rule（可選）。規定這個type的element在計算上的行為。
uniqueness rule（可選）。規定這個type的element各自是唯一的。
用自然數舉例，自然數是通過0和S構造的。
formation rule一般來說都很無聊:
introduction rule限定兩個constructor:
elimination rule麻煩一些，規定怎麼用自然數:
computation rule規定 怎麼參與計算。
uniqueness rule說的是eliminate後再construct的值和原來是相同的。
type theory學習的是不同的型別構造方法。比方說MLTT定義了W和M。然後(co)inductive types generalize這兩種型別構造，etc。
type theory是結構化很強的方向，所有的type theory的構造都離不開上面5種rule。
相較於set theory，在type theory上疊加公理是一件很奇怪的事情。因為公理往往是缺乏某些rule。比方說，你可能聽說過functional extensionality。
這個公理是沒有computation rule的。有人依然會在type theory裡疊加公理，是因為那個人只在意邏輯一致性。但我自己是不會這樣做的。
另外我再指出一條set theory和type theory推理的不同。set theory裡，嚴格來講只有deduction，沒有induction，因為induction是公理的結果，是需要先證明的。但是type theory裡，elimination rule就是induction，是內生的，不需要被證明的。
4樓：王旭競
可以，這需要對實體做更清晰的界定和劃分。
型別主要是用以規定物件的組成結構，從這個角度出發，型別體系確實可以視為某些特徵的集合。只是型別體系最終是用來描述實體的，做不到完全純粹用集合來表示。
Alexander Stepanov在《程式設計原本》對這個問題有所論述，並發展提出C++的concepts概念。
醫療器械FDA註冊和510K註冊二者之間是什麼關係，區別是什麼？
GSG綠科檢測 510K 你可以理解為這產品美國認為相對危險，然後註冊就要多花不少錢，流程也很長，技術資料，產品檢測這些都涉及到 普通的醫療器械，屬於510K豁免的，那就簡單多了，一周左右就能註冊下來 威達檢測認證 美國FDA醫療器械產品目錄中共有1700多種。根據風險等級的不同，FDA將醫療器械分...
怎樣在保持童心和穩重成熟二者之間做乙個最好的平衡？
自由的實用主義者 依然像小時候一樣想當個醫生，認為當醫生是為了救病治人，就是童心，或者說赤子之心 不是成天跟人說當醫生該怎麼樣怎麼樣，而是努力從任何途徑吸收知識，以後當個優秀的醫生，就是成熟穩重 至於題主你說的那些，有什麼大不了的？ 烏鴉 看了這個問題挺感悟，大學時也老想來想去。首先，1.我也喜歡多...
敬語助動詞 可以變為 和 ，但二者在用法上有何區別呢，為什麼感覺很少看到有用 的場合？
龐安常 其實兩個現在都挺少見的。日常使用敬語一般用 一般用命令型 表示請求。的話對天皇一家還是經常用的。可能因為這些都是比較古的說法，使用起來有點文縐縐的，所以就不太單獨拿來用，用也是固定形態。 帝京日語宋老師 瀉藥一般來說，尊敬分兩種，一般尊敬和非常尊敬。前者是一般尊敬的變法，也就是把動詞變成被動...