指標
ある圏において対象と射、公理の組み合わせる決まり事
このScrapboxでは指標を
日本語による列挙または
sig擬似言語で表す
案:先に指標実例の圏を用意する、という構成法は？
例としてモノイダル圏のような
template.sig2-signature Sig
fixed-in <Cat,×,I>
Data
0-morph c : Cat
1-morph m : c × c → c
1-morph i : I → c
2-iso associator @ α
: (m × c^) * m ⇒ (c^ × m) * m
: c × c × c → c
2-iso l-unitor @ λ
: (i × c^) * m ⇒ c^
: c → c
2-iso r-unitor @ ρ
: (c^ × i) * m ⇒ c^
: c → c
Axioms
3-eq暫定
公理系も並べるよ
分ける流儀もある
大文字小文字
上の世界の事柄だけ大文字にしたいけど
ごちゃつく
上の世界から持ってきた……という意味の接頭記号を作る？
もう一つ上のも想定されることがある……
fixed-in 一般のin Cの場合と、指定のものの場合があるけど、どうしようかな……
in Set
in CAT
fixed とかにする？
考え中
左右は混ざりがち
全称限量子はpoint-free化すればいいことが多い
一意性もなんとか……
類語
まだちゃんと読んでない