以下雑なメモ
具体的にそれがなにかは置いといて関係性に注目する
対象と射
命題を点、証明を矢印で表すのおもろい
射の合成と恒等射が成立すれば圏らしい
繰り返しになりますが圏論では具体的なものは無視して、射によって示される関係だけに注目し、矢印の構造が同じであれば実質的に同じものとして扱います。例えば、もしある未知の命題 X があって、それが二等辺三角形と全く同じ矢印の出入りを持っているなら、その X は実質的に「二等辺三角形と同等なもの」として扱えます。
めっちゃインターフェース？
どんな2つを比べても必ず順位がつく（一直線に並ぶ）」のが全順序で、「比較できるものもあるが、そもそも無関係（比較不能）なものも許容する（枝分かれする）」のが半順序
代入可能であるを射とするときに Duck typing を採用するものが前順序で、 Nominal typing を採用するものが半順序
前者 TypeScript とか、 後者 CSharp とか
混乱しそうになったら射を強く意識する
集合は対象だけ、圏は対象と射がある
シンプルに対象の関係性を意識しないのが集合といった感じかな
ちなみに自分から自分への射が圏には必要（恒等射）なので射が１つもない圏はあり得ない
集合の要素を対象という言い方はしないかもだけど
1つの圏には1つの射の定義じゃないと射の合成が成立しなくて詰む、異なる射同士の圏は関手でつなぐらしい
まあともあれふわっと理解、活用してるものをちゃんと理論立てて考え抜いてくれてありがとうだなぁ
順番で言うと逆だけどね、考え抜かれたものを応用したものをちゃんと言語化しなくても使えてるという状態があるだけですね
型システム