Lush の...

石けんですね。新宿東口のLushは三階あって結構楽しかった。

食べられないのが残念。

男性にはスーッとするタイプを勧めるのは定番なのか?

locally small

こっちは圏論の話。圏論の本では良く出てくるんですが、

　　locally small とは圏のHom Setが集合なこと

って、何っているんだかさっぱりわかりません。そもそも圏論だと集合論やらないし公理も出てこない。

なんだけど、Agda で圏論の証明をやってると、

　　Hom Set の等号 ≈ には cong がない

ってのに気がつく。cong は congruent 合同なわけですが、

　　cong-≈ : ( x y : Hom A a b ) → ( f : Hom A a b → Hom A a' b' ) → x ≈ y → f x ≈ f y

のこと。Hom Set の等号は関係なので f が関係を保存しない限り、結果が等号になるかどうかはわからない。つまり反例がある。
群の写像があったとしても群の構造を保存しないなら準同型写像にはならないというわけ。圏の対象は群だったりするから。

なんだけど、集合なら

　　cong : ( x y : A ) → ( f : A → B ) → x ≡ y → f x ≡ f y

になります。これは Agda 的には x ≡ y が

data _≡_ {A} : A → A → Set where
refl : {x : A} → x ≡ x

と定義されてるから。つまり「項として単一化されるものが≡として等しい」ってことは、

　　項として同じ正規形を持つなら等しい

ってこと。λ式として記号的に等しいってことでもあるな。ということは、

　　圏論で Set ってのは、λ項の世界のこと

なわけ。なるほどね。Agda のSetであって、集合論のSetではないと。

　　≡←≈ : ( x y : Hom A a b ) → x ≈ y → x ≡ y

があれば、 cong-≈ は cong から作れます。上の逆は ≈ が同値関係なことからでるので。これは上の反例があるのでAgdaでは証明できません。

なので、≡←≈ を仮定して使ってれば locally small を使ってることがわかるわけ。

さらに、何か I : Set があって、

hom→ : Hom A i j → I
hom← : ( f : I ) → Hom A i j
hom-iso : hom← ( hom→ f ) ≈ f
hom-rev : hom→ ( hom← f ) ≡ f

であれば、確かに Hom A は集合だと言えます。正確には「ある集合に isomorphic 」だな。

じゃぁ、どういう局面で locally small と使うかと言うと、

　　cong-≈ を使いたい時
　　Hom Set と集合を対応させる時 (そのまんまやん)

一つは Sets の Completeness つまり Sets でのLimitの存在を示す時。同じだけど、 Limitを equalizer と product から作る時だな。
もう一つは米田レンマを使う時ですね。 フロイドの随伴関手定理は米田レンマを使うので locally small を使います。

これだけかな。

≈ は同値関係なので、 locally smallness は対応する同値類があることに相当します。じゃぁ、同値関係あるのに同値類作れないことってあるの?
選択公理がないと代表元が取れないので同値類を集合として作れない場合があるらしい。やっぱり選択公理お前だったのか。集合論に戻ってきました。

Product in ZF

結局、ZFいじってたんですが、

　　濃度を定義するのに onto-map 上への写像を定義する
　　そのためには写像を集合の関係で定義する

で、結局、pair から ordered pair を定義する羽目に。そこで、pair が間違ってることを発見。

いや、別な公理を使ったのかも。結局、論理式で、

　　λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y )

とするだけなので、どうってことなくて変更もたいしたことなかったんですが...

その後の ordered pair が迷走することに。論理式つまり一階述語論理で記述すると、ほぼ教科書通り。

なのだが、数学の教科書って、

　　省略しまくり

そして、Agda では省略は許されない。といっても大した量ではないんですけどね。

全部教科書通りというわけにもいかなくて、ZF→ZF ではなく Agda→ZF なので、ZFの集合とAgdaのデータ構造を対応させる感じ。

ordered pair はこんな感じ。

　　<_,_> : (x y : OD) → OD
　　< x , y > = (x , x ) , (x , y )

pair を使って表す感じ。普通は {{x},{x,y}} と書く奴です。これを使って、

　　data ord-pair : (p : Ordinal) → Set n where
　　　 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )

　　ZFProduct : OD
　　ZFProduct = record { def = λ x → ord-pair x }

こんな感じに。これで、pair ox oy が < x , y > に対応します。ox は集合 x に対応する順序数。

これで、直積の性質(射影π1,π2とか、uniqueness)とか示せば良いのだが、射影は簡単

　　pi1 : { p : Ordinal } → ord-pair p → Ordinal
　　pi1 ( pair x y) = x

そのものだ。constructor も普通。introduction とかいう奴ですね。

　　p-iso1 : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >
　　p-iso1 {ox} {oy} = pair ox oy

ところが、uniquness (elimination)がわからない。わかってみれば簡単なんだけど。

　　p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
　　p-iso {x} p = ord≡→≡ (lemma p) where
　　 　　lemma : { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
　　 　　lemma (pair ox oy) = refl

data の定義が uniqness つまり、 p ≡ od→ord ( < ord→od x , ord→od y > ) を要求してる。そういえば、

　　data ord-pair : (p : Ordinal) → Set n where
　　　 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )

だからな。でも証明の項は、

　　 　　lemma (pair ox oy) = refl

refl は x ≡ x のconstructorだけど。pair の型の unification でそうなるんだけど、気づいたのは4日目の飛行機の中でした。

まぁ、そんなもの。分かんない時は、どんどん横道にそれちゃうんだよな。ま、わからない時には refl って書くのがAgdaだが。

残りは面倒なので気が向いた時にでも。

果実園リーべル

まぁ、fj 同窓会なのかな。新宿だなと思って副都心線で。

　　新宿三丁目で降りて、地図を見ると「明治神宮の裏の渋谷区役所のところ」

あれとは思ったんですが、取りあえず、そっちに。区役所しかない。案内のお姉さんに相談したところ...

　　代々木三丁目はもっと新宿の方

げ。で、もう一回クリックすると新宿の方に。くそ〜 おそらくは移転前のとかが地図に残ってる。

ところが、その辺って駅まで遠い... なんかコミュニティバスがあるので乗ったのですが、

　　山手線の内側まで廻ってから、ハチ公前

おかげで、30分遅刻。

おかげで、ふぢーネーネーとゲーセンで遊べて面白かったです。CHUNITHM っていう奴。僕は苦手なんですが。

　　なんか 1000 combo とか飛ばしてる兄ちゃんを目撃しました

実家のリフォーム

壁と床の張替、一階二階のトイレの更新、浴室の棚の更新ですが、

　　見た目、まったく変わらない

俊子の方針で、少し色あせた、そのままの色で更新したみたい。

どちらかと言えば怪しくなってる風呂と湯沸かし器をなんとかして欲しい気もする。最近、浴室に手すり欲しい気もするし。

まぁ、お好きにどうぞというところですね。母の面倒見てもらってるので頭は上がりませんよ。

Gris

画面の綺麗な iPhone のゲーム(600円)。なんだけど、

　　アクション系

つまり、結構難しい。なんか飛び移れなくて。プレイ動画を見たら高さが倍くらい違う。それは無理。

しばらくやって判明したんですが、

　　double tap ではなくて、途中でぐっと押し込むような感じ

3Dではないんですが。先に進めると、二段ジャンプできるようにもなる。そんなこんなで、

　　指がつるゲーム

でした。まだ、上がってません。プレイ動画を見るだけでも楽しいかも。そっちがメインなのかもな。

いつもの習志野

介護施設にいる母の妹ですが、末の妹夫婦に車で送ってもらいました。

　　高速はがらがら

人が年老いていくのを見るのはつらいものだけど、昔、良くしてくれた思い出があるからな。

今回は成美おばさんの反応は前回と同じような感じだったんだけど、母が積極的に声をかけていた。

なんか張ってあった「上を向いて歩こう」を歌ってたし。そんなわけでは母はご機嫌でした。

デーサービスでも歌うたったりとかしてるのかな。少し母のデーサービスの現場も見れました。

お見舞いだけど、結構、エネルギーがいるもの。一緒にいくのが良いかな。

お休みなので ingress

いや、休みでなくてもやりますが。一昨日は昼間は、

　　池袋から中野まで関東バスで

あと中野のモール。今日は、

　　東池袋から都電で三ノ輪橋まで行って都営バスで戻ってくる

予定だったんですが、途中、飛鳥山が白ポなのを発見したので途中下車。そのまま、予定通り廻りました。

三ノ輪橋でバス停さがすのに手間取ったけど。ちゃんとぐぐれよ。

既に歩いてるところが大半ですが、飛鳥山公園は初めてだな。線路沿いから登る道とか、ケーブルかーとか面白い。

今日一日で200グリフハックポイント取れて500まで行きました。千は、まぁ、頑張らない予定です。火曜日までだっけ。

なんとなく都営一日券買ったけど、元は取れてないな。都電170円は安い。

寿司食べ放題

昨日のMeeting、あんまり、良く見てなかったんですが、秋葉原の寿司食べ放題でした。良く見てなかったので、

　　お昼は中野の回転寿司で千円分

だった。三崎口とかそんな名前でしたが、割と良かった。夏の五巻盛り。

僕自身は食べ残しをうるさく言うのはださいとは思っていて、外食とかどうせ量多いし、ご飯半分と言っても多いから普通に残します。

なのだが、おそらく「お寿司いっぱい」ってのをやりたかったんだろうなぁ。まぁ、子供っぽいとは思いますが。(ボケが始まった説もあるが)

3人なのにいきなり60巻とか頼まれてしまって... まぁ、そこそこがんばったんですが、そこで追加を頼むのか。本気ですか。

　　まぁ、でも、そこで止めたりはしません

残った分は罰金取られてましたが(他人事)、まぁ、1巻100円だったが少し負けてくれたみたいです。寿司は、まぁ、食べ放題だから、そんなものでしょう。

その後も行きつけの店によったりBarに寄ったりしたので、ちょっと今日は二日酔い気味です。

お土産はまだ開けてないんですが、明日かな。

NiftyServe

この入門パック5000円くらいしたらしい。でも、もしかすると、そんなものは要らなかったのかも。

社会人になってから入ったので、

　　NetNews に接続して使ってた

つまり、Perl script で NiftyServe から記事を取ってニュースサーバに流して、ニュースサーバ側の投稿をNiftyに流す方式。

そういうことはするなって規約にあったけど、まぁ、個人で読むにはどんな風に読んでもね。

　　BBSのUIは最低

だったし、trn/mnews/mew 辺りの軽快さは素晴らしかった。BBS browserもいろいろあったんだけど。

　fj.rec.sports.sumo
　a Kobayashi Toshiharu 1 栃ノ心
　b Kobayashi Toshiharu 1 逸ノ城

まだ書いている人がいるのが謎い。

つばめ

東工大のTubame 3.0を見てきました。夏休みとか関係なくフル稼働してたみたい。意外にコンパクトで後ろの方がかなり空いてる．

最近は床は直置きで天井に配線するんですね。でも、

後ろの方にある過去のつばめたちが...

　　廃墟っぽくて良い

もちろん稼働してないので超静か。ちょっと焼けたコンデンサの匂いがする。稼働させれば電気代かかるし。合わせて動かそうと言う話もあったらしい。

vSphere とか Nutanix とか KVM とか PBS とかの話もいろいろ聞けました。大川さんありがとうございました。

天気の子

ようやっと見てきました。

東京で Ingress で廻ったところが全部出てくるような感じ。自分は必ず傘を持って出る雨男なので、まぁ、面白かったです。

大人の頼りなさというか、可能性のある子供に好きにさせてやれない想像力のなさとか、社会の許容度の低さとか、そんなのを感じたかな。

もう一回見るかどうかは微妙。エロげっぽさはそんなに感じませんでした。そんなにやってないしな。

暴露試験

自分が沖縄に来た時からあるやつです。新棟の工事で移転。沖縄の太陽と台風に耐えて偉い。

いや、倒れていた時もあったような。細かい奴の方はどこにあるかはわかりませんでした。

2008年と2019年だな。同じ角度でないのが残念だが。

けむりのひやし

池袋に来ると愛用してる燻製とラーメンの店。となりのお客さんは昼間っからビール

　　僕は我慢したのに!

風呂の追い焚きはやっぱりだめでした。この時期は水風呂で良いんだよな。

夏の東京は昼間のIngressは無理だな。誰だよ、東京で夏にオリンピックやるとか言い出したの...

実家の様子

最近は母は一階で寝るようになったのか。階段使わない分、足腰は弱ったかも。自分で歩けるうちはなんとか...

お風呂のスイッチを入れるとなんかお湯が出てくる。なおったかと期待しましたが、

　　10cm貯まった所でギブアップ

あぁ、そうですか。まぁ、手動で入れれば良いし、追い焚きはできてるし。

でも、なんか二階のトイレは修理されたようだ。

2階のクーラーも怪しいですが、一応、つめたい風は出る。しばらく廻していたら夜には冷えたみたい。天井のコンクリの蓄熱がな。

この手のは入れっ放しでないとだめ。

それよりかびくささがな〜 しばらく人が住んでないとこんなものか。

大東寿司とビール

空港で投稿しろよって感じですが。

那覇羽田なので特に問題なく。台風の目の上を飛んで来ました。那覇の出発階は混み混みでしたが、ゲートはがらがら。そんなもの。

東京は台風の影響か、思ったより涼しいかな。

LLVM update

開発versionをおいかけているわけですが、久しぶり。といっても、

　　Mojave でコンパイル環境が...

どうも、brew でinstallした clang ならコンパイルできる説があるらしい。

32bit のcompile環境をいきなり消すのは酷いよな...

適当に merge しましたが、コンパイルする勇気までは出ず。気が向いたらやってると思います。

なんか、CMakeList.txt を見ると MajorVersion 10 とか書いてあるが...

8/15 - 8/29

東京にいます。特に予定なし。qemu いじりたいが、ZF の続きもやってるかも。

TexLive 2019 は 3.9GBもあるのか。yomitan に置いてあるので、学科内なら有線LANなら1分半で取ってこれます。

FreeMind

まだ使ってるんですけどね。2016 からメンテされてないらしい。

Mojave に上げたのでばっちり動かない

　　ls /Library/Java/JavaVirtualMachines で JDK を確認

/Applications/FreeMind.app/Contents/Info.plist の中の

　　<key>JVMRuntime</key>
　　<string>jdk1.8.0_131.jdk</string>

をそれになおす。さらに、

cd /Applications/FreeMind.app/Contents/PlugIns
ln -s /Library/Java/JavaVirtualMachines/jdk1.8.0_131.jdk .

としたら動きました。

ちょっと、ソースを見てみたんですが、ant + Eclipse template で 10万行ある。で、

　　Eclipse template で生成されるソースがある (Plugin とか)

なので、結構、難しい感じですね。だから Eclipse はだめだと...

坂田の交差点

新しくできた陸橋に切り替わったのですが、

　　曲がり損ねると西原インターまで行くことに

前田側には行きやすくなったかな。陸橋は歩道もあるみたいなんですが、ゆいレールに降りれる感じではないな。

坂田の交差点がなんとかなるのはだいぶ先のようです。

これ、本当に10月にゆいレールの駅できるの? 駅はできるんでしょうけど、バスターミナルとか駐車場とか影も形もないですが...

バルス!

うちの奥様の戦利品です。

ばっちり食われたVHS

もう一つだけ救いたいVHSがあるんだけど... 食われたのは別なので良いんだけど。

蓋開けて、無理やり取り出すことはできました。

そこら辺にあるVHS recorderを二台くらい試しましたがだめぽいな。もう一台は再生できるんだがノイズが酷い。トラッキング調整したけどだめ。

前に救出した三本の時にやるべきだったが。

まぁ、でも、諦めつくようなものなので良いんだけど。中身が重要と言うわけではないと思う。

OmniGraffle

NEXTSTEPのDiagram!の頃から使ってるわけですけどね。そこそこ高いと言う問題が... あと、

　　そうじゃない、単に簡単な→と□の図が書きたいだけなんだ

的なところがあってなぁ。なんで高機能な方にいってしまうのか。UI毎回変えるのやめて。

昔のMacDrawは良かったよな〜 TeXDraw も少し懐かしいです。

学生に使わせるのに、こちらでライセンスを用意していたんですが、

　　毎年買えない

ってことは5年後には時代遅れに。くそう〜 180ライセンスそこそこ高いのでやめちゃおうかと思ってます。

で、代わりのものだが、

　　自分は OmniGraffle を使い続ける気まんまん

ひどい。

学科では Office 365 が用意されるらしいので

　　PowerPoint

え〜　「それじゃポスタ書けんだろ」う、確かにその通り。

　　LibreOffice の Draw

ってな話が Twitter から。ああ、それもいいかな。

... しばらく、どよどよしてると思いますが、放っておいてください。

https://store.omnigroup.com/edu

ハリーズのおばちゃん

こと智子さんですが、浦添総合病院に入院していたんですが 8/7 の朝に急変し亡なったそうです。

乳がんで入退院を繰り返すような状況だったのですが、7/20に会ってハリーズのメニューのデザインとかを話していただけに驚き。

2005年くらいから、研究室のゼミはハリーズと一緒みたいな感じだったので、というか、

　　うちの研究室はハリーズのカレーで駆動されている

からなぁ。お店はネーネー達がやってくれてますが、いろいろあるらしい。なんだかんだ、

　　飲食店は儲からないから、やってる人のモティベーションに頼る

ところが大きいと思う。最後の最後まで前向きな人だったことは確か。卒業ハリーズの時のこととか思い出すな。

告別式とかはやらないそうです。僕も那覇で酒のみながら送ることにします。

昨日今日とハリーズに行ってこれなので「呼ばれたんじゃないの?」とか言われました。

自分の残り時間の短さ、あるいは、まだ卒業できない徳の積み切れなさとかを感じます。がんばっている人ほど早く逝ってしまうのか。

悲しいけど、16年もハリーズをありがとう。そういう気持ちです。直前まで仕事している、僕もそういう生き方でありたい。

また鞄が壊れた

まぁ、そうかなと思ったんですが、紐の方の金具が真っ二つ。

でも、これは前にもやったことがある。肩紐は長いので、取っ手のところに結びつければ良い。

この取っ手は妙に丈夫。

沖縄のバスの乗り換え

いくつかくそなのを見かけたので、書き留めておきます。

我如古の上り。乗ってくる若い子が「泊高橋」というので運転手が「行きません」という。いや、90番なので確かに行かないけど。 国際通りまで行くから乗った方が良いとか言えないのかな。もしかすると、まだ、あるのかと思ったが調べたら終バス。

長田の志真志向け。病院行きたいという人が結構いる。反対側は遠回り。そして、最近は、97でも琉大で下ろされてしまう。なので、 琉大まで乗った方が良い(いや、乗り換え券出せよ)と思うが...

長田の志真志向け。南上原行きたいという子供。運転手は反対側だというのだが、琉大で下ろされると言う問題が。志真志ハイツまで乗って 乗り換えが正解なのだが、子供は結局乗らなかった。もっとも南上原だと歩いても同じくらいかも。くそ暑いけど。

中部商業の琉大行乗り換え。時刻表で直前でいく設定になっているバスがあるらしく、97が10分以上遅れれば乗り換えできる。絶対わざとだろ...

美術館前。55と56がほぼ同時にくる。間違えて乗っちゃったよ。乗る時にコンベンション行とか言って。安波茶で曲がって気づくが、同時に来てるのでどうしようもなく。

団子運転はなんとかして欲しいです...

Photos crash on Mojave

Photos は Apple のappの中でも

　　クソ中のくそ

なので落ちても、不思議でもなんでもないです。

何回が落ちたので、~/Picture の下の library を移動して空で上げてみるんだが、

　　昔のを見に行くようだ

移動したのに?

~/Library に変なものがあるんだろうと見当を付けて、

　　find ~/Library -name '*Photos*'

すると、だめそうなものがぞろぞろと。

/Users/kono/Library/Containers/com.apple.Photos/Data/Library/Caches/Photos/Mondrian/Collections/Photos_Cache.noindex/78288A0FEC306A00AFF560FC7F7697D0.PhotosCacheFile
/Users/kono/Library/Containers/com.apple.Photos/Data/Library/Caches/Photos/Mondrian/Collections/Photos_Cache.noindex/886FF8F23AF68155C9849C144494EF9A.PhotosCacheFile

なんだこれ。

　 rm -rf ~/Library/Containers/*Photos*'

ばっさり rm。

これで、立ち上がりました。自分のくそぐらい自分で始末しろってなところですね。

Ingress First Saturday

今週も ingress event。 豊見城ちゅらさんビーチでした。

Lv12の途中でキリ番くらいしかないなと思ってたんですが、

　　レゾ差ししたら、ちょうど白ポの時だった

を食らって失敗しました。あと500なんだから、敵ぽハックとかリチャージとかあるだろ。FS中はそういうのがな。

あとは、ビーチでのんびりしてました。夕方は風があったので割と涼しかったな。

Mojave

来月には Catalina 出る説もあるんですが... なんとなく。Catalina も様子見かも。

特に問題なく、動いているんですが、

　　Xcode が入らない

/Library/Updateを消すとか、/Application/Xode.app をrenameするとか。でも、

　　/Applicateion/Xocde.app

にはできてるじゃん。

ってことは、App Store のバグか。

LLVM/gcc は brew から入れれれば良い説があるらしい。

% /usr/local/opt/llvm/bin/clang -v
clang version 8.0.0 (tags/RELEASE_800/final)
Target: x86_64-apple-darwin18.7.0
% brew tap ArmMbed/homebrew-formulae
% brew install arm-none-eabi-gcc

なんとかなるのかな〜

選択公理と排中律

集合論シリーズ。いい加減一段落したいんですが...

選択公理と正則公理がうまく分離できなくて、ε-induction という正則公理の別表現が証明できてめでたしだったんですが...

　　なんと、直観主義論理上で集合論を構成すると選択公理から排中律が証明できる

え、え〜という感じなんですが、そもそも、

　　record OD {n : Level}　: Set (suc n) where
　　　field
　　　　def : (x : Ordinal {n} ) → Set n

という順序数定義可能集合で定義しているので、

　　ppp : { n : Level } → { p : Set (suc n) } { a : OD {suc n} } → record { def = λ x → p } ∋ a → p
　　ppp {n} {p} {a} d = d

という感じで要素があれば命題pが成立するODが作れる。というわけで、 p ∨ ( ¬ p )　がp空がでないなら選択公理から要素を取ってきて成立。

そんな感じで証明できました。ってことは、逆の

　　排中律を仮定すると選択公理が出る

ってのを思いつくわけですが。元々、ODの整列性は仮定している(ゲーデル数から出る)ので、整列定理から選択公理を証明すること自体は演習レベル。

なんだが、意外に難い。ε-induction の証明をなぞってとかやっていたんですが、

　　http://tinyurl.com/yy59al29

こんなページを発見。つらつら見てたら、

　　超限帰納法の定義が若干違う

てのを見つけました。いや、要らないとか言って少し条件緩めた記憶がある。osuc x が直後順序数で

　　TransFinite : { ψ : Ordinal → Set }
　　　→ ( ∀ (lx : Nat ) → ψ ordinal lx (Φ lx) )
　　　→ ( ∀ (x : Ordinal )　→ ψ x → ψ ( osuc x )
　　　→　∀ (x : Ordinal)　→ ψ x

だったんですが、Φつまり直前の順序数のない無限順序数が孤立していて変だとは思ってたんだよな。

　　TransFinite : { ψ : Ordinal → Set }
　　　→ ( ∀ (lx : Nat ) → ( (x : Ordinal ) → x o< ordinal lx (Φ lx)　→ ψ x ) → ψ ordinal lx (Φ lx) )
　　　→ ( ∀ (x : Ordinal )　→ ψ x → ψ ( osuc x )
　　　→　∀ (x : Ordinal)　→ ψ x

という感じで、無限順序数より小さい順序数ではψ xが成立ってのを仮定として使えるのが正しい。それがないと無理だとは思っていたんだ。

その治した奴をつかっていて、こんどは、

　　 (∀ x → (A x ∨ B)) →　(∀ x → A x) ∨ B

ってのが欲しくなった。Aが「xより小さいのにψ xは成立しない」で、Bが「見つかりました」なんだけど、量化記号を外に出せないと厳しい。

なんだけど、これって排中律で証明できる、そういえば、排中律を仮定して選択公理を出すのをやっているんだった。というのに気がついて証明できました。

つまり、ODの整列性を持つ直観主義論理上の集合論では、選択公理は排中律と同値というわけですね。

ここ数日、これが頭のたこになっていたので、片付いてうれしいです。