普遍射
summary.icon
ちょっと文字がわかりづらいかな……
右随伴函手を構築するための方を右普遍射
code:L-Univ.sig
sig 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
定義