右普遍射

$ \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

https://gyazo.com/df5c6bb240f1d8c236b830bf4d1a9cc0

equal.icon

$ \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

signature.icon

code: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