1樓：Jason Hu
稍微槓一下啊。一般的topos，如Set，由於subobject classifier，因而可能有Choice這種公理，所以其內部語言不一定是intuitionistic type theory。（或者說intuitionistic type theory不是乙個complete internal language）
2樓：
眾所周知，範疇論是建立在集合論裡的。從集合論的角度看，範疇論一方面可以提供一種普遍的方法來研究一類數學物件的總體，比如群、環、域這些代數物件的範疇和拓撲空間等幾何物件的範疇，並通過函子和自然變換的概念來談論這些數學物件之間的關係。從這個方面來看，範疇論很像一種廣義的模型論，比如一些代數物件的範疇，它的物件類可以看作是乙個一階理論的所有模型的構成的初等類，態射是模型之間的同態對映，當然這裡可能並不需要形式語言了。
乙個問題是這些某一類數學物件的總體構成的範疇往往都是大範疇（large），這可以通過加強集合論的公理解決（比如新增Grothendieck universe，其存在性等價於存在強不可達基數）另一方面，範疇論可以看作是一些型別論和邏輯系統的代數語義，就像布林代數是經典命題邏輯的代數語義那樣，一些特殊的範疇可以為一階邏輯、高階邏輯，甚至集合論建立代數語義。這樣看，範疇就是一種代數物件，範疇論是對這種代數物件的研究。
自然的，topos也是這樣一種代數物件，其特殊性在於我們可以在其中建立相當一部分的數學，甚至它可以給像集合論這樣的元理論來建立語義，這使得它具備了作為乙個「數學宇宙」的資格。當然topos也可以從其他角度（比如幾何）來解釋，這種對topos的解釋更接近elementary topos。
我們也可以用範疇論或者型別論來做元理論，然後在其中建立集合論以及其他數學，但是範疇論和型別論在描述元數學方面遠不如集合論方便。
型別論和範疇論中有沒有類似集合論中 空集 的概念？
Slow Learner 如果從範疇論角度來說，集合範疇的空集在裡面是initial object,哪在範疇範疇裡面，我記得initial object是空範疇 就是乙個沒有object的範疇 這句話非常可能是錯的，但我確定空集是所有集合組成的範疇的initial object,所以照理來說你只要找...
集合論，數論，能買菜麼？
Newsman For the fourth time on his journey across America,Forrest Gump,gardener from Greenbow,Alabama,is about to cross the Mississippi River again to...
有什麼超簡單集合論入門教材？
Heinrich 對不同人來說簡單的定義不一樣。題主說的 把該講的點點到了的那種 應該是指把 日常數學 要用到幾乎所有集合論都講到吧？我學集合論的讀的是 Kunen 的 Foundation of Mathematics,學完後基本就差不多了 看到基數不再那麼害怕了，形如 線性空間的維度，群的階之類...