>>435
>たとえばラッセルのパラドックスを圏論でどう解決するの？

それは、下記ですね
１）パラドックスをめぐる立場は、大きく論理主義、直観主義、形式主義の３つに分けられる
２）ブラウワー 直観主義 排中律や二重否定除去、数学的構成主義
３）圏論「圏論的論理学は、直観主義的論理のために型理論に基づいて定義された」
です

圏論 Steve Awodeyにも、ちょっと書いてあったよ

(参考)
https://ja.wikipedia.org/wiki/%E6%95%B0%E5%AD%A6%E5%9F%BA%E7%A4%8E%E8%AB%96
数学基礎論
歴史
19世紀末に、ゲオルク・カントルにより、集合が考えられた。集合にもとづいた数学の再整理は大きな成果を生み、数学において欠くべからざる道具となってきた。一方、バートランド・ラッセルは、素朴な集合の取り扱い（内包公理）により「自分自身を要素としない集合全体の”集まり”」も集合とされるが、左記の集合は、それ自身を要素としない時、その時に限り自身を要素とするという矛盾を引き起こすことをラッセルのパラドックスとして指摘した。ここに、数学の基礎付けの問題が発生した。

パラドックスをめぐる立場は、大きく論理主義、直観主義、形式主義の３つに分けられる。
直観主義は、数学的な対象や真理が、精神活動によって直接とらえられるものとする立場で、ブラウワーが提唱した。彼は数学における構成的方法を重視したが、そのため排中律の無制限な使用が不当であると非難した。

https://ja.wikipedia.org/wiki/%E7%9B%B4%E8%A6%B3%E4%B8%BB%E7%BE%A9_(%E6%95%B0%E5%AD%A6%E3%81%AE%E5%93%B2%E5%AD%A6)
直観主義 (数学の哲学)

来歴と評価
これに類する主張は、カントールの集合論に対抗する形でクロネッカーやポアンカレによってもなされていたが、最も明確に表明したのはオランダの位相幾何学者ブラウワーである。ブラウワーの立場に対してポアンカレらの立場は前直観主義と言われることがある。

ブラウワーの主張は感覚的で分かりにくかったが、その後ハイティング等によって整備され、結果的には古典論理から排中律を除いた形で形式化されたものが今日、直観主義論理として受け入れられている。 現代では直観主義論理は、数学の証明は全て構成的に為されなければならないという主張（数学的構成主義）と関連が深いと考えられている

つづく