1樓：Slow Learner
如果從範疇論角度來說，集合範疇的空集在裡面是initial object, 哪在範疇範疇裡面，我記得initial object是空範疇（就是乙個沒有object的範疇）
(這句話非常可能是錯的，但我確定空集是所有集合組成的範疇的initial object,所以照理來說你只要找到範疇範疇裡的initial object就行了，藍而我對small category和large category的概念不甚清晰，所以所有範疇組成的範疇。。。。我也不太確定是啥 :)）
不知道這個回答能不能讓你滿意，因為這個回答還是從範疇論的角度裡講。。。照理說你要模擬的話，應該用非集合論也非範疇論角度來講集合論和範疇論這兩個理論。。
如果能細緻的定義一下怎麼類似就好了。。。。
因為感覺講空集的特性是subset of 所有的集合；所以你可能要找到乙個型別系統，那個型別系統somehow和所有的型別系統都有關係（哈？真的存在？）；或者就是對乙個特定的型別系統，內部有乙個型別或者term和所有的型別或者term都有關係。
2樓：hhhhhhhhh
既然題主說 「空集是集合論的基礎」 那麼我就假設題主說的是 ZF 集合論了。
在 ZF 集合論中所有的集合都是由比它小的集合構建出來的，也就是說只需要空集這乙個「根本的元素」就能表示出來所有數學 entity。
很不幸，這種 「根本的元素」 在常見的 type theory 中是不存在的。type theory 中每個 type 都會自動帶有一系列的例項。在你說自然數 type 的時候，自然數就是已經設定好了的。
也就是說不像 set theory 中的 entity 全部都是 set（所有 set 都能用空集堆疊出來），type theory 中每乙個 type 的元素會 magically 的存在，解釋這些元素的構成並不是 type theory 研究的問題。
比如有理數 type 中的 2.345 是乙個 value。value 都是自然存在的，而不是用 type 構建的。
所以 type theory 中不存在空集這樣的 「根本的元素」。
但是 type theory 中也有乙個不存在任何 value 的 type 叫做 bottom type。就像空集裡面沒有任何元素一樣。
請問如何入門同倫類型論（HoTT）？
你說的對 先看Homotopy Type Theory Permits Logic of Homotopy Types 找點大餅的感覺 然後學點category theory，教程一大堆自己找然後學點type theory，學一點Haskell 接下來試著用Agda做點證明驗證，教程一大堆自己找 入...
為什麼說型別論裡的所有函式都是「連續」的？
Anqur HoTT 裡頭 types 即 spaces，而 space 一般指的是 topological space。那麼根據書裡的說法，想要各種 homotopy 性質 原話是 We should stress that these spaces are treated purely homo...
集合論與範疇論和topos理論是什麼關係？
Jason Hu 稍微槓一下啊。一般的topos，如Set，由於subobject classifier，因而可能有Choice這種公理，所以其內部語言不一定是intuitionistic type theory。或者說intuitionistic type theory不是乙個complete i...