/-!
# 付録B：日英用語集と訳語の方針

この付録は数学・論理学・型理論で通用する日本語を優先し、Lean固有名は原綴りを保ちます。
訳語だけで国際的な文献検索が困難にならないよう、各語を概念として導入する本編の初出では
英語を併記します。序文、目次、読書案内で名称だけを予告する箇所は初出に数えません。

## 基礎と論理

| English | 本書の日本語 | 注意 |
|---|---|---|
| expression | 式 | 構文上の総称。型が付いたものだけを項とは限らない文脈もある |
| term | 項 | 判断 `t : A` の左側にある型付きの式 |
| type | 型 | 単なる集合と最初から同一視しない |
| metalanguage / object language | メタ言語／対象言語 | 形式体系を記述する側／記述される側の言語 |
| free / bound variable | 自由変数／束縛変数 | どの束縛子のスコープに属するかで区別する |
| scope | スコープ（有効範囲） | 束縛子が変数を束縛する構文上の範囲 |
| alpha-equivalence | α同値 | 束縛変数名の一貫した変更を同一視する関係 |
| capture-avoiding substitution | 変数捕獲を避ける代入 | 自由変数を誤って束縛しない代入 |
| beta-reduction / eta-reduction | β簡約／η簡約 | 適用の計算／関数の外延的な縮約を区別する |
| redex / normal form | 簡約可能式（redex）／正規形（normal form） | 一段簡約できる部分式／それを含まない式 |
| proposition | 命題 | Leanでは `Prop` に属する型 |
| proof term | 証明項 | 命題を型として持つ項 |
| implication | 含意 | `P → Q` |
| logical connective | 論理結合子 | 連言・選言・否定・同値など |
| predicate | 述語 | `α → Prop` のように値から命題を作る関数 |
| universal / existential quantifier | 全称量化子／存在量化子 | 記号は `∀`／`∃` |
| constructive logic | 構成論理 | 「直観主義論理」と重なるが、哲学的立場まで常に含意しない |

## 等式と型理論

| English | 本書の日本語 | 注意 |
|---|---|---|
| definitional equality | 定義的等しさ | 計算・展開でkernelが同一視する関係 |
| propositional equality | 命題的等しさ | `x = y` という型内部の命題 |
| function extensionality | 関数外延性 | 点ごとの等しさから関数の等しさを得る原理 |
| type family | 型族 | 値を添字として型を返す関数 |
| dependent function type / Π-type | 依存関数型／Π型 | `(x : A) → B x` |
| dependent pair type / Σ-type | 依存対型／Σ型 | `Sigma B` |
| subtype | 部分型 | Leanの `{x : A // p x}`、`Subtype p` |
| refinement type | 篩型 | 本編で概念を導入する初出に原語を併記し、以後は日本語で表記する |
| indexed inductive family | 添字付き帰納族 | 「添字付き帰納型」より、型族全体を指すことが明確 |
| quotient type | 商型 | 同値関係で代表元を同一視する型 |
| type class | 型クラス | 数学の「類」やサブクラスではなく探索機構を伴う構造 |
| universe polymorphism | 宇宙多相 | 型引数の多相性と区別する |
| typing judgment / derivation | 型判断／型導出 | `Γ ⊢ t : A` という判断／規則から成る証拠の木 |
| context | 文脈 | 自由変数について仮定した型を順序付きで記録する |
| sort / kind | ソート（sort）／種（kind） | 型を分類する階層。訳語だけに固定せず原語を併記する |
| pure type system | 純粋型システム（PTS） | sort公理とΠ形成規則で型付きラムダ計算を記述する枠組み |
| lambda cube | ラムダ・キューブ | 三種類の追加依存を組み合わせた八体系の包含図 |
| Calculus of Constructions | 構成計算（CoC） | 訳語が一様でないため初出では英語と略号を必ず併記する |
| Calculus of Inductive Constructions | 帰納構成計算（CIC） | CoCへ帰納的定義を組み込む系統の総称 |

## 普遍性と圏論

| English | 本書の日本語 | 注意 |
|---|---|---|
| morphism | 射 | `Type` の例では関数 |
| universal property | 普遍性 | 「普遍性質」も用いられるが本書では短い形に統一 |
| initial / terminal object | 始対象／終対象 | 「始域」「終域」と混同しない |
| product / coproduct | 積／余積 | 直積・直和という具体的実現と普遍的役割を区別する |
| duality | 双対性 | 全ての射と合成順序を反転する操作を含む |
| opposite category | 反対圏 | 射と合成順序を反転した圏 |
| functor / natural transformation | 関手／自然変換 | 射の構造を保つ対応／関手間の射の族 |
| limit / colimit | 極限／余極限 | 錐／余錐の普遍対象として定義する |
| adjunction | 随伴 | homの自然同型、単位・余単位、普遍射の定式化を比較する |
| representable functor | 表現可能関手 | hom関手と自然同型な関手 |
| universal element | 普遍元 | 表現における恒等射の像で、全要素を分類する |
| Yoneda lemma / embedding | 米田の補題／米田埋め込み | 人名は「米田」に統一し、自然な全単射と完全忠実関手を区別する |
| unit / counit | 単位／余単位 | 随伴・モナドの自然変換。対象内部の単位元とは区別する |
| presheaf / sheaf | 前層／層 | 前層は反変関手、層は貼り合わせ条件を満たす前層 |
| sieve | 篩 | 層論の用語。篩型とは無関係 |
| Grothendieck topology / site | Grothendieck位相／サイト | 対象ごとの被覆篩の指定／圏とその指定の組 |
| compatible family / amalgamation | 整合族／貼り合わせ | 局所要素の制限が一致する族／それらを生む大域要素 |
| sheafification | 層化 | 前層から層への普遍射で、層の包含関手の左随伴 |
| elementary / Grothendieck topos | 初等トポス／Grothendieckトポス | 有限極限・デカルト閉性・部分対象分類子による公理的概念／サイト上の層として表示される概念 |
| subobject classifier / characteristic morphism | 部分対象分類子／特性射 | モノ射を真の射の引戻しとして分類する対象／分類を与える一意な射 |
| truth-value object / power object | 真理値対象／冪対象 | 内部真理値を担う対象 `Ω`／部分対象族を分類する指数対象 `Ω^A` |
| internal logic / internal language | 内部論理／内部言語 | 圏内の対象と射によって解釈される論理／それを構文的に記述する言語 |
| Kripke–Joyal semantics | Kripke–Joyal意味論 | 層トポスの内部判断を段階と被覆に関する外部条件へ翻訳する意味論 |
| geometric morphism | 幾何学的射 | 有限極限を保存する逆像関手を左随伴に持つトポス間の射 |
| Boolean topos | Booleanトポス | 内部論理で排中律が成り立つトポス。初等トポスの追加条件 |
| monad / comonad | モナド／余モナド | 単位・乗法／余単位・余乗法を持つ自己関手 |
| comparison functor / monadic | 比較関手／モナド的 | 随伴の定義域からモナド代数圏への関手／それが圏同値であること |
| end / coend | end／coend | wedgeの終対象／cowedgeの始対象。訳語へ固定せず原語を用いる |
| wedge / cowedge | wedge／cowedge | 双関手の対角成分へ入る／対角成分から出る双自然な射族 |
| dinatural transformation | 双自然変換 | 一つの変数が反変・共変の二位置に現れるときの整合する成分族 |
| left / right Kan extension | 左Kan拡張／右Kan拡張 | 前合成に対する左／右の普遍的な関手延長 |
| monoidal category | モノイダル圏 | テンソル積、単位対象、結合子、単位子と整合性公理を持つ圏 |
| tensor unit / associator / unitor | テンソル単位／結合子／単位子 | テンソルの単位対象／括弧変更の同型／単位対象を除く同型 |
| coherence | 整合性 | 構造同型から作る比較射が選択した経路に依存しないこと |
| enrichment / enriched category | 豊穣化／豊穣圏 | hom集合をモノイダル圏の対象へ置き換えること／その構造を持つ圏 |
| enriched functor / enriched natural transformation | 豊穣関手／豊穣自然変換 | hom対象の構造を保存する関手／一般化要素を成分に持つ自然変換 |
| hom-object | hom対象 | 豊穣圏で二対象間の射を表す値圏の対象。通常のhom集合と区別する |
| exponential object | 指数対象 | `Hom(A×X,B)≃Hom(X,B^A)` を自然に実現する対象 `B^A` |
| evaluation morphism / currying | 評価射／カリー化 | `A×B^A→B`／積を始域に持つ射を指数対象への射へ移す操作 |
| internal hom | 内部hom | 外部のhom集合を圏内の対象として表現する対象。指数対象はデカルト積に対する内部hom |
| closed object | 閉対象 | `A⊗-` が右随伴 `[A,-]` を持つ対象 `A`。左右の規約はhom同値で確認する |
| monoidal closed category | モノイダル閉圏 | 全対象が閉対象であり、テンソルに対する内部homを持つモノイダル圏 |
| coevaluation morphism | 余評価射 | 随伴 `A⊗-⊣[A,-]` の単位の成分 `X→[A,A⊗X]` |
| linear logic / linear type | 線形論理／線形型 | 弱化・縮約を無条件に許さず、仮定の使用を推論規則で追跡する論理／型体系 |
| linear implication | 線形含意 | 内部homで解釈される含意 `A⊸B`。入力資源を重複せず関数へ渡す |
| multiplicative / additive connective | 乗法的／加法的結合子 | 文脈を分割する結合子／同じ文脈に対する選択を表す結合子 |
| exponential modality | 指数様相 | 複製・破棄を制御して許す `!` と、その双対 `?` |
| *-autonomous category | *-自律圏 | 線形否定を表す双対化を備えた対称モノイダル閉圏 |
| linear/non-linear model | linear/non-linearモデル（LNLモデル） | デカルト閉な非線形世界と対称モノイダル閉な線形世界を随伴で結ぶモデル |
| computational effect | 計算効果 | 失敗、状態、非決定性、入出力など、値の返却に加わる計算上の振舞い |
| Kleisli arrow / composition | Kleisli射／Kleisli合成 | 射 `X→TY` と、モナドの乗法を用いる効果付き関数の合成 |
| strong monad / strength | 強いモナド／強さ | モノイダル積と両立する射 `A⊗TB→T(A⊗B)` を備えたモナド／その射 |
| algebraic effect / operation | 代数的効果／代数的演算 | 演算と方程式による代数理論の自由モデルとして表せる効果／その生成演算 |
| effect handler | エフェクトハンドラ | 効果演算の解釈を指定し、自由な計算を別の代数へ写す仕組み |
| monad transformer | モナド変換子 | 既存モナドへ別の効果層を加える構成。層の順序は一般に意味へ影響する |
| adequacy | 適切性 | 表示と停止・観察結果などの操作的性質を対応づける意味論上の定理 |
| cartesian closed category | デカルト閉圏 | 有限積と指数対象を持つ圏 |
| categorical semantics | 圏論的意味論 | 構文の型・文脈・判断・代入を対象・積・射・合成として解釈する意味論 |
| denotation / denotational semantics | 表示／表示的意味論 | 式へ割り当てる数学的対象／その表示によって式を解釈する意味論 |
| syntactic category | 構文圏 | 型や文脈を対象、適切な項の同値類を射として構成する圏 |
| soundness / completeness | 健全性／完全性 | 構文的導出が意味論で成立すること／意味論的妥当性を構文で導出できること |
| slice category | スライス圏 | 対象 `I` への射を対象、`I` 上の可換三角形を射とする圏 `C/I` |
| indexed category | 添字圏 | 基底対象ごとに圏を、基底射ごとに再添字付け関手を割り当てる反変擬関手 |
| reindexing | 再添字付け | 基底射 `f:J→I` に沿って `I` 上の対象を `J` 上へ引き戻す操作 `f⁎` |
| cartesian morphism | Cartesian射 | 基底射の上にある射を垂直射を通じて一意に分解する普遍的な持ち上げ |
| fibration / opfibration | ファイブレーション／opfibration | Cartesian／cocartesian持ち上げにより反変／共変な移動を表す射影関手 |
| cleavage | 切断（cleavage） | 各基底射と終域上の対象にCartesian持ち上げを整合的に選ぶデータ |
| Grothendieck construction | Grothendieck構成 | 添字圏の基底対象とファイバー対象を依存対として一つの全圏へ束ねる構成 |
| locally cartesian closed category | 局所デカルト閉圏 | 各スライス圏がデカルト閉圏である圏 |
| exponentiable morphism | 指数化可能射 | その射に沿う引戻し関手が右随伴を持つ射 |
| dependent sum / product | 依存和／依存積 | 再添字付け `f⁎` の左随伴 `Σ_f`／右随伴 `Π_f` |
| dependent currying | 依存カリー化 | `Hom(f⁎A,X)≃Hom(A,Π_fX)` によって射を転置する操作 |
| display map | 表示射 | 文脈 `Γ` 上の型を表す射 `Γ.A→Γ` |
| section | 切断 | 射 `p:E→B` に対し `s≫p=𝟙 B` を満たす右逆射 `s:B→E` |
| contextual category | 文脈圏（contextual category） | 文脈拡張を階層的に備え、依存型の文脈と代入を表す圏 |
| category with families | 族付き圏（category with families; CwF） | 文脈ごとの型・項、代入作用、文脈拡張を構文に近い形で備えるモデル |
| fibration / indexed category | ファイブレーション／添字圏 | 依存する対象と基底変更を圏論的に記述する枠組み |
| well-definedness | 適切に定義されること | 商では「代表元の選択によらないこと」と具体化する |

## 帰納・余帰納・再帰

| English | 本書の日本語 | 注意 |
|---|---|---|
| induction / coinduction | 帰納法／余帰納法 | 帰納法は有限生成、余帰納法は観察可能な振舞を原理とする |
| recursion / corecursion | 再帰／余再帰 | 値を分解して定義する／観察を生成し続ける |
| least / greatest fixed point | 最小／最大不動点 | 順序と単調作用素に依存する定義 |
| initial algebra / final coalgebra | 始代数／終余代数 | 帰納・余帰納を関手の普遍性として記述する |
| endofunctor algebra / coalgebra | 自己関手の代数／余代数 | 構造射 `F(A)→A`／`S→F(S)`。モナド代数と区別する |
| polynomial functor | 多項式関手 | `P(X)=Σa.B(a)→X` のように形と位置から一層を表す関手 |
| W-type | W型 | 形と位置族から生成される整礎木。対応する多項式関手の始代数を与える |
| free algebra | 自由代数 | 生成元からの写像が代数準同型へ一意に延長される代数 |
| catamorphism / anamorphism | カタモルフィズム（catamorphism; fold）／アナモルフィズム（anamorphism; unfold） | 原語と代表的な計算名を併記する |
| Lambek's lemma | Lambekの補題 | 始代数・終余代数の構造射が同型になる定理 |
| total space | 全空間 | 型族 `P:A→Type` の従属和 `Σa,P(a)`。依存するファイバーを一つの型へ束ねる |
| predicate lifting | 述語持ち上げ | 基底上の述語やファイバー構造へ関手の作用を持ち上げる構成 |
| bisimulation | 双模倣 | 余帰納的な振舞同値を示す関係 |
| behavioral equivalence | 振舞等価 | 状態を終余代数へ写した像が等しいことによる同値 |
| relation lifting | 関係持ち上げ | 対象間の関係から関手で写した対象間の関係を作る操作 |
| well-founded recursion | 整礎再帰 | 減少を整礎関係で示す停止する再帰 |
| productivity | 生産性 | 余再帰が有限時間で次の観察を供給できる性質 |
| potential / actual infinity | 潜在的無限／実無限 | 任意の有限段階を越えられること／無限の全体を一対象として扱うこと |
| inverse system / inverse limit | 逆系／逆極限 | 反対向きの結合写像を持つ図式／その整合する糸を分類する極限 |
| compatible thread | 整合する糸 | 逆系の各段階の要素を結合写像と整合するよう選んだ族 |
| recursive type / recursive domain equation | 再帰型／再帰領域方程式 | 型式 `μX.T`／領域そのものを未知数とする方程式 `D≅F(D)` |
| iso-recursive / equi-recursive type | iso-recursive型／equi-recursive型 | fold/unfoldを項で明示する体系／展開を型同値で扱う体系 |
| fixed object | 不動点対象 | 自己関手 `F` に対して同型 `F(D)≅D` を持つ対象。始代数や終余代数とは限らない |
| algebraic completeness / compactness | 代数的完備性／代数的コンパクト性 | 始代数の存在／始代数と終余代数が逆の構造射を介して一致する性質 |
| embedding–projection pair | 埋込み・射影対 | 埋込みと射影が逆法則と近似不等式を満たす射の対 |

## 表記上の原則

1. 本編で概念を導入する初出では「日本語（English）」、その後は日本語を使う。
2. Leanの宣言名 `Subtype`、`Quotient.lift` などは翻訳しない。
3. 日本語訳が分野で一意でない場合は原語を残す。
4. 歴史的文献の語を現代用語へ翻訳した場合、同じ形式体系だとは推論しない。
-/