以下のナタニエル・アーカーとディラン・マクダルメットの論文に、カン拡張と同様な、“左または右”の“拡張または持ち上げ”（正規表現で書くなら {左 | 右}{拡張 | 持ち上げ}）の定義が出てきます。
- [AM23]
- Title: The formal theory of relative moanads
- Authors: Nathanael Arkor, Dylan McDermott
- Submitted: 27 Feb 2023 (v1), 17 May 2023 (v2)
- Pages: 85p
- URL: https://arxiv.org/abs/2302.14014
左か右かを憶えるのがほんとに苦手で（「それでもカン拡張の左右を忘れてしまう」参照）困ってしまうわけですが、上記論文における {左 | 右}{拡張 | 持ち上げ} は、そもそも定義が複雑です。複雑な定義をするときに、どんな構文構造を使っているかを明確にすると、定義を納得する足しになります。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
%\newcommand{\pipe}{\mid }
%\newcommand{\ccol}[1]{\boldsymbol{#1} }
%\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\In}{\text{ in } }
%\newcommand{\Imp}{ \Rightarrow }
%\newcommand{\Iff}{\Leftrightarrow }
%\newcommand{\hyp}{\text{－} }
%\newcommand{\op}{\mathrm{op} }
%\newcommand{\id}{\mathrm{id} }
%\newcommand{\pto}{ \supseteq\!\to }
%\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\cpal}[1]{\mathfrak{#1} }
%\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\bdry}{\partial}
%\newcommand{\td}{ {2 + \varepsilon} }
\newcommand{\hto}{\not\to}
\newcommand{\adc}{\mathop{\circ,}} % anti-diagrammatic comma
`$
内容：
一般的な構文
$`n \ge 1`$ として、$`n`$項〈$`n`$変数〉の述語を次のように書きます。
$`\quad P(x_1, \cdots, x_n)`$
変数 $`x_1, \cdots, x_n`$ の素性〈すじょう〉を明らかにするための宣言の集まりを、この述語 $`P`$ の背景指標〈background signature〉と呼びましょう。背景指標は次の形になります。
$`\quad x_1 \in X_1\\
\quad \cdots\\
\quad x_n \in X_n
`$
もちろん、下のようにラムダ記法で一気に書いてもいいのですが、背景指標と述語を分離して記述することも多いです。
$`\quad \lambda\, (x_1\in X_1, \cdots, x_n\in X_n).P(x_1, \cdots, x_n)`$
$`X_i`$ は集合ですが、集合が圏や2-圏のホムセットのときは、同値な別の書き方をしてもかまいません。
$`\quad x \in \cat{C}(A, B) \;\iff\; x : A \to B \In \cat{C}\\
\quad x \in \cat{K}(A, B)(f, g) \;\iff\; x :: f \twoto g: A \to B \In \cat{K}
`$
述語 $`P`$ の第1変数に関してヒルベルトのイプシロンを適用すると、次の形のイプシロン項〈epsilon term〉が得られます。
$`\quad \varepsilon\, x_1. P(x_1, \cdots, x_n)`$
これは、次の意味です。
- 変数 $`x_2, \cdots, x_n`$ の値が具体化されたときに、述語 $`P`$ を満たす $`x_1`$ の具体値をひとつ返す関数
述語 $`P`$ を満たす $`x_1`$ がたくさんあるときは、テキトーにひとつ選んで返します。選ぶ行為が含まれるので、上記のイプシロン項により定義される関数を選択関数〈choice function〉と呼びます。この選択関数は、通常の関数と違って、同じ引数値に対して呼び出しごとに違う値を返すかも知れません。取り扱い注意です。
変数 $`x_2, \cdots, x_n`$ 達の具体値達に対して、述語 $`P`$ を満たす $`x_1`$ が存在しないとき、選択関数はほんとにテキトーになにか返しますが、ここでは、述語 $`P`$ を満たす $`x_1`$ が存在する状況だけに限定します。
次の表現を考えます。
$`\quad y := \varepsilon\, x_1. P(x_1, \cdots, x_n)`$
これは、自由変数 $`y`$ に、イプシロン記号で作られた選択関数の値を代入することを示します。この表現は、だいたい次の英語の文に相当します。
$`\quad y \text{ is a } x_1 \text{ such that } P(x_1, \cdots, x_n)`$
変数 $`x_1`$ はイプシロン記号で束縛されているので、同じ名前の自由変数を使っても問題ありません。
$`\quad x_1 := \varepsilon\, x_1. P(x_1, \cdots, x_n)`$
変数 $`x_2, \cdots, x_n`$ の値が具体化されたときに、述語 $`P`$ を満たす $`x_1`$ がただひとつに決まることが前もって分かっているなら、イプシロン項を次のように書きます。
$`\quad \varepsilon!\, x_1. P(x_1, \cdots, x_n)`$
このイプシロン項で定義される関数は通常の関数になります。次の表現は、通常の関数の値を $`y`$ に代入することを表します。
$`\quad y := \varepsilon!\, x_1. P(x_1, \cdots, x_n)`$
$`n = 1`$ のときは次のように書けます。
$`\quad y := \varepsilon!\, x. P(x)`$
これは、$`P(x)`$ であるような $`x`$ がただひとつ決まり、それを $`y`$ と名付けていることになります。$`y`$ は固有名として扱われます。
簡単な例： 平方根
2つの2項述語 $`\mrm{SqRoot}, \mrm{PosSqRoot}`$ を次のように定義します。
$`\quad \mrm{SqRoot}(x_1, x_2) := ({x_1}^2 = x_2)\\
\quad \mrm{PosSqRoot}(x_1, x_2) := ({x_1}^2 = x_2 \land x_1 \ge 0)
`$
この2つの述語の背景指標は次です。
$`\quad x_1 \in {\bf R}\\
\quad x_2 \in {\bf R}_{\ge 0}
`$
述語 $`\mrm{SqRoot}`$ に関しては、変数 $`x_2`$ の値が具体化されたときに、述語 $`\mrm{SqRoot}`$ を満たす $`x_1`$ がただひとつに決まることは保証できません。しかし、述語 $`\mrm{PosSqRoot}`$ に関しては保証できます。つまり、次の命題が成立します。
$`\quad \forall x_2 \in {\bf R}_{\ge 0}. \exists! x_1 \in {\bf R}.({x_1}^2 = x_2 \land x_1 \ge 0)
`$
イプシロン項による選択関数を作って、次の表現を考えることができます。
$`\quad y := \varepsilon\,x_1. \mrm{SqRoot}(x_1, x_2)\\
\quad y := \varepsilon!\,x_1. \mrm{PosSqRoot}(x_1, x_2)
`$
これらはだいたい次の英語の文に対応します。冠詞 a, the の違いに注意してください。
$`\quad y \text{ is a }x_1 \text{ such that } \mrm{SqRoot}(x_1, x_2)\\
\quad y \text{ is the }x_1 \text{ such that } \mrm{PosSqRoot}(x_1, x_2)
`$
もう少し簡略かつ自然に表現すれば：
$`\quad y \text{ is a } \mrm{SqRoot}\text{ (square root) } \text{ of } x_2\\
\quad y \text{ is the } \mrm{PosSqRoot}\text{ (positive square root) } \text{ of } x_2
`$
複雑な例： 仮想二重圏の右持ち上げ
冒頭で引用した論文 [AM23] における右持ち上げ〈right lift〉を例にします。右持ち上げを定義するための3項述語を $`\mrm{RightLift}`$ とすると、それは次のように書けます。
$`\quad \mrm{RightLift}( (x, \varpi), q, p)`$
第2変数 $`q`$ と第3変数 $`p`$ を具体化したときに、第1変数 $`(x, \varpi)`$（ペアでひとつの変数とみなす）は一意的には決まりません。しかし、とある同値関係に対する up-to-equivalence で一意的とは言えます。次のイプシロン記号は、なんらかの同値関係に対して up-to-equivalence で一意的に目的の値が決まるときに使うとします。
$`\quad \tilde{\varepsilon}!`$
述語 $`\mrm{RightLift}`$ に関して、次の表現は意味を持ちます。
$`\quad (x, \varpi) := \tilde{\varepsilon}!(x, \varpi).\mrm{RightLift}( (x, \varpi), q, p)`$
up-to-equivalence で一意的のときも冠詞 the を使うとすると、上記の表現はだいたい次の英文に相当します。
$`\quad (x, \varpi) \text{ is the } \mrm{RightLift} \text{ of } q, p`$
習慣により、$`q, p`$ のカンマの代わりに through を使うようです。
$`\quad (x, \varpi) \text{ is the } \mrm{RightLift} \text{ of } q \text{ through } p`$
$`x`$ は $`q, p`$ からほぼ一意に決まるので、$`x = q \blacktriangleleft p`$ という記法を使います。$`\varpi`$ も $`q, p`$ からほぼ一意に決まるのですが、なぜかコッチには演算子記号は用意していません*1。$`\blacktriangleleft`$ を使って書くと：
$`\quad (q \blacktriangleleft p, \varpi) \text{ is the } \mrm{RightLift} \text{ of } q \text{ through } p`$
述語 $`\mrm{RightLift}`$ の引数変数達 $`(x, \varpi), q, p`$ の背景指標が複雑です。 [AM23] とは違う記法を使った箇所があります*2が、背景指標は次のようです。
$`\quad \mathbb{X} \in |{\bf VirtualDoubleCAT}|\\
\quad X, Y, Z \in |\mathbb{X}|\\
\quad p : Y \hto Z \In \mathbb{X}\\
\quad q : X \hto Z \In \mathbb{X}\\
\quad x : X \hto Y \In \mathbb{X}\\
\quad \varpi :: p \adc x \twoto q \In \mathbb{X}
`$
述語 $`\mrm{RightLift}`$ では全称限量子を使っているので、表〈おもて〉には現れない束縛変数達も出てきます。それは、$`r_1, \cdots, r_n, \phi`$ という変数達です。述語 $`\mrm{RightLift}`$ の条件は等式として記述できるのですが、その等式をテキストで書くのは容易ではありません。ペースティング図の画像コピーを以下に貼ります。
束縛変数達 $`r_1, \cdots, r_n, \phi`$ にも背景指標が必要ですが割愛します。
自由変数と束縛変数の背景指標を書き下すのが面倒ではありますが、述語の第2変数と第3変数が具体値として与えられたとき、第1変数の値が（up-to-equivalneceで）一意に決まるので、それに呼び名を付けよう、という基本方針は前節の正平方根〈positive square root〉の例と同じです。
