貸し自転車

最近、バスが減らされちゃって。仕方ないので。我如古の坂を貸し自転車で。

　　しかし、iApp から認証したあと、鍵が開かない

まぁ、良くある話しだ。

　　そのまま、返却して、他のをトライ。

ところが、

　　坂の真ん中で、パワーアシストがだめに

電池切れか。で、残りは、足と手押して。まぁ、

　　バスには抜かれたが、中商からのバスには乗れました

運動になってよろしい。もう、あんまりメンテしないみたいだな。壊れたら撤退ですかね。

ひさしぶりの歯医者

1年ぶりとかいわれましたが、

　ハガキで案内してましたがLINEにしました

って別にいいけど、それは案内しないのか。

奥歯の詰め物取れただけで特に異常はないらしい。少し欠けてたけど「セメントで付けるのでいいかな」

少し歯に色が付いてたんですが、なんか綺麗にしてもらいました。普段、歯磨き使わないからな。

なんか天井にディスプレイがついたのがあるらしい。

準同型定理もう一度

チコノフの方もだいぶできたんが、少し距離あるので、何かほかのを見直してたら、

　　 g ⁻¹ ∙ f ⁻¹　∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ )　　　　 ≈⟨ solve monoid ⟩
　　 g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))

とか並べなおしてくれる機能が。これは便利。いちいち、assoc とかするのかなりつらくて。

でも可換とか逆元とかはやってくれないです。Ring solver もあるけど、その程度。

で、集合結構やったので、商群も集合だよなと思って書き直したら、割とうまくいった。

⟦ n ⟧ で、準同型写像を表すのが Agda 流らしい。

　　record an {A : Group c c }　(N : NormalSubGroup A ) (n x : Group.Carrier A　) : Set c where
　　　　field
　　　　　　a : Carrier
　　　　　　aN=x :　a ∙ ⟦ n ⟧ ≈ x
　　
　　record aN {A : Group c c }　(N : NormalSubGroup A )　: Set c where
　　　　　　n : Carrier
　　　　　　is-an : (x : Carrier) → an N n x

と二重にすると良いらしい。なのだが、相変わらず、準同型定理自体は refl に。なんで。

どうも商群の要素の比較を、

　　 λ f g → ⟦ n f ⟧ ≈ ⟦ n g ⟧

でやってるのがいけないらしい。集合として同じってことなら、少しずれがでる。でも、結局、同じだけどな。

record FundamentalHomomorphism (G H : Group c c )
　　(f : Group.Carrier G → Group.Carrier H )
　　(homo : IsGroupHomomorphism (GR G) (GR H) f )
　　(K : NormalSubGroup G ) (kf : K⊆ker G H K f) :　Set c where
　field
　　h : Group.Carrier (G / K ) → Group.Carrier H
　　h-homo :　IsGroupHomomorphism (GR (G / K) ) (GR H) h
　　is-solution : (x : Group.Carrier G)　→　f x ≈ h ( φ x )
　　unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)　→ (homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 )
　　　 → ( (x : Group.Carrier G)　→　f x ≈ h1 ( φ x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )

修善寺駅

もうだいぶ前だが。

温泉娘が。そして、駅前の寿司屋さん。普通でした。

ひっつき虫電池

ケーブルがだめになるのが残念なのでいいかなと思ったんですが

　　少し重い、ワイシャツに入りにくい

あと、最近の iOS の update で、

　　充電は遅いわ、減りは早いわ

になったので、割と使う羽目になってます。そのまま充電できるのは良いが

　　電池と iPhone の充電は排他

な感じだな。もう少し薄いのが欲しいかな。

初代 Kindle

これが、まったく問題なく使える。もちろん、

　　くそ遅いし、バックライトもない
　　タッチパネルでさせえない
　　UI ひどい

わけなんですが。

読みやすいのは、iPad なんだけど、

　　すぐに陳腐化するのがな

iPad / iPad2 とかすごく残念だった。

電池がだめにならないようにたまに充電してますが、

　　割と奴隷感がある

いや、最低限でいいから、動いてくれれば、いろいろ使えるんですけどね。でも、

　　目と手がたくさんあるわけでもない

からなぁ。

桜

ここ数日あたたかいというよりは、暑いです

なんか寒くなるとか言う話を一週間聞いていたような気が...

舌がなおってきた

年末に、キャベチャーを海苔で食べた時にやっちゃって。なので

　　割と年末正月と残念だった

んですが、まぁ、たいしたことはなく。ただ、

　　年とるとなおりが遅い

怪我や病気すると、男は弱気になるものだしな。

歯の詰め物が取れたんだけど、

　　治療は1/30

え〜　そんな先? けっこう、がしがし磨いているので、良くはずします。もっとも

　　外れるのは虫歯の結果

ってのが多いらしい。まぁ、それもこの年になるといろいろね。

Project Hail Mary

評判を聞いて Kindle で買ったまま死蔵だったんですが、土日暇だったので。

でも結構時間かかったか。英語。わりとネタバレありで。

構成が、記憶喪失な自分と、徐々に思い出す回想になってて、一緒に謎解きできる感じ。

この感じはホーガンに似てるな。勢いがあってよろしい。プロジェクトががんがん進んでく感じも似てる。

計画に

　　すごく良く準備されている

ところもあれば

　　それはないだろう

ってところも。この手の計画は綿密に立てるので

　　普通は何も起こらない

と思うんですけどね。それではお話にならないが。

問題の Astrophage が便利すぎて、そんなものがあるなら、もっといろいろできるだろは思います。

普通にもう一機送るとかするでしょ? Project Hail Mary

温泉といえば...

まぁ、これ。そして、

　　変なお金を入れて動かす機械

パルスオキシメーターにしか見えないが。まぁ、そうなんだろうな。

こういうビジネスモデルを目指せみたいな話がなんども出てくるけど。

プロシンで流行ってたあれ

これなんか見たことある。確かスピーカーの下に置くやつじゃなかったっけ?

それを張り合わせて作るわけね。

必ず地面についてないといけないので、それほど着手数が多いようには見えないんですが
三次元だからいろいろあるんだろうな

北池袋陸橋

この辺、割と好きなところだな。まぁ、ソープ街なんですが。

天気の子の聖地でもあるか。


-
-

ボードコンピューター

電子情報のものもちの良さよ。

これでも自分で配線して作ろうと思うとそこそこ時間がかかる。シミュレーターでいいとも思うけど、

　　実機の楽しさがあるのもわかる

こういうのはがあるのがよい時代もあったんだけどな。

要町恵比寿通りのパスタ

プレファボーレっていうんですけどね。850円。やすい。15年くらいやってるらしい。

前に、一度入ったことがある。そん時は、そんなに思わなかったんだけど、

　　安くてうまい

パスタは最近の値上がりでいろいろ変えてしまうところが多くて... 少しぐらい値上げしてよいんですが。

ここは、母がいるうちに、もっと通うべきだったな。

いや、でも、

　　年々、美味しいと思うしきい値が下がってる

ような気もするんだよな〜

またまた、Echofon が

twitterの3rd party clientが軒並みやられたらしく。今回か復活するかどうかは。本家も

　　twitterへの投稿はずいぶん前

いや、公式 iapp かなりひどくてな...

　　見せたいものだけを見せるんじゃない!

ってところですが。もっとも、

　　PC側は公式 Web UI

なんだよな。学生は Tweet Deck が多いみたい。

景色のいい会議場で遊ぶ人たち

発表中は閉じられてしまうのですけどね。

今回は発表は Zoom つまり

　　画面への接続は Zoom 経由

でも、遅延とかあんまりない。いくつか問題があって

　　会場の声が Zoom に乗りにくい
　　動画再生とかで問題がでることがある(原因はいろいろ
　　この問題は事前チェックできない(Zoomに接続してみないとわからない

でも、全体的にはスムーズだったと思います。Slack も楽しかったな。

研究会と平行した Slack は全部でやって欲しい。

トートバッグ

出張は、いつもの格好に、着替えを入れたトートバックを足すだけ。らくちん。

洗濯も楽だし。

プロシン太り

二泊閉じ込められてたからな〜 1時間半で修善寺駅まで降りられるらしいんですが、ちょっと断念。

麹町に寄ったら、触ってないポータルがたくさん。あと50で、Explorer が10,000か。

沖縄でも結構増えてるんですけど、なかなかね。

気がつくと、他のメダルも色が変わるのが近い。Mind Controller 黒は気がつかなかった。いつのまに。

修善寺からの帰り

修善寺でそば食ってたら、踊り子が一時間先なので

　　鈍行でいいや

で、三島で乗り換えに微妙に間に合わなかったら

　　同じような人がもう一人

そのまま、東海道線/埼京線乗り継ぎで。fnami とゆっくり話せて良かったかな。

ま、べつに急ぎじゃないし。

プロシン二日目

今回のプロシンは

　Slack
　発表者と聴衆
　Zoom

という組み合わせ。

いつものゆるい感じですけど、うちの学生の発表もなんとか。現地に学生が来なかったのは残念だが。

Rubyの高速化の話がいつも通り面白かった。interpreter をアセンブラで書いて、JITとABIをそろえる。

おぉっという感じ。CbC使ってください。

プロシン

3年ぶりのオンサイト

自分は、オンラインでも平気

ではあるんですけどね。でも

　　温泉はいいよな

発表資料書いてたら 50 page だったんですが、ま、時間内には終わりました

電車で

兄妹の妹の方がギャンなき

電車なんかかなりうるさいので、別にいいんだが、

結局、降りることにしたみたい

降りて解決するかどうかは。なんかキャラクター書いた紙で気をそらすとかあるらしい

自分も妹がそんなだったのを見たのを思い出しました

-

授業中の攻撃

いや、今日から授業なんですが

　　いきなり、有線がつながらない

技が... DHCP が死んでるのはわかって、(じゃぁ、なんで無線いきてる)で、サーバに入れない。

で、freeradius の log で DB に接続できてないまではみたんですが、

　　そこであきらめ、無線でもいいよね

「すみません、postgressの設定ミスってました」メッセージが授業後に来てました。

ま、いいけどさ。

二日は飲んだくれてました

毎年そうならしい。去年は pumping lemma やってたとか書いてあるな。

そこしか開いてないので、「ようこ」で飲んでたんですが、帰る頃には他のお店も開いてる。

そうか、そういえば毎年そうだった。と、毎年思い出す。

積位相

結局、トポロジーに手をつけてるんだけど、チコノフやるなら、積位相書かないと。

record Topology　( L : HOD ) : Set (suc n) where
　 field
　　　 OS　　: HOD
　　　 OS⊆PL :　OS ⊆ Power L
　　　 o∩ : { p q : HOD } → OS ∋ p →　OS ∋ q　　　→ OS ∋ (p ∩ q)
　　　 o∪ : { P : HOD }　→　P ⊂ OS　　　　　　　　→ OS ∋ Union P

これの直積だろって思ったんだが、直積の方を見たら、Zornの補題やりまくったせいで、だいぶ見通しが良くなってて、
劇的に簡単に。ところが...

　　積位相って単なる開集合の直積じゃない

え。まぁ、それでも位相空間にはなるらしいんだが。最弱じゃないとかあるらしい。

まぁ、PとQの直積空間をP方向Q方向に短冊みたいに、Pの開集合とQ全体の直積みたいにすれば良いらしい。

のだが、いざ Topology 書いてみるとぜんぜんできない。で、諦めて、少しぐぐって定義をみたら、

　　準開基から生成する

とかある。しかも証明は「明らか」。くそ〜　準開基自体は、集合の可算回の∩ってだけなので瞬殺だったんですが、
開基の生成が意味不明。Union (Power P)かと思ったら、OS ∋ Union P が、まったく出てこない。P ⊂ OS でなくて、P ⊆ OS
でやってたとかもあったんですが(それだと絶対できない)。

しかたないので、教科書に戻って開基からの生成を見直すと、

　　OS = { U ⊂ L | ∀ x ∈ U → ∃ b ∈ P →　x ∈ b ⊂ U }

とある。これが、どうして生成になってるのかわからなかったんですが、Uのすべての点に対して、Uの中にある
(b ⊆ U でもよい) 準開基を使うわけね。

結局、こうらしい。

record Base (L P : HOD) (u x : Ordinal) : Set n where
　 field
　　　 b　 : Ordinal
　　　 u⊂L : * u ⊆ L
　　　 sb　: Subbase P b
　　　 b⊆u : * b ⊆ * u
　　　 bx　: odef (* b) x

SO : (L P : HOD) → HOD
SO L P = record { od = record { def = λ u → {x : Ordinal } → odef (* u) x → Base L P u x } ; odmax = ? ; <odmax = ? }

record IsSubBase (L P : HOD) : Set (suc n) where
　 field
　　　 P⊆PL　: P ⊆ Power L

これで、あら不思議、準開基から位相を生成できた。

　　GeneratedTopogy : (L P : HOD) → IsSubBase L P　→ Topology L

いや、簡単とはいえないけど。P ⊆ Power L だけから、Topology L 作れるとか、すごすぎないですか。

積位相も以下の準開基から簡単に生成できました。

record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where
　 field
　　　 p q : Ordinal
　　　 op : odef (OS TP) p
　　　 prod : x ≡ & (ZFP (* p) Q )

record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where
　 field
　　　 p q　: Ordinal
　　　 oq : odef (OS TQ) q
　　　 prod : x ≡ & (ZFP P (* q ))

base : {P Q : HOD} → Topology P → Topology Q → HOD
base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }

生成は一発

_Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
_Top⊗_ {P} {Q} TP TQ =　GeneratedTopogy (ZFP P Q) (base TP TQ) ?

https://github.com/shinji-kono/zf-in-agda/blob/master/src/Topology.agda