沖縄のテラス席

まぁ、土砂降りではねぇ

そもそも暑すぎるんだが、沖縄の人はわりと平気らしい

真志喜のバス停にて

ラグナガーデンホテルで、55番のバスに目の前でいかれたので、58号線までゆっくり

真志喜のバス停に近づいたら、なんか、ネーネーが走って追い抜いていく

　もしかして、バスが?!

と思ったら、後ろから来てる。なので、一緒に走って乗れたんですが、

　ネーネーは、それを追い込して、いってしまいました

いったいなんだったんだ。沖縄の人って、あんまり走らないので珍しいとは思ったんだよな

でも、実は、その後ろのバスの方が便利だったんだんだが

今日は別なネーネーにも車から挨拶されたんですが、誰だかはわからず。すみません

Sheaf の記述

「It is easily verifed that Γ p is a sheaf」は終わって、Lを書いている最中。たくさん出てくるのが集合であることを示しているところ

まぁ、最初の Functor のFObjが集合なのは仮定するわけだけど

でも、その 「It is easily verifed that Γ p is a sheaf」なんだが、それまでの準備に 600行。そして、sheaf であることを示すのに200行

そもそも sheaf を示すのに関数三つ作らないとだめで、そのひとつは連続写像であることも示すことになる

まぁでも、Zornの補題の時よりはましな気がする。量的には既におなんじくらいだけど、Zorn の時は、かなり書き直したので

これ、Agda 抜きだと、無理だっただろうなとは思う。覚えてられない感じ

眼鏡

どうもレンズがぼろぼろなので。いつもの眼鏡屋さんにいったら

　前回作ったのは 2015

つまり、10年前らしい。ぱかぱか眼鏡は、少なくなってるらしい

　遠近両用がのびてるから

なるほど。で、遠近両用の方も作ることにしました。できるのは少し先だが

下の近くが見えるところを少し指定できるらしい

まぁ、ノートPCでも、遠近両用では無理な感じね。でも、歩きながら Ingress なら使えるか?!

Functor の有界性

Sheaf の ΓのFunctorとΓ p が Sheaf なのは示せたので、L に取りかかってるんだが、いきなり、これ

Sets への関手が有界なわけはない。なに集合演算を平然としてるんだよ…

いや、圏論の人ってそうなんだよな。「一つ上の階層からみれば集合」。どうせ、そんな感じなんでしょう

ChatGPTと相談しても、有界性を仮定するのがよいらしい。あとで、どうトラブルのかは知らないが

agda の abstract

圏論の Sheaf のところまでできたんですが、一箇所、つなげると agda が止まらなくなるところがある

Chat GPT と相談しながらやってたら、abstract が使えると。いつのまに、そんなものが登場したんだ?

確かに通る。しかも、

{-# OPTIONS --cubical-compatible --safe #-}

と両立する。すごい

値の接続は見ずに、型が一致してれば良いというものらしい

Γm : (p : Obj (top / X)) → {A B : Obj OX} → Hom OX A B → Hom HODSets (Γo p A) (Γo p B)
Γm p {a} {b} b⊆a = record {
　　　　 func = λ qs → & (F→FuncHOD (dfunc p {a} {b} b⊆a qs) )
　　　 ; is-func = Γo-⊆ p {a} {b} b⊆a
　　　 ; func-wld = lem02
　　 } where
　 lem02 : {x y : Ordinal} (ax : odef (Γo p a) x) (ay : odef (Γo p a) y) → x ≡ y
　　　 →　& (F→FuncHOD (dfunc p {a} {b} b⊆a ax)) ≡ & (F→FuncHOD (dfunc p {a} {b} b⊆a ay))
　 lem02　{x} {y} ax ay eq = ==→o≡ ( FuncEQ→HODEQ (dfunc p {a} {b} b⊆a　ax) (dfunc p {a} {b} b⊆a ay) lem10 )　where
　　　　-- lem10 it will take long time to check, so we need abstract
　　　 abstract
　　　　　 lem10 : (z : Ordinal) (az : odef (SObj.s b) z) → FuncEQ (dfunc p {a} {b} b⊆a ax) (dfunc p {a} {b} b⊆a ay) z az
　　　　　 lem10 z az = begin
　　　　　　　Func.func (dfunc p {a} {b} b⊆a ax) az　≡⟨ ΓCont-eq ax ay eq z (b⊆a az) ⟩
　　　　　　　Func.func (dfunc p {a} {b} b⊆a ay) az　∎　where open ≡-Reasoning

牧港の変なカプセル

なんなんだろね

なんで、ここに置いてあるのか

Hail Mary

まぁ、日本ではアベマリアの方がメジャーだよな〜

と大浦天主堂の説明をみて思いました

映画はまだなのか

そういえば、Led Zeppelin の映画は9月かららしい

9月は東京

9/5-10 は東京に行く予定です

親戚まわりとかお墓参りとか

Sheaf は、順調だが、まだ終わってない。先も長いらしい

教科書では it is easily verified で終わってるところです

カップメンのビルの取り壊し

いや、まぁ、いいんだけど

結構、適当な壊し方だな

居酒屋リセット

反順序は、自分の議論で掛順を理解しそうになると「やっぱり、かけ算はどっちでもいいんだ」とリセットしたりするんだよな

やっぱり

　"abc" x "de" = "abcabc"

で、掛順の議論は終わりだろと思う今日この頃。なんか、この単なる文字列関数に文句をつけている人たちがいるみたいね

Sheaf の続き

なんか、ぜんぜんできなくて。で、どうも、Sheaf の定義が違うらしい

Pull back って a b の二つの対象にたいして定義するんだが「任意の a b 全部」って書いてある

a b に対して、pull back が決まるのではなくて「全部の a b 　の組に対して」決まるのか

ところが、それを書こうとすると、任意個の直積を書かないとだめ。Equalizer で書けるとか書いてあるが…

まぁ、pull back をコピペして (a b : I )を引数で入れればいいんだろ?

Lean 4 で書いてあるのもあるっぽい

国保の振込

なんか、また、降ってきて。前のは市税だったが、今度は国保

なんだが、用紙持っていって「自動振込でお願いします」っていったら「できない」

ってどういうこと? どうも、自分の沖銀の支店は浦添にあって宜野湾市の「自動振込用紙がないのでできない」

で「我如古支店ならできる」え〜? そうなの。どうせハンコ忘れたので家に戻ってから、もう一回

でも、次の振込は来年度らしい。今回のは振り込んでしまうので。来年、まだ国保かどうかはわかんないな

自動振込設定がネットからできるようになるとか書いてあったが「最初の一回目には間に合いません」とも書いてあってた

まぁ、作業は終了

郵便でいろいろ送ってくるのやめろ〜とも思う。まあ、最近はメールも読まないが

長崎の階段

まぁ、階段の多い街でさ。この風頭山から降りてくる階段ね

10分くらいで降りれました。まあ、汗はかくけどね

そして、どうでもいい喫茶店

なくなるお店

割と通った花ぐるまは、4月いっぱいで終了。40年間御苦労様でした

恵は今月いっぱいらしい。25年御苦労様でした

牧港ボウルのボウリングキャットは、淳子さんのお店でしたが骨折で再開は未定

安波茶のSon of Sun も閉店

大山の松倉は週末営業のみに

普天間のフランクリンアベニューは、居抜きで別なお店に

飲食店は、なかなか厳しい。もっと補助でてよいと思うんだが

文字列のかけ算による掛順の可視化

「かけ算には元から対称な定義があるに違いない」つまり累加でない定義ってことね。それはない、何故なら

　"abc" x "de" = "abcabc"

という文字列のかけ算を考える。これは「いくつ分」の文字列の文字の数だけ「ひとつ分」の結合を繰り返す文字列演算ね

Pthon で書くと

　def string_multiply(a: str, b: str) -> str:
　 return a * len(b)

こんな感じ。これは、もちろん非可換

　"de" x "abc" = "dedede"

これは長さを見ると自然数のかけ算になっている。この非対称なかけ算が書けるのは、かけ算の定義が、この演算にそった累加だからなわけ

つまり、この非対称な演算を実現する定義だけが許される。つまり対称なかけ算の定義は存在しない。そして、

　この文字列のかけ算で掛順が可視化されている

というわけ。

反論1 「単位ごとの交換なら掛順はない」

5m/s x 2kg =2kg x 5m/s だから掛順はないってやつね。

　5m/s x 2kg =2m/s x 5kg

はどうする? これには単位ごとの交換は使えない

反論2 「文字列の割り算が決まらない」

長さで考えれば割り算も定義できる。別になくてもよいんだどね

　"abc" x ? = "abcabc" の ? の文字列を見つける

これは簡単。2文字の文字列だ

　? x "de" = "abcabc" の ? の文字列を見つける

これは "abc" だ。でも、「 ? x "de" = "......" の ? の文字列を見つける。. はwild card」にしても良い

反論3 「文字コードで変わる」

len の仕様にしたがうだけ。文字列のbyte長でも良い。それでもいやなの?

それは「反順序の強迫観念」に過ぎない。「かけ算はどっちでもいい」と思いたいための禁則ね

反論4 「勝手に作ったものに過ぎない」

　"vvvvv" x "mm"

5m/s x 2kg のことだ。結果は v が10個。10 kg m/s のことね。任意のかけ算をこれで考えてよい

　おはじきで学ぶ算数

をおもいだそう

JR九州の QRコード

この手のものはトラブルの好きなんだが

　　予約のQRコードをかざすんだが、エラー

あとで気がついたんだが

　　QRコードを読み解らせたあと、アプリになんか変化があり、ボタンを押す必要がある

らしい。それをしないで、もう一度かざすと「エラー」

ってことらしい。ふーん。なんかリーダーがなんかいってたような言わなかったような。よくわからん

というわけで、沖縄に戻ってきました

長崎

なんか、奥様の馬イベントの付き合いで長崎に

馬のイベントにはいかないんですが、長崎で遊んでます

今日は風頭の山にバスで登って、歩いて降りてきました

夜は稲佐山にスロープカーで登って、ロープウェイで降りてくる感じ

街は階段ばかり

でも、沖縄と違って街がきれい。お金があるところは良いね

歯医者

5ヶ月ごとのクリーニング。特に異常無し

なんだが「フッ素抜りましょうね」「え、いいけど、お昼ご飯は?」「30分、だめです」

と、お昼を30分待つことに。歓海門前の真にしました

予約は、さらに5ヶ月後。そんなんでいいのか

同級生になおしてもらった前歯は35年もってるんだよな

その時以来、目だったトラブルは奥歯一本抜いたくらいだ

マイナーカード更新

なんか、Webで申請していたらしく「できました」的な葉書がきてた。年金もそうだが、こういうのに郵便使うのは政府の陰謀的

で、シールで隠されている市役所の窓口(つまり、隠す意味はまったくない)にいくんだが

　「パスワード(番号)を紙に書け」

え〜とは思ったが、大人なので抵抗せずに書く。のだが

　なんかタッチパネルで、そのパスワードを入力しろ
　と、窓口でタッチパネルが登場

え、じゃぁ、さっきの書いたのはいったいなんなんだ? と思ってフリーズしてたら

　「代わりに入力します?」

はい?! なんだが、大人なので

　「お願いします」

で、更新終了〜

いや、パスワード変更してないんだよ。この行事はいったなんなんだ? 単に市役所にパスワードを教える手続き?

時の庭

普天間のラーメンかながわの近くにある喫茶店。台湾系らしく、台湾茶と

　　仙草ゼリー

があります。広くて、無線LANとコンセントがある。水曜休みだが…

午後いくとガラ空きなんだよな。食事ものが最近登場したらしいんだが

なので、行ってみるとよいと思います

近所のフラップコーヒーとか、スタバ、モスとかは割と人が入ってるんだが

Shaef と Agda

Adjunction (HOD-OSCA (topology X) ) ( top / X )

ですが、なんと、一通り書けて、なんでΓの対象が Sheaf になるのかもわかった。

　連続写像の値域の制限ってだけ

なのを、圏とか トポロジーとかSlice圏とか、関手とか、Contravariant とかで難しく書いてあるだけね

なんだが、

　残ってる穴を埋めにいくと、agdaが止まらなくなる

関数が同値なのはすべての値について一致を調べれば良いだけなんだが、そこで止まってしまう

じゃぁ、サーバ側で動かすかと思ったら、既に Agdaのversionが古い。おおい〜

なんか、チェックに時間かかる部分をさぼる方法があったような気がするんだが…

まぁ、もう少し埋めて、それから別なものかな。C-Monoid が面白そう

Google Photos の振る舞い

なぜか、Academic Account ではない方を使ってたりして、たまに「そろそろ一杯です、ストレージ買え」ってのがくる

くるんだが、昔の jpg / heic の重複のを消すと復活する。それを繰り返してるんですが

　重複が甦ってる気がする
　それを消すと容量が増える気がする

まぁ、たぶん、気がするだけだとは思うんだけどさ

そんなこんなで、最近は「そろそろ一杯です、ストレージ買え」ってのはこなくなりました

もしかすると、Academic Accountの扱いになってるのかも。統合したつもりはないんだが

結局、使っている日焼け止めはこれ

なんだが、つけ忘れてしまうので、カバンにいれておくのがよいらしい

沖縄なんで、真っ黒にやいている人もよくみるが、まぁ、ほどほどにね

日焼け止め

まぁ、いろいろあるらしい

Sheaf

まだ、 Adjunction ((topology X)ᵒᵖ → Sets ) ( top / X ) と戦ってるわけですが、

　ΓとLは、だいぶできた

なんだが、「Finally, it is easily verified that ...」が、まったくわからん

この Finally が笑えるのは、Lを作ってるところの Finally なので、さらに、自然変換二つと、その等式二つが残ってるわけ

でも、Agda で書けるので「忘れることはない」。「今まで書けたところは、そのまま残っていて使える」わけね

でも、これプロシンで発表する話でもないしなぁ。役に立つなら話は別なんですが

まぁ、まったくわからんといっても、nat : F → G から、L(F) → L(G) は構成できて、top / X の射の条件である射を作ってるところ

そのうちできるはずです

孔雀楼の冷やし棒棒鶏麺

大山の老舗。結構広い。いつでも開いてる便利なお店(定休あり)

まぁ、普通?