Internal language 之用 [math-0011]

這是 An informal introduction to topos theory 的閱讀筆記，Leinster 在這裡說 generalized elements 可以說是 Category 的 internal language。而 set theoretic 裡面使用 element 的論證多半都能改用這樣的語言進行，甚至，不使用 LEM 與 AC 的構造式證明，可以在任意 topos 中使用。

除了在 Generalized element 已經討論過的 product $(x, y)$ ，topos 還有 exponentials $Y^X$ ，equalizer 也可以記為

表示 $X \rightrightarrows Y$ 。

這樣就無需使用大量的 diagram，而是採用數學家已經熟悉的集合式的論證即可。