普遍射
ちょっと文字がわかりづらいかな……
随伴系から天下りで記号を定めている
右随伴函手を構築するための方を右普遍射
L-Univ.sigsig L-Universal in CAT
Data
0-morph C
0-morph D
1-morph c : &I -> C
1-morph R : D -> C
1-morph cL : &I -> D
2-morph cμ
: c => cL * R
: I -> C
Axioms
3-formula
∀ d : I -> D
g : c => d * R
∃! Q(d,g) : cL => d
cμ ; (Q(d,g) * R) = g定義