/dragoon8192-main/右普遍射

generated at 2/18/2025, 5:43:38 PM
右普遍射
 \left\lang dR, dε \right\rangが函手L \colon C \to Dから対象d \colon Dへの(右)普遍射
\iff \left\lang\textrm{R-univ}\colon C, D; L, d, dR; d\varepsilon \right\rang
where
dR\colon C
dε\colon dR.L → d 
Axiom
\forall c, f\colon c.L→ d
\exist ! g \colon  c→dR, \
(g.L);d\varepsilon = f
コンマ圏L↓d^♯の終対象と同一視できる
\left\lang\textrm{R-univ}\colon C, D; L, d, dR; d\varepsilon \right\rang
\iff \left\lang dR, *; d\varepsilon \right\rang \cong \operatorname{term} (L↓d^♯)
このとき、終対象への射が普遍性を担う
!=\left\lang g, *^\wedge \right\rang \colon \left\lang c, *; f \right\rang  → \left\lang dR, *; d\varepsilon \right\rang
R-Univ.sig 2-signature <R-Univ: C, D; L, d, dR; dε> in CAT
   Data
     0-morph C
     0-morph D
     1-morph L : C -> D
     1-morph d : %I -> D
     
     1-morph dR : %I -> C
     2-morph dε
       : dR * L => d
       : %I -> D
   Axioms
     3-formula
       ∀ c : %I -> C
       ∀ f : c * L => d
       ∃! f' : c => dR
       (f' * L) ; dε = f