elpinal

https://cbult.space

elpinal

https://cbult.space

Twitterを試験的に再開

個人サイトやnote以外にも、しずかなインターネットというものがあることを思い出しました。しずかなインターネットのコンセプトには非常に共感できます。ここに、いくつか読んだ記事を載せておきます。 みんなの自分語りをどこかに置いといてほしい 12/26 コーヒー屋さん納めをした日の日記 自分を救うプログラミング 公開日記を書くということ また、極限まわりのnarrativeについて考えていました。Category theory in contextの話の流れが割と正解か

elpinal

    • ウェブとは何なのか

      昨日こういったサイトを見つけました。このサイトの著者は、15分おきに「何をしているか」や「何を思ったか」を記録しているみたいです。もしこれがSNSで投稿されていたら大して面白くなかったと思うんですが、これは個人サイトで投稿していることによる趣深さがあると思います。時間とテキスト以外の無駄なものがなく、投稿間の距離が狭いので圧縮されていて読みやすいですね。 一ヶ月くらい前からnoteで日記をたまに書いているんですが、自前のサイトでも公開するようにしました。理由は色々あった気が

      elpinal

      • 米田にすべてを任せてみれば、よかったりしないかな

        明示的構成ばかりを定義として使うと、証明のときに大変だと気づきました。関手性や自然性を何度も何度も証明しなきゃいけなくなり、とてもやってられないのです。たとえば元の圏は米田埋め込みを使ったコンマ圏と同値らしいので、今度からはもうちょっと抽象的な方法で圏を作るようにしてみます。そうすれば多分米田で殴っていけばなんとかなるんじゃないかと思います。圏論初心者らしい所が出てしまいました。 2つの圏が弱同値であるというのが、対象について本質的に全射な充満忠実関手が存在することなのか、

        elpinal

        • 高階論理でも型を構成したいときって、あるよね

          Isabelle/HOLにsubset typeないかな〜と思って「Isabelle/HOL subset type」とか「Isabelle/HOL comprehension」とかで調べていましたが、全然見つからず、最終的にtypedefがその役割を担っていることが分かりました。これがあれば集合から型を作れるので、便利です。 Isabelle/HOLには他にもquotient typeがあるのですが、これはeffectiveでしょうか、そうではないのでしょうか。いずれ確認

          elpinal

        Twitterを試験的に再開

        elpinal

          Heap (груда)とgroup (группа)

          heapというものがあって、heapから任意の元eを選んだら、eを単位元とする群が作れるらしいです。heapの圏から群の圏への関手を定義しようと思ったら、構成手法によってはpointed heapから成る充満部分圏を考えないといけないかもしれませんし、選択公理を仮定するならinhabitedでもいいかもしれません。ちなみに、pointed heapについて考えたときに射がbase pointを保存することまで要求してしまうと、群の圏と圏同値になってしまう予感がします。 co

          elpinal

          Heap (груда)とgroup (группа)

          elpinal

          Contextだとか

          最近はcontextこと"Category theory in context"を読んでいます。私は元々、ベーシック圏論を超スピードで流し読みし、その後にSGL (Sheaves in geometry and logic)のcategorical preliminariesを読むことで圏論に入門したので、圏論をちゃんと学んだとはいえない状態だったのです。「右随伴が極限を保存することは知っているけど、その証明はやったことがない」とかそんな感じで、とても磐石な理解には到達してい

          elpinal

          Contextだとか

          elpinal