Seeker's eye
Thursday, 3 April 2025
Wednesday, 2 April 2025
Graph から CCC の普遍問題
Graph から CCC を作るのはできたので、普遍問題をやってるんだが
直積やCurry化の構造は、グラフ/公理の外にある
なので、その部分は「単にコピーするだけ」になるらしい
確かに、元の圏 A と、そのCCC である CCC A は別なので、まぁ、そうなんだけど
なので、CCC functor が単なる普通の関手でいいことに。なんだそれ? それでいいのか?
直積やCurry化の構造は、グラフ/公理の外にある
なので、その部分は「単にコピーするだけ」になるらしい
確かに、元の圏 A と、そのCCC である CCC A は別なので、まぁ、そうなんだけど
なので、CCC functor が単なる普通の関手でいいことに。なんだそれ? それでいいのか?
Tuesday, 1 April 2025
Graph からCCC
昔、Graph から圏はできたんだが、CCCをPostive logic経由で作るっ4てのができなくて、
Sets への関手を作って終わらすって技を出してたんですが、
それだと、Setsの部分圏がCCCになってるかどうかわからない
なので、その関手の値が等しいという等号を使ってCCCを直接証明するというのを考えた
Lambek には「Minimum Equivalenceを定義する」とか書いてあるんですが、定義の仕方がわからん
f ≐ g → h ≐ i → (h ∙ f) ≐ (i ∙ g)
という resp ってのを示すのに苦労してたんですが、 (f ≐ g) → (f ≡ g)を使うのかと思ったんだが、
○ ⊤ と id ⊤ は同じなので、よろしくない。なんだか関手は
fmap (g ∙ f) z ≡ fmap g (fmap f z)
という分配則があって、それを使うと証明できた。そういうことなのか
それで圏になったので、CCCを示すんだが、大体は refl でいける。ところが、
e4b-lem : {a b c : Obj PLC} {k : Hom PLC c (a <= b)} → PLC [ iv ((PLC [ iv ε (id ((a <= b) ∧ b))
o < PLC [ k o iv π (id (c ∧ b)) ] , iv π' (id (c ∧ b)) > ]) *) (id c) ≈ k ]
が、うまくいかない。でもじっとみてると
関数外延性を仮定するといける
らしい。SetsのCCCでも *-cong を示すには関数外延性を仮定する。なので、必要ならしいです
で、まぁ、Graph から CCC はできた。
https://github.com/shinji-kono/category-exercise-in-agda/blob/e6cb3a1b8e9cadd3e17125fd999a61809665ab30/src/CCCGraph.agda
このあと、この構成が普遍問題の解であることを示す必要があるらしい。情報は落としてないのでいけるはずだが、できるかどうかは
で、これを使って Polynominal 圏が作れるはず。Comonoad でも示してるんだが、関数完全性が微妙にずれてる
Sets への関手を作って終わらすって技を出してたんですが、
それだと、Setsの部分圏がCCCになってるかどうかわからない
なので、その関手の値が等しいという等号を使ってCCCを直接証明するというのを考えた
Lambek には「Minimum Equivalenceを定義する」とか書いてあるんですが、定義の仕方がわからん
f ≐ g → h ≐ i → (h ∙ f) ≐ (i ∙ g)
という resp ってのを示すのに苦労してたんですが、 (f ≐ g) → (f ≡ g)を使うのかと思ったんだが、
○ ⊤ と id ⊤ は同じなので、よろしくない。なんだか関手は
fmap (g ∙ f) z ≡ fmap g (fmap f z)
という分配則があって、それを使うと証明できた。そういうことなのか
それで圏になったので、CCCを示すんだが、大体は refl でいける。ところが、
e4b-lem : {a b c : Obj PLC} {k : Hom PLC c (a <= b)} → PLC [ iv ((PLC [ iv ε (id ((a <= b) ∧ b))
o < PLC [ k o iv π (id (c ∧ b)) ] , iv π' (id (c ∧ b)) > ]) *) (id c) ≈ k ]
が、うまくいかない。でもじっとみてると
関数外延性を仮定するといける
らしい。SetsのCCCでも *-cong を示すには関数外延性を仮定する。なので、必要ならしいです
で、まぁ、Graph から CCC はできた。
https://github.com/shinji-kono/category-exercise-in-agda/blob/e6cb3a1b8e9cadd3e17125fd999a61809665ab30/src/CCCGraph.agda
このあと、この構成が普遍問題の解であることを示す必要があるらしい。情報は落としてないのでいけるはずだが、できるかどうかは
で、これを使って Polynominal 圏が作れるはず。Comonoad でも示してるんだが、関数完全性が微妙にずれてる
Friday, 28 March 2025
Wednesday, 26 March 2025
kea-dhcp6
設定は終わって、動作の確認してるんだが
MacBook Air のAnkderのアダプタ
はぜんぜん認識しない。なんだが、Apple TVとかが応答していることに気がついた
keadhcpdev=# select * from lease6;
address | duid | valid_lifetime | expire | subnet_id | pref_lifetime | lease_type | iaid | prefix_len | fqdn_fwd | fqdn_rev | hostname | state | hwaddr | hwtype | hwaddr_source | user_context | pool_id
--------------------------------------+--------------------------------+----------------+------------------------+-----------+---------------+------------+------------+------------+----------+----------+--------------------------------------+-------+----------------+--------+---------------+--------------+---------
2001:2f8:1c:a504:f66e:24ff:fe2e:5a56 | \x000100012abc87eaf46e24eeeee | 4000 | 2025-03-26 09:05:48+00 | 1 | 3000 | 0 | 116682276 | 128 | f | f | nec01.st.ie.u-ryukyu.ac.jp. | 0 | \xf46e242eeeee| 1 | 2 | | 0
2001:2f8:1c:a504:92dd:5dff:febc:47f6 | \x000100012f67adef90dd5eeeee6 | 4000 | 2025-03-26 09:05:50+00 | 1 | 3000 | 0 | 0 | 128 | f | f | cr-appleTV.cr.ie.u-ryukyu.ac.jp | 0 | \x90dd5deeeee | 1 | 2 | | 0
2001:2f8:1c:a504:23e:e1ff:febe:5752 | \x0003000100113267ae08 | 4000 | 2025-03-26 09:05:51+00 | 1 | 3000 | 0 | 845655560 | 128 | f | f | H-Dunaro.sys.ie.u-ryukyu.ac.jp. | 0 | \x001132eeeee | 1 | 2 | | 0
2001:2f8:1c:a504:7aca:39ff:fefb:d1e3 | \x00020000ab11d20eefd3feeeee0 | 4000 | 2025-03-26 09:06:05+00 | 1 | 3000 | 0 | -158979025 | 128 | f | f | darjeeling.tea.ie.u-ryukyu.ac.jp. | 0 | \xb8cb29eeeee | 1 | 4 | | 0
ってことは基本的なところは動いているのか...
まぁ、いいか、ここまでで
MacBook Air のAnkderのアダプタ
はぜんぜん認識しない。なんだが、Apple TVとかが応答していることに気がついた
keadhcpdev=# select * from lease6;
address | duid | valid_lifetime | expire | subnet_id | pref_lifetime | lease_type | iaid | prefix_len | fqdn_fwd | fqdn_rev | hostname | state | hwaddr | hwtype | hwaddr_source | user_context | pool_id
--------------------------------------+--------------------------------+----------------+------------------------+-----------+---------------+------------+------------+------------+----------+----------+--------------------------------------+-------+----------------+--------+---------------+--------------+---------
2001:2f8:1c:a504:f66e:24ff:fe2e:5a56 | \x000100012abc87eaf46e24eeeee | 4000 | 2025-03-26 09:05:48+00 | 1 | 3000 | 0 | 116682276 | 128 | f | f | nec01.st.ie.u-ryukyu.ac.jp. | 0 | \xf46e242eeeee| 1 | 2 | | 0
2001:2f8:1c:a504:92dd:5dff:febc:47f6 | \x000100012f67adef90dd5eeeee6 | 4000 | 2025-03-26 09:05:50+00 | 1 | 3000 | 0 | 0 | 128 | f | f | cr-appleTV.cr.ie.u-ryukyu.ac.jp | 0 | \x90dd5deeeee | 1 | 2 | | 0
2001:2f8:1c:a504:23e:e1ff:febe:5752 | \x0003000100113267ae08 | 4000 | 2025-03-26 09:05:51+00 | 1 | 3000 | 0 | 845655560 | 128 | f | f | H-Dunaro.sys.ie.u-ryukyu.ac.jp. | 0 | \x001132eeeee | 1 | 2 | | 0
2001:2f8:1c:a504:7aca:39ff:fefb:d1e3 | \x00020000ab11d20eefd3feeeee0 | 4000 | 2025-03-26 09:06:05+00 | 1 | 3000 | 0 | -158979025 | 128 | f | f | darjeeling.tea.ie.u-ryukyu.ac.jp. | 0 | \xb8cb29eeeee | 1 | 4 | | 0
ってことは基本的なところは動いているのか...
まぁ、いいか、ここまでで
Monday, 24 March 2025
飲み会week
まぁ、禁酒中なので自分は飲み過ぎはないんだけどね
木曜日から、金曜日は加藤食堂で小渡さん山田さん白土さんと。土曜日は並列信頼研のOBたちと。日曜日はパーティで。
月曜日にみんな帰るみたいな感じ
まぁ、誰にも声かけなかったんですが、FBに書いた人たちとか、それをかぎつけた人たちとか。お疲れ様です
人をネタに酒を飲むのはうまかろう
けど、さすがに疲れたことは確かだな
木曜日から、金曜日は加藤食堂で小渡さん山田さん白土さんと。土曜日は並列信頼研のOBたちと。日曜日はパーティで。
月曜日にみんな帰るみたいな感じ
まぁ、誰にも声かけなかったんですが、FBに書いた人たちとか、それをかぎつけた人たちとか。お疲れ様です
人をネタに酒を飲むのはうまかろう
けど、さすがに疲れたことは確かだな
Subscribe to:
Posts (Atom)