elpinal
記事一覧
Twitterを試験的に再開
個人サイトやnote以外にも、しずかなインターネットというものがあることを思い出しました。しずかなインターネットのコンセプトには非常に共感できます。ここに、いくつか読んだ記事を載せておきます。
みんなの自分語りをどこかに置いといてほしい
12/26 コーヒー屋さん納めをした日の日記
自分を救うプログラミング
公開日記を書くということ
また、極限まわりのnarrativeについて考えていま
米田にすべてを任せてみれば、よかったりしないかな
明示的構成ばかりを定義として使うと、証明のときに大変だと気づきました。関手性や自然性を何度も何度も証明しなきゃいけなくなり、とてもやってられないのです。たとえば元の圏は米田埋め込みを使ったコンマ圏と同値らしいので、今度からはもうちょっと抽象的な方法で圏を作るようにしてみます。そうすれば多分米田で殴っていけばなんとかなるんじゃないかと思います。圏論初心者らしい所が出てしまいました。
2つの圏が弱同
高階論理でも型を構成したいときって、あるよね
Isabelle/HOLにsubset typeないかな〜と思って「Isabelle/HOL subset type」とか「Isabelle/HOL comprehension」とかで調べていましたが、全然見つからず、最終的にtypedefがその役割を担っていることが分かりました。これがあれば集合から型を作れるので、便利です。
Isabelle/HOLには他にもquotient typeがあるの
Heap (груда)とgroup (группа)
heapというものがあって、heapから任意の元eを選んだら、eを単位元とする群が作れるらしいです。heapの圏から群の圏への関手を定義しようと思ったら、構成手法によってはpointed heapから成る充満部分圏を考えないといけないかもしれませんし、選択公理を仮定するならinhabitedでもいいかもしれません。ちなみに、pointed heapについて考えたときに射がbase pointを保存
もっとみる