浦添運動公園

ANA の名前がついてるんですが、工事中で通り抜けできない

でも、問題はそこではなくて、

　ingressの赤ポータルがはびこってて、誰も刈れない

まぁ、プレイヤーがはっきり減ってるってのもあるんですけどね

体育館経由で、そこそこ寄れたので、そこから半分くらい落としてきました

Ingress Resistance 宴会

Anormally お疲れ会にいってきました

なんですが、Anormally 自体はさぼりました。すみません

Niantic がいろいろ丸投げしてくるので割と不評ならしい

2月に課金はやめたんですが、少し活動してます

Cubical Agda の続き

Cubical Agda の論文も読んだんだけど、1011 みたいなバイナリ表記をℕ と≡ で結ぶとかの話が出てくる

そういう方向ですか。そっちの推論自体は要らないかな。割と証明苦労したところだが、それ自体が簡単になるわけではないらしい

でも、それよりも、Cubical Agda と互換にするのが面白いことを発見しました

だいぶ、慣れてきた

　refl で受けるのには条件がある
　パターンの成立しない条件は明示的に消す ( Cubical でないのは書く必要自体がなかった)

あと

　Dec P

が全滅。yes とか no とかで、真偽の理由を取ってこれる(のを自分で作る) 。でも、なんと

　自分で定義すれば回避できる


data Dec (A : Set) : Set where
yes : A → Dec A
no : (A → ⊥) → Dec A

どういうこと?!

Cubical Agda

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

の修正は終わったんだが、

UnsupportedIndexedMatch の警告を抑制してた

Cubical は Homotopy Type Therory と関係あるらしく、無視しようかと思ってたんですが

量多いし。でも、

　どうも、理論的には少し工夫すると消せるらしい

つまり、with による data の場合分け、つまり、単一化の複雑度の問題なわけね

これを避けると、実は少し見通しが良くなる

なので、取る方向かな。ついでに Cubical Agda を少し学ぶか

台風日和

晴れ時々土砂降りみたいな感じ。バスを降りたときにくらいました

なんか、街が空いてる

こういうの悪くない。コロナ自粛の頃もそうだったけど

　　社会は、これくらいの活動度でいいんじゃないの?

なんか、妙に忙しそうにしているよりも、がらがらな街で、余裕で仕事して、それで社会が進む

大山の米や松倉

オーナーが変わったらしく、昼営業のみ。2000/2500円

和食ですけど、中で精米してお米も売ってます。ひとめぼれと言ってました

前のお店は、おにぎりとかあったんですけどね

雨に降られてってよりは、歩いていったんで、なんかタオル出してもらった

夜やるかどうか迷ってるみたいこと言っていた

iPad の容量

iPad はネットにつなげて使うものなので 32GB 派だったんですが、さすがに最近、足りない感じでな

一時期に比べると高いが、256GBかなぁ

昼間の ingress

暑い

リハビリっぽい感じ。無課金にもなれてきた

Agda のflag

なんか、

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

とすると、いろいろ出るエラーのうち

--warning=noUnsupportedIndexedMatch

を抑制していたみたい。それでいいっていいえばよいんだが、時間はあるので修正してます

他の部分も割と順調

学生のいない気楽さか

Agdaの高速化の話

結局、編集部分だけ別モジュールにしたら、まぁ、許せる速度になったのでそういうことで

ところが、そういう風に行き来すると

　間違えて部分的に消す
　位置が変わる

という残念なことがおきる。まぁ、いいどさ

agda の遅いのなんとかならんの?

それほど、でかいわけでもないんだが... check に数分ってのはなぁ

削ると速くなることは確かなんですが

沖縄の水

東京にいる間は、なんか便秘気味で。でも、沖縄では、わりとゆるゆる

やっぱり、水の違いなのかなぁ

それに馴染めないで、1年くらいで戻ってしまう人もいます

一方で、沖縄に住もうかなと思って、様子を見にきただけなのに、いきなり気に入ってしまい、そのまま住む人も

自分はトランク一つで沖縄に来て、まぁ、すぐに馴染んだ感じだな

浦添、宜野湾は、そんなに田舎じゃないので、車なしでもだいじょうぶだったし

P's squre の Cafe

なんか、West Field が復活してたので行ったら、本日休業

でも、上のシエルがお昼だけ営業してるのか。60人は入るんですが、がらがらだった

まぁ、インスタントな感じの料理でしたけど、空いてるカフェがいいならいいかも

https://www.ps-square.jp

agda update

沖縄に戻ってきました

Agda version 2.6.4.3 に上げたんですが、standard library が微妙に違う

開発版は 2.1 で現行は2.0 で、2.0 を修正していったら、なぜか 2.1 でも通るように

agda --library=standard-library-2.1 --include-path=.

とするらしい。2.0と2.1の関係は良くわからず

お墓参り

去年は台風でさぼったので。明日には戻るんですが、なんとなく寄ってきました

信心深いとかそういうわではないが、自分のため。あと一応自分で持ってるお墓だからな

お墓の周りのきまったお店によって、桶と花と線香をもらっていくだけ

そんなものでも続ける面白さはあるかも

なんか線香を付けるマッチもくれるけど、真っ白

なんでマッチ? ラベルも宣伝もなしですか

突然の同窓会

博士の同期の Marin Nilsson がスウェーデンから来るというので、そのためだけに東京に

横浜中華街でしたが、10人くらい。田中英彦先生にも会えました

ニルソンの娘さん二人も。日本語普通に話せてて素晴らしい

　「日本語やってもやらなくてもいいよ」

と言われていたらしいんですが、日本人の祖母とか母とかのスウェーデン語で話すようになって
それは良くないと思ったみたいなことを言ってました。それだけではないだろとは思うけど

「日本語勉強しなさい」と言われると嫌いに泣ってしまう人もいるみたいなのがあるらしい

ただ、スウェーデンには日本人が少ないらしく、日本語を学ぶのは難しいらしい。それはニルソンも
言ってたな

アニメとか見るのって聞いたけど、あんまりみないらしい。いや、僕も、10代後半とか、そんなに
テレビ観てなかったよ。他にやることたくさんあるからな

宮崎の青さぎは見たけど難しかったとか言ってたな

というわけで、娘さんたちといろいろ話して楽しかったかも

neovim update

brew upgrade neovim したら、なんか、colorscheme がおかしくなってしまって

どうも、defulat を変更するという技をだしたらしく

この機会に、新しい zellner 使うかって思ったんですが

　　agdaの黄色がでない

どいうこと? 実は、この黄色は Debug という color mode で、それは新しい zellner にはない。あっそ

で、なおしたんですが、vimrc が複数いろいろあって、どれを治すかでしらばくハマりました

シドバレット

あまり知られてない人のドキュメンタリー映画

ピンクフロイドは狂気からなので、シドバレットは、すでに「おかしくなってやめた人」という認識でした

2枚のアルバムはカナの影響で聴いてたけど

＊　すごいいい奴だったらしい

顔が良くて人が良くて、格好良くてギターが引けて、当時のサイケデリックブームの寵児

この辺の映像が割と良い。当時のブームの雰囲気がわかる

LSDの影響とかもあったが

＊　ピンクフロイドがメジャーになる時点で、おかしくなって抜けた

その後の二枚のアルバムはデビットギルモアがかなり手伝ったらしい(いい奴すぎる)

Wish you were here のアルバム作成のスタジオに現れたなんていうエピソードも

ギルモアは80年代/90年代に会いにいくべきだったみたいなことをいうけど、それはなぁ

でも、ちょっとシドのことがわかったのは良かった

https://eiga.com/movie/101385/

Zotero PDF path

論文管理用ですけどね。Mendeleyが、あんなになってしまったしなぁ

また、MindMap base のやつを使ってみたい気もするけど、今は Zotero

これが、iPhone と相性がよろしくない。iOS アプリもあるが、いつものパターンで、sign させて、Could Storage を使わせようというわけね

　　300 MB Free
　　2 GB $20
　　6 GB $60
　　Unlimited $120

どこも、そんな感じだが、「どこも」ってのが問題だよな。1箇所なら、まぁ容認するとしても、そこもあそこもってのはね

まぁ、結局、見たい分だけ、Good Reader に置いておけばよいわけで、あとは、どうやって取ってくるかだろ?

Terminus の sftp っていうってがあるらしく、あとは、Zotero の pdf path がわかればよい。ってことなら、

sqlite3 ですか。

SELECT
　itemData.itemID AS "Item ID",
　value AS "Item Title",
　path AS "File Path"
FROM
　itemData, itemDataValues, itemAttachments
WHERE
　itemAttachments.itemID = itemData.itemID
　AND itemDataValues.valueID = itemData.valueID
　AND itemDataValues.value LIKE ?
　AND itemAttachments.path IS NOT NULL
SQL

くらいで良いらしいんだが、でないものがある?!

WHERE
　itemAttachments.parentItemID = itemData.itemID

な場合があるのか。OR でつなげてもよい。もう少し工夫はいるけど、これでいいか

かたぶいな日

土砂降りと晴れ間と両方

沖縄にしては暑い日

でも、降ってる時は少し涼しめ

今後は、こういう日が増えていくのか?

ルックバック

FBの中で少し話題になってたので。短いのは良いね

よい話なんだが、そっちの方にいくのか

タイトルはそういう意味なのね

シネマQ限定は珍しい

良い話しなんだが、それが引っかかる。でも、それを含めて観るべきって感じでした

https://lookback-anime.com

Agda の --safe --cubical-compatible への書き換え

割と順調。ZFの書き換えは終わって、圏論の方。まぁ、主に

　functional extentionality

の部分ですね。

　　Extensionality : (a b : Level) → Set _
　　Extensionality a b =
　　　{A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
　　　(∀ x → f x ≡ g x) → f ≡ g

これらは、Free Theorem 排中律と同じで Agda で直接証明できない

あと、

　　≡-irr : { c₂ : Level}　{d : Set c₂ }　{ x y : d } ( eq eq' :　x　≡ y ) → eq ≡ eq'

これは、--with-K としないといけないらしい

仮定にすれば良いので、困るわけではないけど

これに合わせて修正ていくわけですが、見通しが良くなることは確か。全体的には影響しないんですが

　局所的には確かに短くなっているかも

ZF側は外延性の公理の関係だけで、だいたい通ったんですが、圏論の方がちょっと微妙で、全部取れるわけではないらしい

まぁ、でも良い感じかな

普天間宮の広場

綺麗になってましたが、単なる広場とトイレなのか。駐車場かと思ったけどそうではなかったのね

石平(いしんだ)側もなんとかするんだろうな

普天間宮のわっか

なんか、8の字に三回くぐれと

一応、くぐってきました