一部の証明支援系／プログラミング言語において、シグマ型を直積型と同じ '$`\times`$' で、パイ型を指数型と同じ '$`\to`$' で書くという記法が採用されています。これは短く書けて便利なのですが、当然ながら混乱を招くので、少し変更した形で紹介します。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mfk}[1]{ \mathfrak{#1} }
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\twoto}{ \Rightarrow } % use
\newcommand{\LL}{\langle} % List Left
\newcommand{\LR}{\rangle} % List Right
`$
内容：
例題
例題としては、昨日の記事「最近の型理論のハマリ所」に出てきた、第一射影のコンビネータ $`\mfk{p}`$ のプロファイルを、依存型を使って記述する問題を考えます。
$`\mfk{p}`$ の由来・氏素性はともかくとして、$`\mfk{p}`$ の引数と値の仕様（それがプロファイル）は、次のように書けます。
$`\text{For }X, Y\in |\cat{C}|\\
\text{For } B \in \mrm{Ty}(Y)\\
\text{For }g \in \cat{C}(X, Y\cdot B)\\
\quad \mfk{p}^{X, Y, B}(g) \in \cat{C}(X, Y)
`$
$`\mfk{p}`$ は関数〈写像〉ですが、$`\mfk{p}^{X, Y, B}(g)`$ という書き方は、$`X, Y, B`$ というパラメーターにより $`g\mapsto \mfk{p}(g)`$ という関数が決まる高階関数（関数値の関数）という“感じ”がします。この“感じ”を明示的に書くために、シグマ型とパイ型を使ってみます。
まず、次のようなシグマ型を考えます。ブラケットは指数型〈関数空間型〉の型構成子です。
$`\quad
\sum_{(X, Y)\in |\cat{C}|^2} \sum_{B \in \mrm{Ty}(Y)}
[
\cat{C}(X, Y\cdot B),\, \cat{C}(X, Y)
]
`$
このシグマ型に対してベースを
$`\quad \sum_{(X, Y)\in |\cat{C}|^2} \mrm{Ty}(Y)`$
と考えて、次の射影を考えます。
$`\quad
\sum_{(X, Y)\in |\cat{C}|^2} \sum_{B \in \mrm{Ty}(Y)}
[
\cat{C}(X, Y\cdot B),\, \cat{C}(X, Y)
]
\to \sum_{(X, Y)\in |\cat{C}|^2} \mrm{Ty}(Y)
`$
この射影のセクションが $`\mfk{p}`$ です。
$`\quad \mfk{p} : \sum_{(X, Y)\in |\cat{C}|^2} \mrm{Ty}(Y) \to
\sum_{(X, Y)\in |\cat{C}|^2} \sum_{B \in \mrm{Ty}(Y)}
[
\cat{C}(X, Y\cdot B),\, \cat{C}(X, Y)
]
`$
シグマ型の射影のセクションは、パイ型の要素なので、次のように書けます。
$`\quad \mfk{p} \in \prod_{( (X, Y), B) \in \sum_{(X, Y)\in |\cat{C}|^2} \mrm{Ty}(Y)}
[
\cat{C}(X, Y\cdot B),\, \cat{C}(X, Y)
]
`$
なんかゴチャゴチャしてますね。
短縮記法
$`A, B`$ を、型項（型を表現する記号的表現）とします。型項のなかには変数〈パラメーター〉が含まれてもかまいません。シグマ型とパイ型の型構成子を、二項演算子記号で表します。
- シグマ型を構成する二項演算子記号を $`\ltimes`$ とする ： $`(x\in A) \ltimes B`$
- パイ型を構成する二項演算子記号を $`\twoto`$ とする ： $`(x\in A) \twoto B`$
$`x`$ は変数名で、どんな名前を使ってもかまいません。型理論では所属記号（$`\in`$）ではなくてコロン（$`:`$）ですが、まーどっちでもいいとします。
前節の $`\mfk{p}`$ のプロファイル（$`\mfk{p}`$ が所属する集合）を、この記法で書き直してみます。
$`\quad
( ( (X, Y), B) \in ( (X, Y) \in |\cat{C}|^2 ) \ltimes \mrm{Ty}(Y) )
\twoto
[
\cat{C}(X, Y\cdot B),\, \cat{C}(X, Y)
]
`$
変数名の繰り返し記述を避けるために次の書き方を許したほうがいいですね。
$`\quad
( ( (X, Y) \in |\cat{C}|^2 ) \ltimes (B \in \mrm{Ty}(Y)) )
\twoto
[
\cat{C}(X, Y\cdot B),\, \cat{C}(X, Y)
]
`$
通常の指数型はパイ型の特殊なものなので、同じ記法に統一します。
$`\quad
( ( (X, Y) \in |\cat{C}|^2 ) \ltimes (B \in \mrm{Ty}(Y)) )
\twoto
(
\cat{C}(X, Y\cdot B)\twoto \cat{C}(X, Y)
)
`$
二項演算子記号 $`\ltimes`$ のほうが優先度が高く、二項演算子記号 $`\twoto`$ は右結合的という規則を設けて省略できる括弧を省略すると：
$`\quad
( (X, Y) \in |\cat{C}|^2 ) \ltimes (B \in \mrm{Ty}(Y))
\twoto
\cat{C}(X, Y\cdot B)\twoto \cat{C}(X, Y)
`$
意味は変わりませんが、$`\ltimes`$ を2個使ってみます。
$`\quad
(X \in |\cat{C}|) \ltimes (Y \in |\cat{C}| ) \ltimes (B \in \mrm{Ty}(Y))
\twoto
\cat{C}(X, Y\cdot B)\twoto \cat{C}(X, Y)
`$
二項演算子記号 $`\ltimes`$ は左結合的と約束します。
演算子の優先度や結合性（左か右か）の約束に過度に頼ると、可読性が悪くなる（どこで切っていいか分からない）ので要注意ですが、見た目がフラットになるのでスッキリします。
追記
第ニ射影 $`\mfk{q}`$ は第一射影 $`\mfk{p}`$ より複雑になります。$`\mfk{q}^{X, Y, B}(g)`$ と書いたとき、$`g`$ によっても値の集合（余域）が変化します。
$`\quad
(X \in |\cat{C}|) \ltimes (Y \in |\cat{C}| ) \ltimes (B \in \mrm{Ty}(Y))
\ltimes (g \in \cat{C}(X, Y\cdot B))\\
\qquad \twoto
\mrm{Sect}(\rho^{X, \mrm{Ty}(\mfk{p}^{X, Y, B}(g) )(B) } )
`$
さらに追記
二重矢印 $`\twoto`$ を、2-射のプロファイル記述や1-変換手空間として使いたくて、かつパイ型も使いたいときは、二重矢印の奪い合いになってしまいますね。そのときは、パイ型は $`\leadsto`$ かな。
- $`\to`$ ： 1-射のプロファイル〈居所〉、0-変換手空間
- $`\twoto`$ ： 2-射のプロファイル〈居所〉、1-変換手空間
- $`\Rrightarrow`$ ： 3-射のプロファイル〈居所〉、2-変換手空間
- $`\rightrightarrows`$ ： コンビネータのプロファイル〈居所〉、コンビネータ空間
- $`\leadsto`$ ： パイ型〈依存関数空間型〉の型構成子
これは矢印記号の使い方の問題だな（「矢印記号の使用法と読み方 2024」参照）。
