Classical.choice とZFCの選択公理の関係について

[Seasawher]

選択原理は global choiceに相当するらしいので、調べたらnLabとかに詳しく書いてありそう

[Seasawher]

選択原理は，Lean 版選択公理とでも言うべきものです．選択原理は，ある型が空ではないという情報だけから，「魔法のように」具体的な元を構成することができると主張します．

現在の説明だと、数学における選択公理について誤解されてしまいそう。 数学における選択公理、 global choice について説明する。 「lean版の選択公理」という言い方はせずに、「似ている」くらいに止める。