圏論の並進式の提案

並進式【translational notation】を検討・提案する。

特徴
- 圏論の各記法と関連付けがし易い。実際それらにインスパイアされた。
  - 二方向規則【two-way rule、竹内による式の表示法】
  - ストリング図【string diagram】
  - 可換図式【commutative diagram】
  - 箙表現
  - ハッセ図
  - 数式
  - 結合の文章順記法【operation sequence as text sequence】
- テキスト形式(メモ帳アプリなど)で記載し、そのまま、または $\TeX$ ソースでも可読性がある。

今回は以下のルールにしています。好みで変更することも可能ですが、全体の整合性を保持するのに考慮が必要です。

```math
\newcommand\sets{\mathrm{Set}}
\newcommand\op{^{\mathrm{op}}}
\newcommand\iv{^{-1}}
\newcommand\⇨{\text{⇨}} % 関手
\newcommand\➡{\text{➡}} % 自然変換
\newcommand\cone{\mathrm{Cone}}
\newcommand\cocone{\mathrm{Cocone}}
\newcommand\colim{\mathrm{colim}}
\newcommand\lett{\,\text{let}\,}
\newcommand\and{\,\text{and}\,}
\newcommand\st{\,\text{s.t.}\,} % such that
\newcommand\ie{\,\text{i.e.}\,}
```

```math
\newcommand\eq[1]{\begin{array}{}#1\end{array}} % 式
\newcommand\a[1]{&[#1]&} % 射
\newcommand\so{⋯} % 省略対象
\newcommand\sa{&⋯&} % 省略射
\newcommand\spn{&\|&} % 並進を跨った射
\newcommand\h{&[\ ]&} % ホムセット
\newcommand\p[1]{\langle #1 \rangle} % 直積
\newcommand\ap[1]{&[\langle #1 \rangle]&} % 直積の射
\renewcommand\i[1]{&[1_{#1}]&} % 恒等射(規定の文字の定義を上書き)
\newcommand\t[1]{[\![#1]\!]} % 並進式(規定の文字の定義を上書き)
```

|オブジェクト|並進式の方向|式の方向|式の結合記号|
|--|--|--|--|
|直積|上→下|左→右|$\p{a,b}$|
|射|左→右|左→右|$f⨾g$|
|垂直合成|左→右|左←右|$G∘F$|
|水平合成|上←下|左←右|$G∙F$|
|自然変換|左→右|左→右|$n⨾m$|

## 並進式の検証

対象と射と圏
※射と矢を大かっこでくくるのは、ストリング図の影響です。
```math
\eq{
\text{対象}&\text{射}→&\text{対象}&\text{圏}\\
\text{頂点}&\text{矢}→&\text{頂点}&\text{箙}&\text{:説明用}\\ \hdashline
a \a{f} b &∈A \\
}
```
またはケットを流用する。※本投稿では使用しない。
```math
\eq{
a &|f \rangle& b &∈A \\
}
```
これは以下を意味する。
```math
\eq{
\text{射}&\text{対象}& &\text{対象}&\text{圏}\\ \hdashline
f:& a &→& b &∈A \\
}
```

射の合成、箙上の道
```math
\eq{
&  a \a{f &⨾& g} c \\
:=&a \a{f}b\a{g} c \\
}
```

射の結合律
```math
\eq{
&  a \a{(f &⨾&     g) &⨾& h}  d \\
=& a((\a{f} b  \a{g})c \a{h}) d \\
=& a  \a{f} b  \a{g} c \a{h}  d \\
=& a (\a{f} b (\a{g} c \a{h}))d \\
=& a  \a{f &⨾&    (g  &⨾& h )}d \\
}
```

可換図式は、先頭対象同士と末尾対象同士が同一の、2個の並進式の等式で表現される。
```math
\eq{
&  a \a{f} b \a{g} d \\
=& a \a{h} c \a{k} d \\
}
```
または、先頭対象と末尾対象を、罫線文字を用いてつなげる。※本投稿では使用しない。
```math
\eq{
&           a \a{f} b \a{g} \text{┐} \\
↺& \text{└} \a{h} c \a{k} d \\
}
```

恒等射
```math
\eq{
&  b \i{b} b  \\
=& b \a{b} b  &\text{※1}\\
=& b \sa   \so &\text{※2}\\
=&\so \sa   b  &\text{※2}\\
}
```
※1 恒等射を対象と同一視して表記を合わせることが可能。
※2 同じ対象と射を省略可能(本投稿ではアンダースコア)。ストリング図の縦線に対応。

恒等射のスライディング則
```math
\eq{
&  a \a{f &⨾& 1_b}  b \\
=& a \a{f}   b  \i{b} b \\
=& a \a{f}   b  \sa   \so \\
=&\so \sa     a  \a{f} b \\
=& a \i{a}   a  \a{f} b \\
=& a \a{1_a &⨾& f}  b \\
}
```

モノ
```math
\eq{
&    &∀&    &\text{is mono}\\
&  a \a{x} b \a{f} c \\
=& a \a{y} b \a{f} c \\
⟹&a \a{x} b \\
=& a \a{y} b \\
}
```

エピ
```math
\eq{
&    &\text{is epi}&    &∀ \\
&  a \a{f} b \a{x} c \\
=& a \a{f} b \a{y} c \\
⟹&  &&    b \a{x} c \\
=&   &&    b \a{y} c \\
}
```

分裂エピモノ性
```math
\eq{
&    &&   b \a{m} a \a{e} b && \\
=&   &&   b \i{b}   &&    b && \\ \hdashline
\lett&&&     &&    a \a{e} b \a{x} c \\
=&   &&             &&    a \a{e} b \a{x} c \\ \hdashline
∴&  &&     &&      &&    b \a{x} c \\
=&   &&   b &&      \i{b} b \a{x} c && \\
=&   &&   b \a{m} a \a{e} b \a{x} c \\
=&   &&   b \a{m} a \a{e} b \a{y} c \\
=&   &&   b &&      \i{b} b \a{y} c \\
=&   &&     &&      &&    b \a{y} c \\ \hdashline
\lett&c \a{x} b \a{m} a \\
=&c \a{y} b \a{m} a \\ \hdashline
∴
& c \a{x} b &&      &&      \\
=&c \a{x} b \i{b}   &&    b \\
=&c \a{x} b \a{m} a \a{e} b \\
=&c \a{y} b \a{m} a \a{e} b \\
=&c \a{y} b \i{b}   &&    b \\
& c \a{y} b &&      &&      \\
}
```

逆射、同型
```math
\eq{
&     a \a{f} b \a{g} a \\
=&    a &&      \i{a} a \\
\and&   &&    b \a{g} a \a{f} b \\
=&      &&    b \i{b}   &&    b \\
}
```

終対象
```math
\eq{
& 1∀ &2∃!& & \text{※}\\
& a   \a{h}  1 \\
}
```
※述語論理の量化子の前に数値で順序を付け、並進式の順序と独立させる。

始対象
```math
\eq{
&   &2∃!& 1∀\\
& 0 \a{h}  a \\
}
```

集合の要素は終対象(1点集合)からの射と同一視が可能。
```math
\eq{
& \{*\} \a{a} A  &∈\sets \\
⟺&     &a∈& A  &∈\sets \\
}
```

双対圏
```math
\eq{
&   c \a{g} b  \a{f} a &∈A\op \\
=&  c \a{g &⨾& f}  a &∈A\op \\ \hdashline
⟺&a \a{f} b  \a{g} c &∈A \\
=&  a \a{f &⨾& g}  c &∈A \\
}
```

圏の直積
```math
\eq{
&\p{a,a'}\ap{f,f'}\p{b,b'}&∈A×B \\
=&\p{ a   \a{f}      b    &∈A \\
&,    a'  \a{f'}     b'  }&∈B \\
}
```

圏の直積の合成
```math
\eq{
& \p{a,a'} \a{\p{f,f'} &⨾& \p{g,g'}}\p{c,c'}&∈A×B \\
=&\p{a,a'} \ap{f,f'}\p{b,b'}\ap{g,g'} \p{c,c'}&∈A×B \\
=&\p{  a      \a{f}     b    \a{g}       c    &∈A \\
&,     a'     \a{f'}    b'   \a{g'}      c'  }&∈B \\
=&\p{  a      \a{f     &⨾&    g}       c    &∈A \\
&,     a'     \a{f'    &⨾&    g'}      c'  }&∈B \\
=&\p{a,a'} \a{\p{f⨾g &,& f'⨾g'}}  \p{c,c'}&∈A×B \\
}
```

圏の直積のスライディング則
```math
\eq{
& \p{a,a'}\a{\p{f,1_{a'}} &⨾&\p{1_b,f'}}\p{b,b'}&∈A×B \\
=&\p{a,a'}\ap{f,1_{a'}}\p{b,a'}\ap{1_b,f'}\p{b,b'}&∈A×B \\
=&\p{  a   \a{f}          b      \i{b}       b    &∈A \\
&,     a'  \i{a'}         a'     \a{f'}      b'  }&∈B \\ \hdashline
=&\p{  a   \a{f}                   &&        b    &∈A \\
&,     a'     &&                 \a{f'}      b'  }&∈B \\
=&\p{a,a'}    &&                \ap{f,f'} \p{b,b'}&∈A×B \\
=&\p{  a      &&                 \a{f}       b    &∈A \\
&,     a'  \a{f'}                  &&        b'  }&∈B \\ \hdashline
=&\p{  a   \i{a}          a      \a{f}       b    &∈A \\
&,     a'  \a{f'}         b'     \i{b'}      b'  }&∈B \\
=&\p{a,a'}\ap{1_a,f'}\p{a,b'}\ap{f,1_{b'}}\p{b,b'}&∈A×B \\
=&\p{a,a'}\a{\p{1_a,f'} &⨾&\p{f,1_{b'}}}\p{b,b'}&∈A×B \\
}
```

関手 $F:A\➡B$
```math
\eq{
&\t{ F \sa    \so &∈B^A &\text{※}\\
&,   a \a{f}  b }&∈A \\
=&\t{F &F&    F  &∈B^A \\
&,   a \a{f}  b }&∈A \\
=&  Fa \a{Ff} Fb &∈B \\ \hdashline
=&\t{F &&        &∈B^A \\
&,  (a \a{f}  b)}&∈A \\
=& F(a \a{f}  b) &∈B \\
}
```
※同じ関手(対象)と恒等自然変換(射)を省略可能。ストリング図の縦線に対応。

関手の凖同型
```math
\eq{
&\t{  F \sa           &&   \so &∈B^A \\
&,    a \a{f   &⨾&  g}   c} &∈A \\
=&   Fa \a{F(f &⨾&  g)}  Fc &∈B \\ \hdashline
=&\t{ F  \sa     \so \sa      \so &∈B^A \\
&,    x \a{f}   b  \a{g}   c} &∈A \\
=&   Fa \a{Ff}  Fb \a{Fg}  Fc &∈B \\ \hdashline
=&\t{ F  \sa         \sa     \so &∈B^A \\
&,    a \a{f   &⨾&  g}   c} &∈A \\
=&   Fa \a{Ff  &⨾&  Fg}  Fc &∈B \\ \hdashline
=&\t{ F    &&         &&      &∈B^A \\
&,    x \a{f}   b  \a{g}   c} &∈A \\
=&  F(a \a{f}   b  \a{g}   c) &∈B \\
}
```

関手は恒等射を恒等射に移す
```math
\eq{
&   Fa \a{F(1_a)} Fa &∈B \\
=&\t{F \sa        \so &∈B^A\\
&,   a \i{a}      a }&∈A \\
=&  Fa \i{Fa}     Fa &∈B \\
=&  Fa \a{Fa}     Fa &∈B \\
=&  Fa \sa        \so &∈B \\
}
```

恒等関手
```math
\eq{
&\p{1_A \sa   \so &∈A^A \\
&,  a   \a{f} b }&∈A \\
=&  a   \a{f} b  &∈A \\
}
```

双関手 $F:A×B\➡C$
```math
\eq{&\t{ F   \sa            \so      &∈C^{A×B} \\
& , \p{a,a'} \ap{f,f'}      \p{b,b'} &∈A×B \\
=&,F\p{a,a'} \a{F\p{f,f'}}F \p{b,b'}}&∈C \\ \hdashline
=&\t{    F   \sa            \so      &∈C^{A×B} \\
&,\p{    a   \a{f}          b        &∈A \\
&,       a'  \a{f'}         b'     }}&∈B \\
}
```

双関手の一意性：各圏の対象を固定した、ある性質を満たす関手 $F,G$ で $T$ 一つに決まる。
```math
\eq{
=&T\p{a,a'} \a{T\p{f,f'}} && T\p{b,b'} \\
&\t{ T  \sa      &&    \so \\
&,   a  \a{f}    &&    b \\
&,   a' \a{f'}   &&    b'}\\
=&\t{T  \sa   \so \sa   \so \\
&,   a  \a{f} b  \sa   \so \\
&,   \so \sa   a' \a{f'} b'}\\
=&T\p{a,a'} \a{G_{a'}f} T\p{b,a'} \a{F_bf'} T\p{b,b'} \\
}
```
双関手の準同型。ある性質とは、以下の等式の括弧内の等式性。
```math
\eq{
& T\p{a,b} \a{T\p{f&⨾&g&,&f'&⨾&g'}} T\p{c,c'} \\
=&T\p{a,a'} \a{G_{a'}(f&⨾&g)} T\p{c,a'} \a{F_b(f'&⨾&g')} T\p{c,c'} \\
=&T\p{a,a'} \a{G_{a'}f} (T\p{b,a'} \a{G_{a'}g} T\p{c,a'} \a{F_cf'} T\p{c,b'}) \a{F_cg'} T\p{c,c'} \\
=&T\p{a,a'} \a{G_{a'}f} (T\p{b,a'} \a{F_bf'} T\p{b,b'} \a{G_{b'}g} T\p{c,b'}) \a{F_cg'} T\p{c,c'} \\
=&T\p{a,a'} \a{T\p{f&,&f'}}  T\p{b,b'} \a{T\p{g&,&g'}} T\p{c,c'} \\
}
```

自然変換 $n:F\⇨G$ (対象への作用)
```math
\eq{
&      F \a{n}   G      &∈B^A \\
=&\{\t{F \a{n}   G      &∈B^A \\
&,     a   \sa   \so}\}_a&∈A \\
=&\{  Fa \a{n_a} Ga \}_a&∈B \\
}
```

自然変換の自然性公理(スライディング則)
```math
\eq{&Fa \a{Ff   &⨾& n_b} Gb &∈B \\
=&   Fa \a{Ff}  Fb \a{n_b} Gb &∈B \\ \hdashline
=&\t{\so   \sa   F \a{n}    G &∈B^A \\
&,    a \a{f}    b   \sa   \so }&∈A \\
=&\t{ F \a{n}    G   \sa   \so &∈B^A \\
&,   \so   \sa   a \a{f}   b} &∈A \\ \hdashline
=&   Fa \a{n_a} Ga \a{Gf}  Gb &∈B \\
=&   Fa \a{n_a  &⨾& Gf}  Gb &∈B \\
}
```

恒等自然変換の自然性公理
```math
\eq{&Fa \a{Ff  &⨾& 1_{Fb}} Fb  &∈B \\
=&   Fa \a{Ff}   Fb  \i{Fb}  Fb  &∈B \\ \hdashline
=&\t{\so   \sa    F  \a{1_F} F   &∈B^A \\
&,    a \a{f}     b    \sa   \so }&∈A \\
=&\t{ F \i{F}     F    \sa   \so &∈B^A \\
&,   \so   \sa    a  \a{f}   b  }&∈A \\ \hdashline
=&   Fa \i{Fa}   Fa  \a{Ff}  Fb  &∈B \\
=&   Fa \a{1_{Fa}&⨾&  Ff}  Fb  &∈B \\
}
```

自然変換(射への作用)
```math
\eq{&Fa \a{n∙f}    &&  Gb &∈B \\
:=&\t{F \a{n}      &&  G  &∈B^A \\
&  ,  a \a{f}      &&  b} &∈A \\ \hdashline
=&\t{\so  \sa  F \a{n} G  &∈B^A \\
&,    a \a{f}  b   \sa \so }&∈A \\
=&\t{ F \a{n}  G   \sa \so &∈B^A \\
&,   \so  \sa  a \a{f} b }&∈A \\
}
```

対角関手
```math
\eq{&Δ_ai \a{Δ_fi  &⨾& Δ_bu}   Δ_bj &∈C \\
=&     a  \a{f}       b   \sa     \so &∈C \\
=&   Δ_ai \a{Δ_fi} Δ_bi \a{Δ_bu} Δ_bj &∈C \\
=&\t{Δ_a  \a{Δ_f}  Δ_b  \sa      \so  &∈C^I \\
&,   \so  \sa      i     \a{u}    j   }&∈I \\
=&\t{Δ    \sa      \so   \sa      \so  &∈C^{C×I} \\
&,   a    \a{f}    b     \sa      \so  &∈C \\
&,   \so  \sa      i     \a{u}    j   }&∈I \\ \hdashline
=&\t{Δ    \sa      \so   \sa      \so  &∈C^{C×I} \\
&,   \so  \sa      a     \a{f}    b    &∈C \\
&,   i    \a{u}    j     \sa      \so }&∈I \\
=&\t{\so  \sa      Δ_a  \a{Δ_f}  Δ_b  &∈C^I \\
&,   i    \a{u}    j     \sa      \so }&∈I \\
=&   Δ_ai \a{Δ_au} Δ_aj \a{Δ_fj} Δ_bj &∈C \\
=&   \so  \sa       a \a{f}       b &∈C \\
=&   Δ_ai \a{Δ_au  &⨾& Δ_fj}   Δ_bj &∈C \\
}
```

対象を終対象(1点集合)からの関手と同一視可能。
```math
\eq{
&\t{Δ_a \sa \so &∈C^1 \\
&,  *   \i{*} *}&∈1 \\
=&  a   \i{a} a &∈C \\
}
```

射を自然変換と同一視可能。(スライディング則が自明に成り立つ)
```math
\eq{&Δ_a* \a{Δ_f1_*  &⨾& Δ_b1_*}   Δ_b* &∈C \\
=&     a  \a{f}       b   \sa     \so &∈C \\
=&   Δ_a* \a{Δ_f1_*} Δ_b* \a{Δ_b1_*} Δ_b* &∈C \\
=&\t{Δ_a  \a{Δ_f}  Δ_b  \sa      \so  &∈C^1 \\
&,   \so  \sa      *     \i{*}    *   }&∈1 \\
=&\t{Δ    \sa      \so   \sa      \so  &∈C^{C×1} \\
&,   a    \a{f}    b     \sa      \so  &∈C \\
&,   \so  \sa      *     \i{*}    *   }&∈1 \\ \hdashline
=&\t{Δ    \sa      \so   \sa      \so  &∈C^{C×1} \\
&,   \so  \sa      a     \a{f}    b    &∈C \\
&,   *    \i{*}    *     \sa      \so }&∈1 \\
=&\t{\so  \sa      Δ_a  \a{Δ_f}  Δ_b  &∈C^1 \\
&,   *    \i{*}    *     \sa      \so }&∈1 \\
=&   Δ_a* \a{Δ_a1_*} Δ_a* \a{Δ_f1_*} Δ_b* &∈C \\
=&   \so  \sa       a \a{f}       b &∈C \\
=&   Δ_a* \a{Δ_a1_*  &⨾& Δ_f1_*}   Δ_b* &∈C \\
}
```

自然変換の垂直合成【2圏間合成】
(圏論一般の用語に倣っている。文字列の進む方向を上下として考えれば良い)
```math
\eq{&  F  \a{n    &⨾&  m}    H      &∈B^A \\
:=&    F  \a{n}   G  \a{m}   H      &∈B^A \\
=&\{\t{F  \a{n}   G  \a{m}   H      &∈B^A \\
&,     a    \sa   \so  \sa   \so }\}_a&∈A \\
=&\{   Fa \a{n_a} Ga \a{m_a} Ha \}_a&∈B \\
}
```

自然変換の垂直合成の自然性公理(スライディング則)
```math
\eq{&Fa \a{Ff&⨾& (n   &⨾&   m)_b} Hb &∈B \\
&    Fa \a{Ff&⨾&  n_b &⨾&    m_b} Hb &∈B \\
=&   Fa \a{Ff}  Fb \a{n_b} Gb   \a{m_b} Hb &∈B \\ \hdashline
=&\t{\so  \sa   F  \a{n}   G      \a{m} H  &∈B^A \\
&,    a \a{f}   b    \sa   \so    \sa \so }&∈A \\
=&\t{ F \a{n}   G    \sa   G      \a{m} H  &∈B^A \\
&,   \so  \sa   a  \a{f}   b      \sa \so }&∈A \\
=&\t{ F \a{n}   G  \a{m}   H       \sa \so &∈B^A \\
&,   \so  \sa   \so  \sa   a      \a{f} b }&∈A \\ \hdashline
=&   Fa \a{n_a} Ga \a{m_a} Ha    \a{Hf} Hb &∈B \\
=&   Fa \a{n_a&⨾&  m_a &⨾&    Hf} Gb &∈B \\
=&   Fa \a{(n &⨾& m)_a &⨾&    Hf} Gb &∈B \\
}
```

自然変換の水平合成【3圏間合成】とそのスライディング則
(圏論一般の用語に倣っている。文字列の進む方向を上下として考えれば良い)
```math
\eq{&\{F'Fa\a{n'_a∙n_a}     &&         G'Ga \}_a&∈C^A \\
=&   F'F  \a{n'   ∙n}       &&         G'G      &∈C^A \\
=&\t{  F' \a{n'}            &&         G'       &∈C^B \\
&,     F  \a{n}             &&         G       }&∈B^A \\
=&\{\t{F' \a{n'}            &&         G'       &∈C^B \\
&,     F  \a{n}             &&         G        &∈B^A \\
&,     a  \sa               &&         \so }\}_a&∈A \\ \hdashline
:=&\{F'Fa \a{n'_a∙F_a} G'Fa \a{G'a∙n_a} G'Ga \}_a&∈C^A \\
=&   F'F  \a{n'  ∙F}   G'F  \a{G' ∙n}   G'G      &∈C^A \\
=&\t{  F' \a{n'}         G'   \sa      \so      &∈C^B \\
&,    \so \sa            F    \a{n}    G       }&∈B^A \\
=&\{\t{F' \a{n'}         G'   \sa      \so      &∈C^B \\
&,    \so \sa            F    \a{n}    G        &∈B^A \\
&,     a  \sa            \so  \sa      \so }\}_a&∈A \\ \hdashline
=&\{ F'F  \a{F'a∙n_a}  F'Ga \a{n'_a∙Ga} G'Ga \}_a&∈C^A \\
=&   F'F  \a{F' ∙n}    F'G  \a{n'  ∙G}  G'G      &∈C^A \\
=&\t{ \so \sa            F'   \a{n'}   G'       &∈C^B \\
&,     F  \a{n}          G    \sa      \so     }&∈B^A \\
=&\{\t{\so \sa           F'   \a{n'}   G'       &∈C^B \\
&,     F  \a{n}          G    \sa      \so      &∈B^A \\
&,     a  \sa            \so  \sa      \so }\}_a&∈A \\
}
```

恒等自然変換 $1_F = F$ とおくことが可能。
```math
\eq{& F'F \a{1_{F'}∙n} F'G   &∈B^A \\
=:&   F'F \a{F'∙n}     F'G   &∈B^A \\
=&\t{ F'  \sa          \so   &∈B^B \\
&,    F   \a{n}        G    }&∈B^A \\
=&\{\t{F' \sa          \so   &∈B^B \\
&,    F   \a{n}        G     &∈B^A \\
&,    a   \sa         \so }\}_a&∈A \\
}
```

垂直合成と水平合成のスライディング則
```math
\eq{&F'F \a{(n' &⨾& m')&∙&(n&⨾&  m)}             H'H &∈C^A \\ \hdashline
=&\t{F'  \a{n'  &⨾& G' &   &    &⨾&       m'}    H'  &∈C^B \\
&,   F   \a{n   &⨾& G  &   &    &⨾&       m }    H  }&∈B^A \\
=&\t{F' (\a{n'} G'  \a{m'})H'  \sa  \so \sa     \so &∈C^B \\
&,   \so \sa    \so \sa F(\a{n}  G       \a{m}) H  }&∈B^A \\
=&\t{F'  \a{n'} G'  \a{m'} H'  \sa   \so \sa    \so &∈C^B \\
&,   \so \sa    \so \sa    F   \a{n}  G  \a{m}  H  }&∈B^A \\
=&\t{F'  \a{n'} G'  \sa    G'  \a{m'} H' \sa    \so &∈C^B \\
&,   \so \sa    F   \a{n}  G   \sa    G  \a{m}  H  }&∈B^A \\
=&\t{F'  \a{n'} G'  \sa    \so \sa    G' \a{m'} H'  &∈C^B \\
&,   F   \a{n}  G   \sa    \so \sa    G  \a{m}  H  }&∈B^A \\ \hdashline
=&   F'F \a{(n'     &∙&     n)  &⨾& (m'  &∙& m)} H'H &∈C^A \\
}
```

自然同型
```math
\eq{&&  &          Ga \a{Gf} Gb  &       &    &∈B \\
=&\t{&  &          G  \sa    \so &       &    &∈B^A \\
&,   &  &          a  \a{f}  b   &       &   }&∈A \\ \hdashline
=&\t{G  \a{n\iv}   F  \sa    F   \a{n}   G    &∈B^A \\
&,  \so \sa        a  \a{f}  b   \sa     \so }&∈A \\
=&   Ga \a{n\iv_a} Fa \a{Ff} Fb  \a{n_b} Gb   &∈B \\
}
```

```math
\eq{
&  Ga \a{Gf} Gb &∈B \\ \hdashline
≅&Fa \a{Ff} Fb &∈B &\text{※}\\
}
```
※二方向規則が表現されている。

$n$ が自然変換⟺ $∀x, n_x$ は同型射
$n$ が自然変換、 $∀x, m_x = (n_x)\iv$ は同型射⟹$m$ は自然変換
```math
\eq{
=&\t{G  \a{m}   F  \sa         &&          &&      \so  &∈B \\
&,  \so \sa     x  \a{f}       &&          &&      y   }&∈B \\ \hdashline
=&   Gx \a{m_x} Fx \a{Ff}      &&          &&      Fy   &∈B \\
=&(  Gx \a{m_x} Fx \a{Ff}  Fy) \a{n_y  &⨾& m_y}    Fy   &∈B \\
=&(  Gx \a{m_x} Fx \a{Ff}  Fy) \a{n_y} Gy  \a{m_y} Fy   &∈B \\ \hdashline
=&\t{G  \a{m}   F  \sa     F   \a{n}   G   \a{m}   F    &∈B^A \\
&,  \so \sa     x  \a{f}   y   \sa     \so \sa     \so }&∈A \\
=&\t{G  \a{m}   F  \a{n}   G   \sa     G   \a{m}   F    &∈B^A \\
&,  \so \sa     \so \sa    x   \a{f}   y   \sa     \so }&∈A \\ \hdashline
=&   Gx \a{m_x} Fx \a{n_x}(Gx  \a{Gf}  Gy  \a{m_y} Fy)  &∈B \\
=&   Gx \a{m_x  &⨾& n_x}(Gx    \a{Gf}  Gy  \a{m_y} Fy)  &∈B \\
=&   Gx &&            &&       \a{Gf}  Gy  \a{m_y} Fy   &∈B \\ \hdashline
=&\t{\so &&           &&       \sa     G   \a{m}   F    &∈B^A \\
&,   x  &&            &&       \a{f}   y   \sa     \so }&∈B \\
}
```

双関手の間の自然変換の自然性公理(スライディング則)
```math
\eq{&F\p{a,b} \a{F\p{f,g}   &⨾&         n_\p{a',b'}}   G\p{a',b'} &∈C \\
=&   F\p{a,b} \a{F\p{f,g}}  F\p{a',b'} \a{n_\p{a',b'}} G\p{a',b'} &∈C \\ \hdashline
=&\t{\so      \sa           F          \a{n}           G          &∈C^{A×B} \\
&,\p{a        \a{f}         a'         \sa             \so        &∈A \\
&,   b        \a{g}         b'         \sa             \so      }}&∈B \\
=&\t{F        \a{n}         G          \sa             \so        &∈C^{A×B} \\
&,\p{\so      \sa           a          \a{f}           a'         &∈A \\
&,   \so      \sa           b          \a{g}           b'       }}&∈B \\ \hdashline
=&   F\p{a,b} \a{n_\p{a,b}} G\p{a,b}   \a{G\p{f,g}}    G\p{a',b'} &∈C \\
=&   F\p{a,b} \a{n_\p{a,b}  &⨾&        G\p{f,g}}       G\p{a',b'} &∈C \\
}
```

双関手間の自然変換の一意性：各圏の対象を固定した自然変換で一つに決まる。
```math
\eq{
& F\p{a,b}\a{F\p{f,g}}&&F\p{a',b'}\a{n_{a',b'}}G\p{a',b'} &∈C \\
=&\t{ \so \sa   &&        F   \a{n} G    &∈C^{A×B} \\
&,    a   \a{f} &&        a'  \sa   \so  &∈A \\
&,    b   \a{g} &&        b'  \sa   \so }&∈B \\
=&\t{ \so \sa   \so \sa   F   \a{n} G    &∈C^{A×B} \\
&,    \so \sa   a   \a{f} a'  \sa   \so  &∈A \\
&,    b   \a{g} b'  \sa   \so \sa   \so }&∈B \\
=&\t{ \so \sa   F   \a{n} G   \sa   \so  &∈C^{A×B} \\
&,    \so \sa   \so \sa   a   \a{f} a'   &∈A \\
&,    b   \a{g} b'  \sa   \so \sa   \so }&∈B \\
=&\t{ F   \a{n} G   \sa   \so \sa   \so  &∈C^{A×B} \\
&,    \so \sa   \so \sa   a   \a{f} a'   &∈A \\
&,    \so \sa   b   \a{g} b'  \sa   \so }&∈B \\
=&\t{ F   \a{n} &&        G   \sa   \so  &∈C^{A×B} \\
&,    \so \sa   &&        a   \a{f} a'   &∈A \\
&,    \so \sa   &&        b   \a{g} b'  }&∈B \\
=& F\p{a,b}\a{n_{a,b}}&&G\p{a,b}\a{G\p{f,g}}G\p{a',b'} &∈C \\
}
```

homセット
```math
\eq{
&   a\a{a⨾b} b    &∈A \\
=&  a \h    b     &∈A \\
=&\{a \a{h} b \}_h&∈A \\
=&  a \a{A(a,b)} b &∈A & \text{※}\\
}
```
※圏論一般の表記法

homセットとhom関手と自然変換の自然性
```math
\eq{
&   (a' \a{f}  a \h    b) \a{g} b'     &∈A \\
=&\{(a' \a{f}  a \a{h} b) \a{g} b' \}_h&∈A \\
=&\{ a' \a{f} (a \a{h} b  \a{g} b')\}_h&∈A \\
=&   a' \a{f} (a \h    b  \a{g} b')    &∈A \\
}
```
⟺
```math
\eq{
&  a⨾b \a{f⨾b} a'⨾b \a{a'⨾g} a'⨾b'&∈\sets \\
=& a⨾b \a{a⨾g} a⨾b' \a{f⨾b'} a'⨾b'&∈\sets \\
}
```
∴
```math
\eq{
&\t{ a⨾- \a{f⨾-} a'⨾- \sa      \so &∈\sets \\
&,   \so \sa    b    \a{g}    b' }&∈A \\ \hdashline
=&   a⨾b \a{f⨾b} a'⨾b \a{a'⨾g} a'⨾b'&∈\sets \\
=&   a⨾b \a{a⨾g} a⨾b' \a{f⨾b'} a'⨾b'&∈\sets \\ \hdashline
=&\t{\so \sa    a⨾-  \a{f⨾-}  a'⨾- &∈\sets \\
&,   b   \a{g}  b'   \sa     \so }&∈A \\
}
```
また
```math
\eq{
&\t{ \so \sa     -⨾b \a{-⨾g}  -⨾b'  &∈\sets \\
&,   a   \a{f⨾}  a'  \sa      \so }&∈A\op \\ \hdashline
=&   a⨾b \a{f⨾b} a'⨾b \a{a'⨾g} a'⨾b' &∈\sets \\
=&   a⨾b \a{a⨾g} a⨾b' \a{f⨾b'} a'⨾b' &∈\sets \\ \hdashline
=&\t{-⨾b \a{-⨾g} -⨾b' \sa      \so  &∈\sets \\
&,   \so \sa     a   \a{f⨾}   a'  }&∈A\op \\
}
```

hom系の式変形
```math
\eq{
&  \so \sa  a   \a{f}  b    &∈C \\
=&  a \i{a} a   \a{f}  b    &∈C \\
=&\t{ \spn  a⨾- \sa    \so  &∈\sets \\
&,  * \i{}  a   \a{f}  b   }&∈C \\
=&\t{ \spn  a⨾- \sa    \so  &∈\sets \\
&,  * \a{f} b   \sa    \so }&∈C \\
=&\t{ \spn  b⨾- \a{f⨾-} a⨾-  &∈\sets \\
&,  * \i{}  b   \sa    \so }&∈C \\
}
```

$n : (a⨾-) \⇨ K : C\op\➡\sets)$ 集合値関手への自然変換の式変形
```math
\eq{
&       &&   a⨾- \a{n} K      &∈\sets \\
=&\{\t{ &&   a⨾- \a{n} K      &∈\sets \\
&,    d \sa  \so \sa   \so }\}_d&∈C \\
=&\{\t{ \spn a⨾- \a{n} K      &∈\sets \\
&,    * \i{} a     \h  d }\}_d&∈C \\
=&  \t{ \spn a⨾- \a{n} K      &∈\sets \\
&,    * \i{} a     \h  -     }&∈C \\
}
```

米田写像 $y_{K,a}$
```math
\newcommand\pin{{n∈(a⨾-)⨾K}}
\eq{
&       &&         &&      &y_{K,a}(n)∈&  Ka&    (\pin)& \\
⟺&\{ * &&        &&       \a{y_{K,a}(n)}  Ka & \}_\pin&∈\sets \\
=&\{\t{ \spn  a⨾-  &&       \a{y_{K,a}(n)} K  &        &∈\sets^C \\
&,    * \i{}  a    \sa  \so \sa            \so &}\}_\pin&∈C \\
\xlongequal{f:=1}
&\{\t{  \spn  a⨾-  &&       \a{y_{K,a}(n)} K  &        &∈\sets^C \\
&,    * \i{}  a    \a{f} d  \sa            \so &}\}_{\pin,f∈a⨾d}&∈C \\
=&\{\t{ \spn  a⨾-  &&       \a{y_{K,a}(n)} K  &        &∈\sets^C \\
&,    * \i{}  a    \h    d  \sa            \so &}\}_{\pin,d}&∈C \\
=&\{\t{ \spn  a⨾-  \a{n} K  \a{y_{K,a}}    K  &        &∈\sets^C \\
&,    * \i{}  a    \h    d  \sa            \so &}\}_{\pin,d}&∈C \\
=&\{\t{ &&    a⨾-  \a{n} K  \a{y_{K,a}}    K  &        &∈\sets^C \\
&,      &&    d    \sa   \so \sa            \so &}\}_{\pin,d}&∈C \\
=&\{    &&    a⨾-  \a{n} K  \a{y_{K,a}}    Ka & \}_\pin&∈\sets \\
=&      &&    a⨾-  \h    K  \a{y_{K,a}}    Ka &        &∈\sets \\
=&      &&((a⨾-)   &⨾&   K) \a{y_{K,a}}    Ka &        &∈\sets \\ \hdashline
:=&\t{  \spn  a⨾-  &&       \h             K  &        &∈\sets^C \\
&,    * \a{!} a    &&       \sa            \so &}       &∈C \\
=&\{\t{ \spn  a⨾-  &&       \a{n}          K  &        &∈\sets^C \\
&,    * \a{!} a    &&       \sa            \so &}\}_\pin&∈C \\
=&\{\t{ \spn  a⨾-  &&       \a{n}          K  &        &∈\sets^C \\
&,    * \a{!} a    &&       \i{a}          a  &}\}_\pin&∈C \\
=&\{  * &&         &&       \a{n_a∙1_a}    Ka & \}_\pin&∈\sets \\
⟺&     &&         &&       &n_a∙1_a∈&    Ka&   (\pin)& \\
}
```
逆向きの米田写像 $Y_{K,a}$
```math
\renewcommand\pin{{x∈Ka}}
\eq{
&        &&       &Y_{K,a}(x)∈& (a⨾-)⨾K& (\pin)& \\
⟺&\{  * &&       \a{Y_{K,a}(x)} (a⨾-)⨾K & \}_\pin&∈\sets \\
=&\{   * \a{x} Ka \a{Y_{K,a}}    (a⨾-)⨾K & \}_\pin&∈\sets \\
=&       &&    Ka \a{Y_{K,a}}    (a⨾-)⨾K &        &∈\sets \\ \hdashline
:=&\t{   \spn  K  \sa            \so     &        &∈\sets^C \\
&,     * \a{?} a  \h             -       &       }&∈C \\
=&\{\t{  \spn  K  \sa            \so     &        &∈\sets^C \\
&,     * \a{x} a  \h             -       &}\}_\pin&∈C \\
=&\{\t{  \spn  K  \sa            \so     &        &∈\sets^C \\
&,     * \a{x} a  \a{f}          d   &}\}_{\pin, f∈a⨾d}&∈C \\
=&\{\t{* \a{x} Ka \a{Kf}         Kd  &}\}_{\pin, f∈a⨾d}&∈C \\
=&\{\t{* &&       \a{Kf(x)}      Kd  &}\}_{\pin, f∈a⨾d}&∈C \\
⟺&      &&       &Kf(x)∈&      Kd  &    (\pin, f∈a⨾d)& \\
}
```

```math
\eq{
&              &&    a⨾- \a{n} K   &&      &∈\sets \\
\xmapsto{y}&\t{\spn  a⨾- \a{n} K   &&      &∈\sets^C \\
&,           * \a{!} a   \sa   \so &&     }&∈C \\
\xmapsto{Y}&\t{\spn  a⨾- \a{n} K   \sa \so &∈\sets^C \\
&,           * \a{!} a   \sa   \so \h  -  }&∈C \\
=&             &&    a⨾- \a{n} K   &&      &∈\sets \\
}
```

```math
\eq{
&\t{           \spn  K  &&     &∈\sets^C \\
&,           * \a{x} a  &&    }&∈C \\
\xmapsto{Y}&\t{\spn  K  \sa \so &∈\sets^C \\
&,           * \a{x} a  \h  - }&∈C \\
\xmapsto{y}&\t{\spn  K  &&     &∈\sets^C \\
&,           * \a{x} a  &&    }&∈C \\
}
```

hom関手との合成
```math
\eq{
&    && a'⨾Fa \a{a'⨾Ff} a'⨾Fb &∈\sets \\
=&\t{&& a'⨾F- \sa       \so   &∈\sets \\
&,   && a     \a{f}     b    }&∈A \\
=&\t{&& a'⨾-  \sa       \so   &∈\sets \\
&,   && F     \sa       \so   &∈B^A \\
&,   && a     \a{f}     b    }&∈A \\
=&\t{\spn F   \sa       \so   &∈B^A \\
&,a' \h a     \a{f}     b    }&∈A \\
}
```
∴
```math
\eq{
&\t{ && a'⨾F- &∈\sets \\
&,   && ?    }&∈A \\
=&\t{&& a'⨾-  &∈\sets \\
&,   && F     &∈B^A \\
&,   && ?    }&∈A \\
=&\t{\spn F   &∈B^A \\
&,a' \h ?    }&∈A \\
}
```
また
```math
\eq{
&    Fa⨾b' \a{Ff⨾b'} Fb⨾b' &&    &∈\sets \\
=&\t{F-⨾b' \sa       \so  &&    &∈\sets \\
&,   a     \a{f}     b    &&   }&∈A \\
=&\t{-⨾b'  \sa       \so  &&    &∈\sets \\
&,   F     \sa       \so  &&    &∈B^A \\
&,   a     \a{f}     b    &&   }&∈A \\
=&\t{F     \sa       \so  \spn  &∈B^A \\
&,   a     \a{f}     b    \h b'}&∈A \\
}
```
∴
```math
\eq{
&\t{F-⨾b' &&   &∈\sets \\
&,     ?  &&  }&∈A \\
=&\t{-⨾b' &&   &∈\sets \\
&,     F &&    &∈B^A \\
&,     ? &&   }&∈A \\
=&\t{  F \spn  &∈B^A \\
&,     ? \h b'}&∈A \\
}
```

コンマ圏 $(F⇉G)$
```math
\eq{
&\p{a,h,b}\ap{f,& &g}\p{a',h',b'}&∈(F⇉G)\\ \hdashline
=&\t{F   \a{h}  G   \sa    \so &∈C^{\text{below}}\\
&,   a   \spn       &&         &∈A\\
&,       \spn   b   \a{g}  b' }&∈B\\ \hdashline
=&   Fa  \a{h}  Gb  \a{Gg} Gb' &∈C\\
=&   Fa  \a{Ff} Fa' \a{h'} Gb' &∈C\\ \hdashline
=&\t{\so \sa    F   \a{h'} G   &∈C^{\text{below}}\\
&,   a   \a{f}  a'  \spn       &∈A\\
&,       &&         \spn   b' }&∈B\\
}
```

コンマ圏 $(F⇉b):=(F⇉!)$
```math
\eq{
&\p{a,h} \a{f}      && \p{a',h'}&∈(F⇉b)\\ \hdashline
=&\t{F   \a{h}  !   \sa    \so  &∈C^A\\
&,   a   \spn   b   \sa    \so }&∈A\\ \hdashline
=&   Fa  \a{h}  b   \sa    \so  &∈C\\
=&   Fa  \a{Ff} Fa' \a{h'} b    &∈C\\ \hdashline
=&\t{\so \sa    F   \a{h'} !    &∈C^A\\
&,   a   \a{f}  a'  \spn   b   }&∈A\\
}
```

スライス圏 $A/b:=(1_A⇉b)=(1_A⇉!)$
```math
\eq{
&\p{a,h}\a{f}&&\p{a',h'}&∈A/b\\ \hdashline
=& a  \a{h} b  \sa    \so &∈A\\
=& a  \a{f} a' \a{h'} b   &∈A\\
}
```

$F$ から $b$ への普遍射 $:=(F⇉b)$ の終対象
```math
\eq{
& 1∀   &2∃!&     && 1= \\
&\p{a,h}\a{f}      &&\p{a',h'} &∈(F⇉b)\\ \hdashline
=&\t{F  \a{h}  !   \sa    \so  &∈C^A\\
&,   a  \spn   b   \sa    \so }&∈A\\ \hdashline
=&   Fa \a{h}  b   \sa    \so  &∈C\\
=&   Fa \a{Ff} Fa' \a{h'} b    &∈C\\ \hdashline
=&\t{\so \sa    F  \a{h'} !    &∈C^A\\
&,   a   \a{!f} a' \spn   b   }&∈A\\
}
```

コンマ圏 $(a⇉G):=(!⇉G)$
```math
\eq{
&\p{h,b}&&       \a{g}\p{h',b'}&∈(a⇉G)\\ \hdashline
=&\t{!  \a{h} G  \sa    \so &∈C^B\\
&,   a  \spn  b  \a{g}  b' }&∈B\\ \hdashline
=&   a  \a{h} Gb \a{Gg} Gb' &∈C\\
=&   \so \sa   a \a{h'} Gb' &∈C\\ \hdashline
=&\t{\so \sa   ! \a{h'} G   &∈C^B\\
&,   \so \sa   a \spn   b' }&∈B\\
}
```

余スライス圏 $a/B:=(B⇉1_B)=(!⇉1_B)$
```math
\eq{
&\p{h,b}&&\a{g}\p{h',b'}&∈a/B\\ \hdashline
=& a   \a{h} b \a{g}  b' &∈B\\
=& \so \sa   a \a{h'} b' &∈B\\
}
```

$a$ から $G$ への普遍射 $:=(a⇉G)$ の始対象
```math
\eq{
& 0=     &&   &2∃!&    1∀ \\
&\p{h,b} &&       \a{g}  \p{h',b'}&∈(a⇉G)\\ \hdashline
=&\t{!   \a{h} G  \sa    \so &∈C^B\\
&,   a   \spn  b  \a{g}  b' }&∈B\\ \hdashline
=&   a   \a{h} Gb \a{Gg} Gb' &∈C\\
=&   \so \sa   a  \a{h'} Gb' &∈C\\ \hdashline
=&\t{\so \sa   !  \a{h'} G   &∈C^B\\
&,   \so \sa   a  \spn   b' }&∈B\\
}
```

随伴
前提: $F:A⇄B:G$ は関手
$w:F⊣G:A⇄B$
$⟺ w:B(F-,?)≅A(-,G?)$
$⟺ ∀a,b, w_{a,b}:B(Fa,b)≅A(a,Gb)$

随伴の自然性
```math
\eq{
& Fa⨾b \a{Ff⨾g}    Fa'⨾b' \a{w_{a',b'}} a'⨾Gb' &∈\sets \\
=&Fa⨾b \a{w_{a,b}}  a⨾Gb  \a{f⨾Gg}      a'⨾Gb' &∈\sets \\
}
```
∴ $∀h$
```math
\eq{
&  Fa'\a{Ff} Fa    \a{h}     b       \a{g}           b'  &∈B \\
=&  &Ff⨾&     h     &⨾g&             &&                  &∈B_1 \\
≅& &Ff⨾&     h     &⨾g&     ⨾       &w_{a',b'}&         &∈A_1 \\
=&  h &⨾& (       &Ff⨾g&     ⨾       &w_{a',b'}&       ) &∈A_1 \\
=&  h &⨾& (Fa⨾b \a{Ff⨾g}    Fa'⨾b' \a{w_{a',b'}} a'⨾Gb') &∈A_1 \\
=&  h &⨾& (Fa⨾b \a{w_{a,b}}  a⨾Gb  \a{f⨾Gg}      a'⨾Gb') &∈A_1 \\
=&  h &⨾& (       &w_{a,b}&  ⨾       &f⨾Gg&            ) &∈A_1 \\
=& (h &⨾&         &w_{a,b})& ⨾      &(f⨾Gg&            ) &∈A_1 \\
=&    &f⨾&   (h  &⨾w_{a,b})& ⨾         &Gg&              &∈A_1 \\
=& a' \a{f}   a   \a{h⨾w}      Gb    \a{Gg}         Gb'  &∈A \\
}
```
∴
```math
\eq{
&  Fa' \a{Ff} Fa \a{h}    b \a{g}   b' &∈B \\
≅& a' \a{f}   a \a{h⨾w} Gb \a{Gg} Gb' &∈A \\
}
```
※二方向規則が表現されている。
⟺
```math
\eq{
&\t{\so \sa   F \a{h}       &&       &∈B^A \\
&,   a' \a{f} a \spn        &&       &∈A \\
&,      &&      \spn      b \a{g} b'}&∈B \\
≅&\t{  &&      \a{h⨾w}   G \sa   \so &∈A^B \\
&,   a' \a{f} a \spn        &&        &∈A \\
&,      &&      \spn     b \a{g}   b'}&∈B \\
}
\newcommand\Dt{D^\sim}
```
※二方向規則をストリング図で表したものが表現されている。

極限はコンマ圏 $(Δ⇉\Dt) (Δ:C\➡C^I, D:I\➡C, \Dt:{*}\➡C^I = D)$ の終対象
```math
\eq{
& 1∀    &2∃!&      &&    1= \\
&\p{y,g} \a{h}       &&    \p{x,f}&∈(Δ⇉\Dt) \\ \hdashline
=&\t{Δ   \a{g}  \Dt  \sa   \so    &∈(C^I)^{\text{below}} \\
&,   y   \spn        &&           &∈C \\
&,       \spn   *    \sa   \so   }&∈\{*\} \\ \hdashline
=&  Δ_y \a{g}   \Dt* \sa   \so   &∈C \\
=&  Δ_y \a{Δ_h} Δ_x \a{f} \Dt*  &∈C \\ \hdashline
=&\t{\so \sa     Δ    \a{f} \Dt   &∈(C^I)^{\text{below}} \\
&,   y   \a{h}   x    \spn        &∈C \\
&,       &&           \spn  *    }&∈\{*\} \\
}
```
自然変換 $g:Δ_y\⇨D = \cone(y,D) \ie y$ を頂点とする $D$ の錐のスライディング則
```math
\eq{
&    y    \a{g_i}  D_i   \a{D_u} D_j   &∈C \\ \hdashline
=&\t{Δ_y  \a{g}    D     \sa    \so    &∈C^I \\
&,   \so  \sa      i     \a{u}   j    }&∈I \\
=&   Δ_yi \a{g_i}  D_i   \a{D_u} D_j   &∈C \\
=&   Δ_yi \a{Δ_yu} Δ_yj \a{g_j}  D_j  &∈C \\
=&\t{\so   \sa     Δ_y   \a{g}    D    &∈C^I \\
&,   i     \a{u}   j     \sa      \so }&∈I \\ \hdashline
=&   \so   \sa     y     \a{g_j}  D_j  &∈C \\
=&   y     \a{g_j}       &&       D_j  &∈C \\
}
```
上記２つを組み合わせて整理した、極限
```math
\eq{
&       &&    x \a{f_i} D_i \a{D_u} D_j \\
=&      &&    x \a{f_j}     &&      D_j \\ \hdashline
\and∀y,g&y &&  \a{g_i} D_i \a{D_u} D_j \\
=&       y &&   \a{g_j}     &&      D_j \\
∃!h\st& y &&   \a{g_i} D_i && \\
=&    y \a{h} x \a{f_i} D_i && \\
\and& y &&      \a{g_j}     && D_j \\
=&    y \a{h} x \a{f_j}     && D_j \\
}
```

余極限はコンマ圏 $(\Dt⇉Δ) (Δ:C\➡C^I, D:I\➡C, \Dt:{*}\➡C^I = D)$ の始対象
```math
\eq{
&        0= &&         &2∃!&   1∀      \\
&   \p{x,f} &&         \a{h}    \p{y,g} &∈(\Dt⇉Δ) \\ \hdashline
=&\t{\so    \sa   \Dt  \a{g}    Δ       &∈(C^I)^{\text{below}} \\
&,          &&         \spn     y       &∈C \\
&,   \so    \sa   *    \spn            }&∈\{*\} \\ \hdashline
=&   \so    \sa   \Dt* \a{g}    Δ_y    &∈C \\
=&   \Dt*   \a{f} Δ_x  \a{Δ_h} Δ_y    &∈C \\ \hdashline
=&\t{\Dt    \a{f} Δ    \sa     \so    &∈(C^I)^{\text{below}} \\
&,          \spn  x    \a{h}    y     &∈C \\
&,        * \spn       &&            }&∈\{*\} \\
}
```

自然変換 $g:D\⇨Δ_y = \cocone(D,y) \ie y$ を頂点とする $D$ の余錐のスライディング則
```math
\eq{
&    D_i \a{D_u} D_j  \a{g_j} y     &∈C \\ \hdashline
=&\t{\so \sa     D    \a{g}   Δ_y   &∈C^I \\
&,     i \a{u}   j    &&           }&∈I \\
=&   D_i \a{D_u} D_j  \a{g_j}  Δ_yj &∈C \\
=&   D_i \a{g_i} Δ_yi \a{Δ_yu} Δ_yj &∈C \\
=&\t{  D \a{g}   Δ_y  \sa     \so   &∈C^I \\
&,   \so \sa     i    \a{u}    j   }&∈I \\ \hdashline
=&   D_i \a{g_i} y    \sa      \so  &∈C \\
=&   D_i &&           \a{g_i}  y    &∈C \\
}
```
上記２つを組み合わせて整理した、余極限
```math
\eq{
&         D_i \a{D_u} D_j \a{f_j} x && \\
=&        D_i &&          \a{f_i} x && \\ \hdashline
\and∀y,g&D_i \a{D_u} D_j \a{g_j}   &&    y \\
=&        D_i &&          \a{g_i}   &&    y \\
∃!h\st&  D_i &&          \a{g_i}   &&    y \\
=&        D_i &&          \a{f_i} x \a{h} y \\
\and&         &&      D_j \a{g_j}   &&    y \\
=&            &&      D_j \a{f_j} x \a{h} y \\
}
```

## 技術情報
$\TeX$ で小さなコマンドを定義すると、ソースの可読性が高まったり、記号を切り替えたり、と便利です。
|名前|英語|表示例|$\TeX$定義文|その他|
|--|--|--|--|--|
|式|equation|省略|`\newcommand\eq[1]{\begin{array}{}#1\end{array}}`||
|射|arrow|$[f]$ or $\ket{f}$|`\newcommand\a[1]{&[#1]&}`|`&`を含める|
|同様対象|same object|⋯|`\newcommand\so{⋯}`||
|同様射|same arrow|⋯|`\newcommand\sa{&⋯&}`|`&`を含める|
|並進を跨る射|span|$\\\|$|`\newcommand\spn{&\\|\\|&}`|`&`を含める|
|ホムセット|hom|$[\ ]$|`\newcommand\h{&[\ ]&}`|`&`を含める|
|直積|product|$\p{a,b}$|`\newcommand\p[1]{\langle #1 \rangle}`||
|直積の射|a & p|$[\p{a,b}]$|`\newcommand\ap[1]{&[\langle #1 \rangle]&}`|`&`を含める|
|恒等射|identity|$1_a$|`\renewcommand\i[1]{&[1_{#1}]&}`|`&`を含める、上書き|
|並進式|translational|$\t{F,a [f] b} $|`\renewcommand\t[1]{[\![#1]\!]}`|上書き。mathjaxではllbracket等が規定で利用不可|

※本投稿でも Markdown 内で $\TeX$ を使用する際に活用しています。Markdownのソースを参照してみてください。

## 更新履歴
- 2025/02/25a 新規公開
- 2025/02/26a 文章順結合の演算子を変更(;→⨾)。その演算子の記号誤記を修正。
- 2025/02/28a モノ、エピ、分裂エピモノ性、逆射、終対象、始対象、双関手の一意性、双関手間の自然変換の一意性、極限、余極限を追加。
- 2025/02/28a 双関手の間の自然変換の自然性公理(スライディング則)を修正。
- 2025/03/01a 双関手の準同型を修正。
- 2025/03/04a homセットの並進式を追加、随伴の並進式を一部調整。
- 2025/03/04a 記号の見直し(アンダースコアとハイフンが似ているため、アンダースコアを点線に変更)。

## 参考文献
- 中平健治著, ストリング図で学ぶ圏論の基礎, 森北出版, 2025.
- 朝芝秀人著, グラフ表現で可視化する圏論, 共立出版, 2024.
- S.マックレーン著, 三好博之, 高木理訳, 圏論の基礎, 丸善出版, 2012.
- S.アウディ著, 前原和寿訳 圏論 原著第2版, 共立出版, 2015.
- T.レンスター著, 斎藤恭司監修, 土岡俊介訳, ベーシック圏論, 丸善出版, 2017.
- 雪田修一著, 圏論入門 Haskellで計算する具体例から, 日本評論社, 2020.
- https://en.wikipedia.org/wiki/Composition_of_relations (結合の文章順記法について)