2024/2/25 直和とか直積とかよくわからんくなってきた
2つの文脈でよくわからさが出てきたmrsekut.icon
依存型理論の文脈
記号の表記揺れ？理解の誤り？
「依存積」と「依存直積」を同じものとみなしていたがどうやら違うっぽい？
圏論の文脈
和、直和、積、直積、ってなんだっけというのを復習しようとしたら余計にわからなくなった
直和
direct sum
圏論的直和
coproduct
余積
双対直積
なんで、直和のことを「coproduct」と訳する？
先にこっちを解消したほうが良さそう
圏論の文脈の方の整理
良い機会なので、改めてこの辺のキーワードをちゃんと整理したい
和
sum
直和
direct sum
Direct sums and weak direct products
weak direct productsとは #?? 3種類ある
集合的直和→非交和
代数的直和
圏論的直和→余積?
積
product
圏論的積とは
直積
direct product?
そもそも「direct」「直」ってなんだんだ #?? 積と直積が異なるものを指す時はどういうとき #?? 余積
coproduct
圏論的直和?
日本語を使っているからややこしくなっていたりする？
全部英語のキーワードを使うとマシになったりする？
どういう順序で整理すべきなのかもわからないmrsekut.icon
みんなの圏論 3.1でも読むか
依存型理論の文脈の方の整理
dependent productを、
これがそもぞも誤っていたりする？
依存積
dependent sum?
関数の一般化?
依存直積、依存和
dependent product
『論理と計算のしくみ』.iconではΣを使っている
直積の一般化?
「直積」と「和」が同じものを指すとはどういうことなのか #?? 依存直和
dependent coproduct
依存関数型
dependent function type
『論理と計算のしくみ』.iconではΠを使っている
Wikipediayukikurage.icon
A function whose type of return value varies with its argument (i.e. there is no fixed codomain) is a dependent function and the type of this function is called dependent product type, pi-type (Π type) or dependent function type.
The dual of the dependent product type is the dependent pair type, dependent sum type, sigma-type, or (confusingly) dependent product type.
(confusingly) と言われているw
完全に表記揺れそう
pi型, sigma型と言っておけば語弊なく伝わりそう
pi型
関数の一般化
Π_{n=1..a}b = b ^ a
依存関数
依存積
sigma型
直積の一般化
Σ_{n=1..a}b = a × b
依存積
依存和
これに加えて「積/直積」、「和/直和」も表記揺れ(圏論では同じ意味)していて、地獄の様相 といった感じか
つらいmrsekut.icon
直和(圏論的和)が余積と呼ばれるのは、圏論的積の定義に置ける矢印の向きを全部逆にすれば圏論的和になるから(双対概念)
依存的な積/和がどう圏論に対応するのか知らない
ある対象の要素で indexed された対象全ての積/和
indexed された、とはどう表現できるか