普段のingress Lv.13

まぁ、お店が早く閉まっちゃうので、夕ご飯食べたあとで歩きにでるわけですが、

　　酒が入って歩くとしつこくなるのがな...

運動公園まで一周見たいな感じで。途中のコカコーラの会社のポータルが

　　人気のない通り

でな〜　自分で生やしたポータルなので自分がいけないのだが。2時間くらい。

でも、翌日の夜まではだいたい落とされてました。Ingress は

　　暇人 vs 暇人

的なところがあるのでね。

去年の11月にRecursして Lv13 になりました。Lv16 は自分のペースだと1年以上かかりますね。

証明書解決編

もう podman かなり忘れてて、podman-compose とかの k8s もどきもあって

　　復習大作戦

的な感じで。まぁ、もともと教育的プロジェクトだからいいかとは思うんですけどね。自分の。

dockder/podman には、そういう文化があって、それに乗るのが慣れない。

　　atp-get で install

とかやらないのね。container のimage上で command 一発だけ的な。Docker.io から取ってきた image 信用するのか的な。

まぁ、でも、podman network を思い出したので、その network を使って podman でlegoで証明書を取れば良いだけか。

というあたりで、優秀だったOBが入ってきてくれたので、そこからは30分くらいで片付きました。

Web server を止めずに lego で証明書をとる方法もあるらしいが、まあ、いいか。

gitlab は rails に lets encrypt の support が入ってるらしい。えらい。

偉そうな SINET のジムと対決するよりは lets encrypt が良いよね。

証明書切

よくあるアレですが。MatterMost の方は少し苦労したみたいだが、シス管が自力でなんとかしたみたい。

いや、Lets' encrypt でいいし、MatterMost はそうして片付けたらしいし、月曜日にも同じことやってた。

なのだが、Web と gitlab だめらしい。いや、コンテナ/VMの外からではだめだと思うよ。

NIIが中間証明書をrevokeしてしまうので、期限切れではなく「読めなくなってしまう」ってのがな〜

自分の研究室のサーバには「証明書なんか入れてない」ので、こういう問題とは関係ないんですけどね。

また、夜頑張るみたいです。(他人事?!)

石鹸派です

アルコールでちょこちょことかおまじないに過ぎない感じで嫌い。

やっぱり巨大な石鹸で泡立ててついでに顔も洗う的なのが良いな。

風呂場でもボディーシャンプーとかシャンプーとかよりも石鹸の方が良い感じ。

クエン酸リンスすればごわごわしないし。

去年の今頃も石鹸がなくなるとかまったくなくてよろしかったです。

すごい硬いアイス

随分前に横浜のルノアールで。なんで横浜まできてルノアールかって言うと、

　　風速20mの嵐をくらったから

です。アイスチーズケーキらしいです。ナイフの歯がたたない感じ。

結構良かったです。ルノアールは、自分の年には便利な感じの場所だな。

レンタル自転車

琉大にも四月から登場したので使ってみました。宣伝皆無。やる気ゼロだな。バスの中くらいなんか出せば?

15分80円は安いとは感じないな。バスに合わせるみたいなくそな基準なのではないかと想像します。
1時間使って400円。琉大北口からキリ短往復くらい。

アプリのアカウント登録はクレカ/PayPayが必要。日本人/学生はクレカ嫌いだからなぁ。
年齢とか聞いてくるが skip 可能。登録はマイナンバーよりは簡単です。学生は無料くらい
やらないと誰も使わないんじゃないの? むしろ、逆に使うとローソンのポイントが付くとか。
エコとか言いながら発想がけちくさい。沖縄だと戦ってるのは車なんだから金かけないと。

割と色んな場所に返せるらしいけど、平均化みたいなのはやってないらしく「0台」が結構ある。
任意の場所、あるいは登録可能にするとかもありだろうな。

電動アシストだけど、1時間はそこそこ疲れる。1時間歩くより疲れる感じ。ぴーかんで出たはずなのに

　雨が降ってきた

のは笑いました。そういう雨男なので。

昼間乗るには帽子が必須か。あるいはメット。
自分は自転車とか少し危ないんだよな。周り見ない人なので。

Ingress で取りにくいポータルとかに行くのは便利。
大学内のポータルを取るには便利だと思います。車使うか普通は。

ひとなべ

まぁ、狙いはわかるんですけどね。

その語感なんとかならないの? お一人様な時代が来てるとは思います。

VSCode Mathjax

Markdown にかっこいい数式が書けて、しかもLaTeX互換。でも VSCodeだといくつか落とし穴が...

　　Markdown+Mathを入れれば良いが delimitor を gitlab にする必要がある
　　変な小さな○が付いているボタンを押さないと preview できない
　　new file してもファイル名がないから .md で save as して開け直す必要がある

macOS で backslash を入力するには環境設定のkeybordのinoput source/日本語から¥をbackslash に。

最後に、

　　VSCode で backslash は¥と表示される

え、それはないでしょ? なにそれ。フォントの問題か? 自分のは問題ないぞ。でも

　　表示されるだけで Mathjax 的には問題ないらしいです

面白いね。

筋トレグッズ

まぁ、男だからな。卒業する時に研究室にゴミ捨てるのも許すよ。

週二回くらいでもいいから、筋トレ。ただ、血圧に響かない程度に。

Polynominal

Lambek/Scott の Higher order categorical logic の続き。

　　Polynominal　　変数として使う射x : Hom A 1 a を追加した圏Aの拡張 A[x]
　　Functional Completeness　x を使った推論の正規形 a ∧ b → b の unique な射ψ(x)
　　internal language 集合を含む直観主義論理を表す A 上の record

で、ψ(x) が { x∈a | ψ(x) } : Hom A 1 (P a) になるってことらしい。これで internal language で集合が扱えるようになります。

結果的に全部つながってめでたいのだが、いろいろ大変だった。

　　そもそも、x は A に入ってないはずだろ? しかし、x : Hom A 1 a と書いてある....
　　Hom A 1 a は複数あるが、それは変数名なので同じものを指すはず
　　Hom A 1 a があるとは限らないじゃん

x を使った推論は5種類しかない(証明なし)。これで場合わけする。これは data φ で表す。

本には「分解してgraphで再構成」とかご無体なことが書いてある。結論から言うと、

　record Poly (a c b : Obj A )　: Set (c₁ ⊔ c₂ ⊔ ℓ)　where
　　field
　　　 x :　Hom A １ a
　　　 f :　Hom A b c
　　　 phi　:　φ x {b} {c} f

という record がψ(x)に相当する。そもそも x は局所変数なので大域的に持ってはいけないらしい。

Functional Completeness は

　record Functional-completeness {a b c : Obj A} ( p : Poly a c b ) : Set　(c₁ ⊔ c₂ ⊔ ℓ) where
　　x = Poly.x p
　　field
　　　fun　: Hom A (a ∧ b) c
　　　fp　 : A [　fun ∙ <　x ∙ ○ b　 , id1 A b　>　≈ Poly.f p　]
　　　uniq : ( f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b　 , id1 A b　>　≈ Poly.f p ]
　　　　 → A [ f　≈ fun　]

で良いらしい。fun には x は関与してないし、使う時にはxは既に存在する射 Hom A 1 α に置き換えられる。

これの存在を示すのは fp まではφの場合わけで良いだが、uniq は

　　f ≈ g → k f (ψ(x)) ≈ k g (ψ'(x))

が必要になる。locally smallなら単なる cong だが、そうでないと自明には成立しそうにない。特に、
ψ(x)と ψ'(x)の x は型が合ってるだけで値が同じとは限らない。これは「分解してgraphから再構成」
からしかでない。そして、それはまだ書けてない。なので、仮定してしまうのが早いらしい。
locally small からは出るので矛盾にはならない。

internal language と接続はこんな感じ。まだ正しいとは限らないが。

　　select : {a : Obj A} → ( φ :　Poly a Ω １ ) → Hom A １ (P a)

あとは、これを internal language で使うε形式に直せば良い。

　-- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) →　f ∙ x ≈　φ x　
　record Fc {a b : Obj A } ( φ :　Poly a b １ )
　　　　 :　Set ( suc c₁　⊔　suc c₂ ⊔ suc ℓ ) where
　　field
　　　sl :　Hom A a b
　　g :　Hom A １ (b <= a)
　　g　= (A [ sl　o π' ]　) *
　　field
　　　isSelect : A [　A [ ε　o < g　, Poly.x φ　> ]　≈　Poly.f φ　]
　　　isUnique : (f : Hom A １ (b <= a) )　→ A [　A [ ε o < f , Poly.x φ　> ]　≈　Poly.f φ　]
　　　　→　A [ g　 ≈ f ]

とすれば良い。g は変わった記号を使うんだが、k14にないので作らないと...

これを示すには、そこそこ計算が必要。CCC の計算練習みたいなものだが。型を書いてみて分かったのだが、

　　εは型を持つ

なので、CCCで変換する時にεを生成する型を間違えると当然致命的。型変換 s・s ⁻¹ を挟んで途中で
切って合わせてやると良いらしい。

そこまで気がつけば、Fc の生成できました。長いけど時間がかかるだけ。これ全体がそんなものではある。

A[x]をある意味で構築できたので、coMand な関手S(a) : a ^ b → b の Kleisli 圏S(a)を考えれば普遍問題になる。
つまり、任意のA[x]がS(a)に iso になるというのが functional completeness で、それはS(a)が CCC関手である
ことを示せば良いらしい。ただ、record Poly は技巧的なので、それに使えるかどうかは謎です。

でも、とりあえず、これで、Polyniominal 圏、Functional Completeness、Internal language まではつながりました。
まだ、直観主義論理の公理はチェックしてないけど。CCCのは成立するので集合分、つなり、fuctional completeness
の確認作業になるはずです。

https://github.com/shinji-kono/category-exercise-in-agda/blob/master/src/Polynominal.agda

猫バス

あの、そんなに広く開けちゃうと、猫は気に入らないんじゃないかな。

キーボードの横には箱を置いておくと、キーボードに乗らないっていう説を聞いたけど、実践してません。

お医者さんのはしご

といっても、歯医者さんのクリーニングはお布施だし、血圧の薬は税金みたいなものだな。

バスで両方にと思ったのだが、午前中って

　　内科は割と混む

そうね、お年寄りは早いのだった。なので思う通りにはいかなかったんですが、任務完了。

最近、体重を維持できてるせいか、血圧も低め。そもそも、お医者さんだと低めな方だし。

あと気温かな。寒いと上がるね。80-140 くらい。

-

カセット

まだ、普通に売ってるんだよね。ありえんだろって思うけど。一つは、

　　デザインの敗北

だと思う。最新機器、スマホとか録音機のUI設計がカセットに負けてる。

　　大きくてわかりやすい

を捨ててしまったからか。たまに、

　　昔のソニーのラジカセ (CF-1500 とか)

を使ってみたいなとは思います。カセットは捨てられちゃったけど。

回収することは可能だったし、iTunes に取り込む機材と時間がなかったわけではないのだが、

　　なんとなく、もういいです

的な感じで。カセットの生録は割と黒歴史だしな。生々しくて。

ゆいレール作業所

ここに停まっているのをみるのは割と珍しい。

中途半端な屋根が謎ですが、工事費削減かな。

最後の発掘

この前から残っていた VHS の最後のですが、総情センタに用事でいったら

　　いろいろ古い機材が置いてある VHS/DVD とか VHS/DV とか

VARDIA とか懐かしすぎるんですが。しかも、ちゃんと動く。ところが、

　　もはや、HDMIでないディスプレイがない

ふふ。こんなこともあろうかと、Video/S端子なディスプレイがあるのだ。

なので、わざわざそれを持ち込んでダビング。

　　「ディプレイ置いておく? 他の人が使えるように」

まぁ、それはお断りだったのでディスプレイは回収。VHSも無事HDDに収納できました。

ま、ものは大したことないんですけどね。

基礎数学

というと、あの岩波の基礎数学の苦い思い出が...

蓋を開けてみると

　　受講者は一人!

なくなるのかなと思って「登録しなくても受けていいよ」と言ったら三人に。

1から勉強するというのはなんか魔法な感じがあるね。

初日は

　　gitlab の README.md に Mathjax で数式を書く

だったんですが、それで一杯一杯だな。そんなものです。

まだ全然できてないが...

https://ie.u-ryukyu.ac.jp/~kono/lecture/basic-math/math01/lecture.html

歯医者さん

1年くらい空いたかな。詰め物少し空いたかなと思ったけど、そんなことはなく。

なんか新しいCTが。なのだが古い方が大きく映るので使いやすいらしい。で、

　　あ、ここ虫歯ですね

げ。先生、見落とし多いんじゃないですか? ま、僕は

　　医者は少しやぶの方が好み

なので。今時は麻酔も削る道具も詰め物も便利なものが多い。光凝固で1時間も掛からず終了。

神経に引っ掛からなかったし。前回はブリッジで引っかかってさっさと神経抜かれたのだった。

来週クリーニングで終わりみたいです。

体重

Omron の体重計を使っているんですが、アプリが最低で... データを抜き出すことさえできない。
この手のもので直接サーバに通信するのやめて欲しい感じ。せめて有線で抜き出せるとか。
アプリのスクロールを動画で撮って画像認識で抜き出すってのを考えたんですがやる気ゼロです。
アプリ変わるみたいな話なんだが...

もっとも、この間の胃酸過多(2/10)で60kg/166cmになったので、お昼ご飯控え目 + 筋トレで
それを維持できている感じ。
まぁ、筋トレはたいしてやってるわけでもないので関係しているとは思えないです。

筋トレ頑張りすぎると血圧のせいか気持ち悪くなるので、そこまではやらないという対処なので、
負荷が足りないんだろうな。

数学の授業の準備

二桁の足し算からやる授業ですが、だいぶ資料は進んで、整数、有理数、多項式、そして、

　　方程式

と。で、その解を作るのに原子根で代数的拡大すると複素数が入るってな感じですね。

方程式の解を作るのに数を拡張していくってのは面白い。どっかの本にもそんな解説があった。

Wolflam alpha に方程式を解かせるみたいな課題もだそうかと思ってます。

超準解析も順調だが、積分は区間の無限分割をやらないとだめなのか。natural extension? え〜

でも、そこが終われば微分方程式の解として不定積分やって、exp/sin を級数でだして終わりかな。

もちろん、いろいろ足りないが... 教科書は分厚いから。

黒いパネル

そういうの見ると液晶Displayっぽい。まぁ、なんか表示しておいても良いかな。

写真スタンドみたいな感じで。でも、いざ、点いてると

　　うっとうしいと感じる気がする

消さないといけないし。スマートスピーカーは導入してないんだが、

　　それも、うっとうしいと感じるかもな

特に大きなDisplayを普段どうするべきか...

Internal Language

圏論の続き。竹内外史先生の層圏トポス、Lambek/Scott の Higher order categorical logic の
両方の中心的なところ

　　圏のトポスから直観主義論理を導出する

ってところですね。やっとここまで来た的な。ところが、Lambek ではInternal Language は1 page。

これが難い。そもそもAgdaは直観主義論理なので、自分自身を書くようなことになる。万能Turing machine
みたいなものだが、気をつけないと書けなくなったり、逆に変数を番号で表して詳細を展開するような羽目に。

論理をdataで構文木に展開したりするとかなり大変。竹内先生の方ではそうしていて十数ページ。なぜ、

　　1 page に収まっているのかが謎 definition 3.5

でも「型は圏A/Toposのそれ(対象)」とか書いてある。ToposはCCCだしN(自然数)も入っているので
* 0 Sn <a,b> はそれをそのまま使って良いんじゃないか? 残るは三つ。a=a' と a∈αはそこに書いてある
ように射を組み立てるだけでできた。 要するに直観主義論理の要素を圏Aの射に変換するだけなので、
マクロみたいなパターンで書いて良いらしい。

これは簡単。つまり、Topos と同じで、CCCな圏に射を付け加えるrecordとして inernal language を作れる。
これだと、Topos <=> Internal Language は、ほぼ対等になるのでよろしい。

問題は最後なんですが

{x∈a|ψ x} is λ (x∈a) →ψ x , the unique arrow α : 1 → P a such that x∈a ≈ ψ x

ってなんだよ。その the ってなんですか。ψ x ってなんだよ。で、さっぱりわからない。なんですが、
そのページの上の方を見ると、「λ (x∈a) →ψ x」がそのままある。そこか。

この前、格闘した Functional Completeness を使うとある。ところが前にやったのは割とインチキでなぁ。
そのままでは使えない。要するに、「λ (x∈a) →ψ x」なので x : 1 →a (aの要素を一つ指し示している射)
は引数(仮パラメータ)なわけだ。でも、x : 1 →a　は仮定なので圏Aにあるとは限らない。なので、
A[x] とか coKleisli圏とかの工夫が... 層圏トポスの方だと別なものを使ってる。でも、ヒントが。

そうか、ここで使える用に Functional Completeness を仮定してしまえば良い。それを実際に証明できる
かどうかは後回しで良い。

結果的にはかなり短くできたみたい。使えるかどうかはこれからだな。

record InternalLanguage (Ω : Obj A) (⊤ : Hom A (CCC.１ c) Ω) (P : Obj A → Obj A)
: Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
field
_==_ : {a : Obj A} (x y : Hom A (CCC.１ c) a ) → Hom A (CCC.１ c) Ω
_∈_ : {a : Obj A} (x : Hom A (CCC.１ c) a ) (α : Hom A (CCC.１ c) (P a) ) → Hom A (CCC.１ c) Ω
-- { x ∈ a | φ x } : P a
select : {a b : Obj A} (α : Hom A (CCC.１ c) (P a) ) → ( (x : Hom A (CCC.１ c) a ) → Hom A (CCC.１ c) Ω ) → Hom A (CCC.１ c) (P a)

中学校の時計

バス停の目の前にあって、微妙に便利だったんですけどね。壊れちゃって。

でも、この仕打ちですか? 公共の建物でしょ? 景観とあるじゃん。

　　その貧乏くさいの、なんとかならないんですか?

Mathjax の続き

自分の授業のページは、Emacs の outline mode から生成してます。流行りのMarkdownだが、

　　自分の方が早い

と思わなくもない。でも、Mathjax は入れんとあかんのか。自分勝手なのだから自分で直すしかない。まぁ、

　　</script>
　　<script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
　　<script type="text/javascript" id="MathJax-script" async
　　　src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
　　</script>

を入れるだけらしい。たぶん、Browserでキャッシュされるんだろうから、そんなに重くないだろう。
とは思うが、年寄りなのでなんか残念には感じる。だからといって使っているかどうか判断するのを入れるのもな。

これだけで動いたみたい。

Facebook でも、\(a^2+b^2=c^2\) ぐらいでてもバチはあたらないとは思いますが。

代数学の基本定理

n次方程式には必ず複素数面上の解があるというガウスのあれですね。1年次の授業用になんかあるかなと思って。

5次方程式には代数解がないというガロアのと重なって大惨事。なんて事件も。

自分の好きな証明はシュワルツに載っていた

　(1) 零点がなければ逆数を取ると全域で有界
　(2) 全域で有界なら定数関数と一致

なのでで矛盾ってやつです。(2)は最高次の係数が0でなければ、どんどんでかくなるはずなので割と自明。

なので、3Dグラフでガウス平面上の関数を表示すると、x³+ 1 の三つの零点が見えるんじゃないか?

と思ったのだが割とめんどい。|(x+yi)³+ 1|だけど... いやでも、1年次が面白がってやるかも?

j5 374 復活

BigSur update で使えなくなっていた j5 なんですが、代わりのものを物色してたら

　　SIP切れば昔のdriverが入る

ってな記事を見かけて。Driver入れ直しはやったんだけど、そういえば、BigSur install したから

　　ばっちりSIPが再設定されてる

Recovery mode から csrutil disable の driver の再インストールで、セキュリティでの許可を入れて再設定

　　ばっちり認識しました

もう、一日の仕事終わった気分だよ。やっぱり、無線LANの Zoom は不安定だからな。

まぁ、これも使えなくなるのは時間の問題だとは思います。

BDのケース

そろそろ録画もやめちゃえ的なところもあるんですが、録画の整理の季節。

エレコムの48枚ケースを愛用してるんですが、ある日、Goodwill から消滅。どうも、

　　不織布ケースはメディアに跡が付く

とかいうblogを書いた奴がいるらしく。そういえば、HD-DVD陣営はBlu-rayは記録域が浅いから弱い的な主張をしてた。

で、Blu-ray側は硬度があるから大丈夫的な反論で。まぁ、もともとケースとか流用できるからCD/DVDと同じ大きさなわけですが。

で、その後、エレコムはBD用と称する「不織布の目の細かいケース」を200円高で発売(30%くらい高い)。なるほど。

でも、Goodwill で復活することはなく。ま、そうだよな。狙い通りだったんですかね?

ま、水平に積んで圧力かけるぐらいでないとな。もっとも、そんなことすればDVDでもだめなわけだが。

もともと縦におけば問題ないし、DVD-Rの信頼性の低さの方が問題。Blu-rayもたまに「スピンドルごと不良」を喰らいますが。

最古のDVDが2005くらい? BDは2010からかな。特に問題ないかな。どっちかっていうと

　　多重音声がレート変換で落ちる

って方が困ってて、それが原因でスカパー使っていたんですが、スカパーも多重音声軽視なのでやめてしまいました。

で、そろそろ録画もやめちゃえになってきてるわけだな。

数式を書くには...

1年次向けだからな。Renderingがいるってのがネックなんですが、

　　gitlab 上の Markdown

が良いんじゃないかと。そう言われ見ると、自分の使ってる Emacs Outline にはそういうの入れてない。

自前勝手ツールの悲哀だな。ま、markdown に降っても良いんですけどね。

　　athjax example
　　===

　　third
　　----

　　This math is inline $`a^2+b^2=c^2`$.

　　This is on a separate line

　　```math
　　a^2+b^2=c^2
　　```

https://gitlab.ie.u-ryukyu.ac.jp/math/basic-06/e215799/-/blob/c79b278ea044b2603acf6db788efd220c2414d95/m01/ex01.md

新学期

なんか新しい授業が入れらちゃったけど、学生に数学の問題解いてもらうくらいらしい。

今の学生の数学能力は英語の能力と同じくらい怪しいからなぁ。二桁の足し算から始めようかと思ってます。

MathJax? それもいいかな...