2021-01-19_#1
ふりかえり用アセット
見てきた範囲
参加者によるメモ
関数 という用語は誤解を招きやすいと感じた。
プログラマ的には、何等かの実装のあるメソッドのようなイメージを抱きやすい
高校数学までだと、例えば$ y = x^2のグラフと関数を混同している例をよく見かける
Re: いっそ 型とプログラムの圏 と書いた方が、誤解が少ないまでありますね 🤔 (1 回目)
しりとりの圏に対して、射の合成の記号が不自然な印象を受ける
「りんご」の射$ fに続けて「ごりら」の射$ gを合成した射を$ g \circ fを記述するが、これは「ごりら$ \circりんご」となってしまっている。「りんご$ \circごりら」で「りんごりら」の方が自然ではないか
あるいはしりとりのルールを「後ろに言葉を続ける」ではなく、「りんご」に対して前に「パリ」→「らっぱ」と続けるルールに改定すると、合成記号として自然な見た目になる気がする
Re: 合成記号の記述がなぜこうなるか？という点に関しては、この辺 を見ていただくと納得できるかも知れません 📋 ただ、わざわざ$ \circという記号を使わない流儀もあって、その場合は人間にとって直感的な記述が可能だったりします
e.g. $ \gggという記号を用いて、$ fに続けて$ gを用いる合成射を$ f \ggg gと表すなど
残っている疑問・質問事項
$ \mathrm{Hom}(B, X)の元$ bに対して、右から$ f : A \rightarrow Bを作用させることで$ \mathrm{Hom}(A, X)の元$ a = b \circ fも考えられるのでは？
$ *をどこにも移さないという場合は考えないの？
Re: 集合論的な関数では、必ず基点となる集合の中身に対して、すべての写し先を考える必要があるので、そのようなケースは考えません
合成射の定義を「単語の最後の文字 & 単語の最初の文字をつなげて、新しく単語をつくる」とする場合は、対象に現れる ひらがなそのものが恒等射 になります
e.g. ご$ \circりんご = りんご，ごりら$ \circご = ごりら，∴ 恒等射の性質を満たす
合成射の定義を「単語を単純にならべ、新しく単語をつくる」とする場合は、パス (無単語) が恒等射 になります
e.g. (パス)$ \circりんご = りんご，ごりら$ \circ(パス) = ごりら，∴ 恒等射の性質を満たす
このトピック，正直初学者向けの記事が (自分の確認する限り) 世の中に存在しないので、どうしたものか感です 😇
おっしゃる通り、集合論における関数の同値性は外延性の公理から言えますが、ラムダ計算の同値性は決定不能命題でかつ、外延性の公理から与えられるものでは無いですよね 👍
なので、型と関数の圏における射の同値性は、やはり集合論の尺度では測っちゃダメなわけです
いっそ 型とプログラムの圏 と書いた方が、誤解が少ないまでありますね 🤔 (2 回目)
前提として、自分自身に伸びる矢印 (射) ＝ 恒等射，とは限らない ということを考慮する必要があったりします 🤔
自分自身に伸びる矢印 (射) であって、なおかつ特殊なショートカットが作れる ＝ 恒等射 という考え方なので、その意味では increment は 特殊なショートカットが作れない ので、恒等射では無いということになりますね