--- title: "基礎語彙" module: Base.Prelude lang: ja site: "Bedrock" description: "基礎語彙" stage: "基礎" reading_order: 2 canonical: https://bedrock.institute/ja/Base.Prelude.html html: Base.Prelude.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/Base/Prelude.lagda.md prerequisites: [] routes: [common-foundations] translations: [https://bedrock.institute/en/Base.Prelude.md, https://bedrock.institute/zh/Base.Prelude.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # 基礎語彙 集合論を学ぶとき、私たちは集合とその要素、集合の間の関係や関数について考えます。定義は扱う対象が何であるかを示し、定理はその対象がどのような性質を持つかを述べ、証明はその性質がなぜ成り立つかを明らかにします。本書では、集合論を**対象理論**、立方型理論を**メタ理論**とします。つまり、立方型理論の中で集合論のモデルを構成し、集合論の文を解釈して、そのモデルが所定の公理や定理を満たすことを証明します。 これらの構成と証明は、証明支援系 Agda を用いて記述し、検査します。Agda は形式言語とその検査機構を提供し、立方型理論はこの形式化の数学的基礎を与え、Cubical ライブラリはその基礎の上で築かれた定義や定理を集めています。本書では、対象理論の形式化を支えるこの Cubical Agda の環境を**ホスト**と呼びます。したがって、後に現れる「ホストの型」「ホストの関数」「ホストレベルの構成」はいずれもメタ理論の側に属し、集合論のモデル内部の対象ではありません。 これらを読み解くために、まずはホストの基礎語彙に慣れていきましょう。 本章は、この言語の基礎概念から始めます。一つずつ取り上げ、その意味と、数学の主張や証明での使い方を見ていきます。すべての記号を一度に覚える必要はありません。後の章で同じ概念に繰り返し出会ううちに、その使い方にも慣れていくでしょう。必要なときには本章に戻り、概念の意味を確かめることもできます。 ## 語彙の出所をたどる そのような参照をしやすくするために、まず、これらの基礎概念がどこから来るのか、そして定義をどう探せばよいのかを説明します。 後の章では、冒頭に `import` を含む文が現れます。これは、どのモジュールからどの名前を導入するかを示し、その後の議論で使う既存の概念や結果を明らかにします。見慣れない名前があれば、まずこれらの文で出所を確かめ、名前をクリックして具体的な定義を参照できます。 本章にまとめる基礎語彙は、この約束の例外です。全書を通じて頻繁に使うため、`Base.Prelude` にまとめ、後の章では個々の名前を列挙せずに一括して導入します。ここでは Cubical ライブラリから選んだ定義を列挙し、本書を読むために必要な意味と使い方を説明しますが、ライブラリ内部の構成や証明を一つずつ展開することはしません。さらに学びたい場合は、名前のリンクから元の定義を参照したり、Cubical ライブラリの文書や立方型理論の学習資料を読んだりできます。 これらの語彙を導入する前に、二行の短いコードを説明します。 ```agda {-# OPTIONS --cubical --safe --guardedness #-} module Base.Prelude where ``` これで二行の役割と、`where` の後にあるモジュール本体が分かりました。ここから概念を一つずつ見ていきましょう。 ## 宇宙レベル 型理論では、型の大きさを区別しなければなりません。すべての型を量化する型があれば、それは自分自身を含んでしまいます。そこでホストは、各レベル `ℓ : Level` に一つずつある宇宙 `Type ℓ` へ型を分類します。代数的には、宇宙レベルは後続演算を備えた最小元付き結び半束をなします。`ℓ-zero` が最小元、`ℓ-suc` が後続演算、`ℓ-max` が二項の結びです。各宇宙はそれ自身も型です。
Type ℓ : Type (ℓ-suc ℓ)
本書が「すべての集合」や「すべての命題」のような全体を扱うとき、主張に付いたレベルが、その全体をどの大きさとして扱うかを記録します。 ```agda open import Cubical.Foundations.Prelude public using ( Type; Level; ℓ-zero; ℓ-suc; ℓ-max ) ``` ## Π 型 本書の後の多くの構成では、各対象に対して、それに依存するデータを与える必要があります。Π 型はこの関係を表す基本形です。 型 `A` と、各 `x : A` に対して型 `B x` が与えられたとき、Π 型を作ります。
(x : A) → B x
Π 型の元を**依存関数**と呼びます。依存関数 `f` は、各 `x : A` に対して `B x` の元 `f x` を与えます。結果が属すべき型は入力 `x` に依存するため、入力を定めて初めて対応する出力の型が定まります。 `B` が `x` に依存しない場合、すべての出力は同じ型に属し、依存関数は通常の関数に特化します。
A → B
通常の関数は各入力に対して同じ型の出力を与えますが、Π 型は各 `x` に対して、対応する型 `B x` に属するデータを与えます。 ## Σ 型 本書の後の多くの構成では、ある対象と、それに依存する一つのデータを一緒に保つ必要があります。Σ 型はこの関係を表す基本形です。 型 `A` と、各 `x : A` に対して指定された型 `B x` があるとき、Σ 型を作ります。
`Σ` (x : A) B x
Σ 型の元を**依存対**と呼びます。まず `a : A` を選び、次に `B a` の元 `b` を選びます。得られた対を `(a , b)` と書きます。`a` を**第一成分**、`b` を**第二成分**と呼びます。第二成分の型は `a` に依存するため、第一成分を定めて初めて、第二成分がどの型に属すべきかが決まります。 `B` が `x` に依存しない場合、すべての第二成分は同じ型に属し、依存対は通常の積に特化します。
A × B := `Σ` (_ : A) B
通常の積は互いに独立した二つの元を一緒にしますが、Σ 型は、ある `a` と、対応する型 `B a` に属するデータを一緒にします。依存対は `_,_` で作り、`fst` で第一成分を、`snd` で第二成分を取り出します。 Π 型が扱うのは「すべての `x` に対して、`x` に依存するデータを与えること」です。Σ 型が扱うのは「一つの `x` を選び、それに依存するデータと一緒に収めること」です。 第二成分を、第一成分の性質を示す証明にすることもできます。本書では、後の議論でその性質を使えるよう対象とともに携える証明を**証明書**と呼びます。証明書は通常の Agda の証明であり、この名前は依存対の中で果たす役割を強調しています。 ```agda open import Cubical.Data.Sigma public using ( Σ; Σ-syntax; _×_; _,_; fst; snd ) ``` ## レコード型 レコード型は、複数の Σ 型を入れ子にしたものに対する構文糖と考えられます。たとえば、元 `a : A`、`a` に依存する元 `b : B a`、さらにその両方に依存する証明 `c : C a b` を一緒にまとめるとします。対応する入れ子の型は次のものです。
`Σ` (a : A) `Σ` (b : B a) C a b
その元は次の形になります。
(a , (b , c))
Agda では、キーワード `record` がレコード型の宣言を開始し、続いて各成分にフィールド名を与えます。レコード型の元を構成するには、すべてのフィールドに対応する値を与えなければなりません。レコード宣言では、キーワード `constructor` を使ってこの構成操作に名前を付けることもできます。この名前をレコード型の**構成子**と呼びます。構成子は依存関係の順にフィールドの値を受け取り、一つのレコードへ組み立てます。三つのフィールドが順に `a`、`b`、`c` に対応するなら、`mkR` という構成子による構成は平らに次のように書けます。
mkR a b c
これは入れ子の Σ 型の値 `(a , (b , c))` と同じデータを表しますが、入れ子を表面に出しません。フィールド名は対応する成分を直接取り出す射影として働きます。そのため、成分が何段目にあるかを覚えたり、`fst` と `snd` を何度も組み合わせたりする必要がありません。レコード型は入れ子になった Σ 型の依存構造を保ちながら、名前付きフィールドと構成子によって大きなデータのまとまりを明瞭な平面インターフェースとして提示します。宣言、構成、射影の詳細は [Agda のレコード型の文書](https://agda.readthedocs.io/en/v2.8.0/language/record-types.html)を参照してください。 ## 宇宙レベル間の移動 ここで使う Agda の型宇宙は累積的ではありません。`Type ℓ` の要素が自動的に `Type (ℓ-suc ℓ)` の要素になるわけではありません。レベル間で型を移すには、明示的な演算 `Lift` が必要です。 `Lift ℓ A` はそれ自身がレコード型です。フィールドは元の型 `A` の元を保存する `lower : A` 一つだけで、構成子は `lift` です。`a : A` を与えると、構成子は `lift a : Lift ℓ A` を作ります。逆に `b : Lift ℓ A` があれば、フィールド射影 `lower b` が保存された `A` の元を取り出します。 `lift` と `lower` は `A` と `Lift ℓ A` の間で互いに逆です。その二つの向きを別々の等式が表します。
`lower (lift a) ≡ a`
`lift (lower b) ≡ b`
第一の等式は、元を包んですぐ取り出せば元の要素に戻ることを述べます。第二の等式は、持ち上げられたレコードから元を取り出して包み直せば、元のレコードに戻ることを述べます。したがって `Lift` は型を提示する宇宙と元の表現を変えますが、数学的な情報を加えたり失ったりしません。 より正確には、`A` が `Type ℓ₁` に住むなら、`Lift ℓ₂ A` は `Type (ℓ-max ℓ₁ ℓ₂)` に住みます。一方の宇宙レベルがすでに他方より高ければ、`ℓ-max` はそのレベルを保ちます。そうでなければ、両方を収めるのに十分な共通の宇宙レベルを与えます。したがって `Lift` は型を決まった段数だけ持ち上げるのではなく、現在の二つのレベルにとって十分大きな宇宙へ型を置きます。 型は常にこの方法で上へコピーできますが、一般には下へ動かせません。 ```agda open import Cubical.Foundations.Prelude public using ( Lift; lift; lower ) ``` ## 等式とパス 通常の数学では、`x = y` は二つの対象が等しいという命題です。型理論では命題を型で表すので、等しさも型で表します。`A` の二つの要素 `x` と `y` に対して、`x ≡ y` は「`x` と `y` が等しい」という命題に対応する型であり、その要素が等しさの証明です。 立方型理論では、この等しさの証明を `x` から `y` への**パス**と呼び、`x ≡ y` をパス型と呼びます。したがって、パスは等しさとは別に置かれた関係ではありません。パスが本書で使う等しさの証明であり、パス型が本書における等しさの表現です。パスには始点と終点があるため、向きを逆にしたり、端と端をつないだりできます。以下の基本操作はこの構造から生まれます。 - `refl` は要素からそれ自身へのパスであり、等しさの反射性を与えます。 - `sym` はパスの向きを逆にします。`x` から `y` へのパスは、これによって `y` から `x` へのパスになります。 - `_∙_` は端点の一致するパスを合成します。`x` から `y` へ進み、続いて `y` から `z` へ進めば、`x` から `z` へのパスが得られます。 - `cong` は関数が等しさを保つこと、すなわち等しい入力を等しい出力へ送ることを述べます。`cong₂` は対応する二引数版です。 - `funExt` は各点での等しさから関数の等しさを与えます。すべての `x` について `f x ≡ g x` ならば、`f ≡ g` です。 - `transport` は型の間のパスに沿って要素を移します。`subst` は `x ≡ y` に沿って、`x` に依存するデータを `y` に依存するデータへ移します。 例えば関数 `f : A → B` があるとき、`cong` の働きは次のようにまとめられます。
`cong f : x ≡ y → f x ≡ f y`
これは関数 `f` が等しさのパスに作用し、入力の間の等しさを出力の間の等しさへ移すことを表します。 パス自身も型の要素なので、二つのパスがさらに等しいかを考えられます。等しさの構造はこのように高い層へ続きます。二つの要素が等しいかだけでなく、その等しさの証明どうしが等しいかも問えるのです。次節では、このような等しさの構造を型が何層まで保つかを測る階層的な分類を導入します。 Cubical Agda のパス型について詳しくは、[Agda 2.8.0 マニュアルの Cubical の章](https://agda.readthedocs.io/en/v2.8.0/language/cubical.html)を参照してください。本節では、後の構成を理解するために必要な基本的性質だけを使います。 ```agda open import Cubical.Foundations.Prelude public using ( _≡_; refl; sym; _∙_; cong; cong₂; transport; subst; funExt ) ``` ## ホモトピーレベル パス自身も型の要素なので、パスどうしの間にさらにパスを作れます。ホモトピーレベルは、このような等しさの証明に区別できる構造がどれだけ残るかによって型を分類します。型の大きさを測るものではありません。大きさを扱うのは宇宙レベルであり、ホモトピーレベルが扱うのは要素とその等しさの証明をどこまで区別できるかです。 - **`isContr A`：`A` は可縮である。** これは `A` の中に中心を一つ選び、すべての `x : A` に対して中心から `x` へのパスを与えることを要求します。したがって `A` には要素が存在し、すべての要素が選ばれた中心と等しいので、等しさによって要素を区別できません。本書では `isContr` が持つこのデータを**一意存在**と読みます。中心が存在を与え、すべての要素へのパスが一意性を与えます。 - **`isProp A`：`A` は命題である。** これは `A` の任意の二要素が等しいことを要求します。中心を選ぶ必要はなく、`A` に要素が存在することさえ要求しません。`A` の証明が存在するなら、それらの間に区別が残らないことだけを述べます。したがって命題には証明がないことも、証明があることもありますが、互いに区別できる二つの証明はあり得ません。 - **`isSet A`：`A` は h-集合である。** 接頭辞はホストレベルの概念であることを示します。h-集合とは `isSet` を満たす型であり、モデル化される集合論の集合ではありません。これは `A` の任意の二要素が等しいことを要求するのではなく、任意の二要素の間のパス型が命題であることを要求します。`A` の要素は互いに異なっていてよく、その一部を結ぶパスが存在してもかまいません。しかし始点と終点を同じものに固定すれば、その間の任意の二つのパスは等しくなります。要素の間には区別が残り得ますが、等しさの証明の間には、それ以上区別できる構造が残りません。 - **`isProp→isSet`：すべての命題は h-集合である。** `A` が `isProp` を満たせば、`isSet` も満たします。これはホモトピーレベルを上向きに移す操作と見なせます。`A` を変えず、「任意の二要素が等しい」という強い条件から「任意の二つの等しさのパスが等しい」という弱い条件を導きます。この点は `Lift` による宇宙レベルの移動と似ています。どちらも同じ数学的対象を、より高いレベルの要件のもとで扱えるようにするからです。ただし、作用する軸は異なります。`Lift` は型を提示する宇宙を変え、元の型と同値なレコードのコピーを作ります。`isProp→isSet` は型もその宇宙も変えず、一つの等しさの性質から別の性質を導くだけです。 ```agda open import Cubical.Foundations.Prelude public using ( isProp; isSet; isContr; isProp→isSet ) ``` ## 命題の宇宙 立方型理論では、命題とは `isProp` を満たす型です。この条件により、その型の任意の二つの元は等しくなります。したがって、証明どうしを区別せず、証明が存在するかどうかという論理的な情報だけが残ります。型の元を構成すれば対応する命題が成り立つことが示され、元をまだ構成できなければ、その命題の証明はまだ得られていません。 命題を、それが命題であるという事実と一緒に収めるため、Cubical ライブラリでは `hProp ℓ` を使います。これは宇宙レベル `ℓ` にあるすべての命題の型です。言い換えれば、`hProp ℓ` はそのレベルの**命題の宇宙**です。`P : hProp ℓ` は二つの成分を含みます。 - 第一成分は命題の基礎型、すなわち命題を表す型であり、命題の記述そのものです。 - 第二成分は、その型が確かに `isProp` を満たすという証明書です。 したがって、`P : hProp ℓ` は命題を表しますが、その命題がすでに証明されているとは主張しません。`P` が持つ証明書は、第一成分が命題であることだけを示し、第一成分に元が存在するとは主張しません。 命題の宇宙について、後の章で繰り返し使う基本性質が二つあります。 - `isSetHProp` は `hProp ℓ` 自身が h-集合であることを示します。異なる命題は区別できますが、命題間の等しさの証明には、区別できる高次の構造が残りません。 - `isPropΠ` は、命題が Π 型に対して閉じていることを示します。すべての `B x` が命題なら、`(x : A) → B x` も命題です。したがって、命題の族を全称量化して得られる結果も命題です。 ```agda open import Cubical.Foundations.HLevels public using ( hProp; isSetHProp; isPropΠ ) ``` 射影 `⟨_⟩` は命題の記述を取り出します。`P : hProp ℓ` に対して、`⟨ P ⟩` はその第一成分です。`P` が表す命題を証明するには、`⟨ P ⟩` の元を構成しなければなりません。命題性の証明書は第二成分 `P .snd` に残ります。 `P` は命題の記述とその命題性の証明書を一つの対象にまとめるため、全体を関数の引数や返り値として渡したり、レコードのフィールドに格納したりできます。命題を述べたり証明したりするときは、`⟨ P ⟩` を通して対応する型を取り出します。 ```agda open import Cubical.Foundations.Structure public using ( ⟨_⟩ ) ``` ## 論理演算 命題の宇宙は通常の論理演算について閉じています。二つの論理定数は真と偽です。真 `⊤` は常に要素をもつ命題であり、ライブラリはこれを任意の宇宙レベルで使える命題として与えます。 ```agda open import Cubical.Functions.Logic public using ( ⊤ ) ``` 偽命題は、不可能性を表す型から作られます。空型 `⊥*` には要素も構成子もありません。それでも論証のある分岐で `x : ⊥*` が得られたなら、その分岐の仮定は成立しえず、`x` を任意の型へ消去できます。
⊥* → A
この原理は、実際のデータから `A` の要素を計算するものではありません。処理すべき構成子の場合が一つもないことを述べています。`isProp⊥*` が空型の命題性を示せる理由も同じで、等しさを証明すべき二要素が存在しません。 ```agda open import Cubical.Data.Empty public using ( ⊥*; isProp⊥* ) ``` 空型と偽命題は、同じ不可能性を異なる構造のレベルで表します。空型は `⊥` の基礎型です。`⊥*` とその命題性の証明 `isProp⊥*` を対にすれば、必要な宇宙レベルの偽命題としてまとめられます。 ```agda ⊥ : ∀ {ℓ} → hProp ℓ ⊥ = ⊥* , isProp⊥* ``` 命題 `P` と `Q` に対して、`P ⊓ Q` はその連言を表します。その証明は `P` と `Q` の証明をともに含み、宇宙レベルは二つの入力レベルの最大値になります。 ```agda open import Cubical.Functions.Logic public using ( _⊓_ ) ``` `P ⊔ Q` は選言を表します。直和型はどちら側から証明が得られたかを記憶するため、ライブラリはそれを**命題的切り詰め**、少なくとも一方が成り立つという情報だけを残します。 ```agda open import Cubical.Functions.Logic public using ( _⊔_ ) ``` `P ⇒ Q` は含意を表します。その証明は `P` の任意の証明を `Q` の証明へ送る関数です。`Q` が命題なので、この関数型も命題になります。 ```agda open import Cubical.Functions.Logic public using ( _⇒_ ) ``` `¬ P` は否定を表し、`P` の証明から偽命題 `⊥` が導かれることを述べます。したがって、その意味は含意と偽から成ります。一般の二項含意とは異なり、否定は `P` と同じ宇宙レベルにあります。 ```agda open import Cubical.Functions.Logic public using ( ¬_ ) ``` 命題族 `P : A → hProp ℓ'` に対して、`∀[ x ∶ A ] P x` は全称量化を表します。その証明は各 `x : A` に `P x` の証明を与えます。型を `∶` の後に書くことで、量化の論域が式に現れます。 ```agda open import Cubical.Functions.Logic public using ( ∀[]-syntax; ∀[∶]-syntax ) ``` `∃[ x ] P x` は存在量化を表します。依存対は証人 `x : A` と `P x` の証明をともに保持しますが、命題的切り詰めによって、どの証人が選ばれたかを忘れ、証人が存在することだけを残します。 ```agda open import Cubical.Functions.Logic public using ( ∃[]-syntax; ∃[∶]-syntax ) ``` 次節では、対象に応じて変化する命題を考えます。 ## クラスと所属関係 ここでいう**クラス**は集合論における class であり、型理論における type ではありません。本書では以後、前者を**クラス**、後者を**型**と呼び分けます。形式化の中で両者は密接に関係しますが、同じ概念ではありません。型はどの項がその要素になれるかを定め、クラスは、すでに与えられた対象の中から、ある性質を満たすものを選び出します。 クラスが考察する対象の範囲を、そのクラスの**論域**と呼びます。`A` と書くとき、論域は型 `A` であり、その要素が現在分類されるすべての対象です。`A` を論域と呼ぶことは、変数 `x : A` がこれらの対象を動くということだけを表し、`A` に所属関係や演算などの構造がすでに備わっていることを意味しません。後に集合論のモデルを構成するとき、`A` に集合論的な所属関係を加えます。そのとき `A` はモデルの台にもなり、その要素がモデル内の集合の役割を果たします。 論域 `A` 上のクラスは関数で表されます。
M : A → hProp ℓ
各 `x : A` に対して、命題 `M x` は「`x` がクラス `M` の定める性質を持つ」ことを表します。したがって `M` は、`x` をどこかに集められた別の対象へ送るのではありません。各 `x` に命題を割り当て、その命題を満たす対象が、まさにそのクラスに属する対象です。 これにより、集合をまだ導入していない段階でクラスを論じられる理由も分かります。ここでのクラスはメタ理論で定義される述語であり、必要なのは論域と命題の宇宙だけです。対象理論で集合がすでに定義されていることを前提とせず、クラス自身が集合であるとも主張しません。後にこの論域へ集合論の構造を加えれば、このようなクラスを使って、モデル内である性質を満たす集合を記述できます。 クラスへの所属を `x ∈ᶜ M` と書き、「`x` はクラス `M` に属する」と読みます。その意味は、`M` が `x` に割り当てる命題です。
x ∈ᶜ M := ⟨ M x ⟩
したがって `x ∈ᶜ M` を証明することは、命題 `⟨ M x ⟩` の証明を構成することです。上付きの `ᶜ` は、ここでクラスへの所属を使っていることを示します。これはホストレベルの述語を、後に集合論のモデルで解釈する集合間の所属関係から区別します。前者は対象がある性質を満たすかを述べ、後者は対象言語の関係です。 ```agda open import Cubical.Foundations.Powerset public using () renaming ( _∈_ to _∈ᶜ_ ) ``` ## 自然数 自然数 `ℕ` は、二つの構成子から生成される帰納型です。構成子 `zero` は `ℕ` の要素であり、構成子 `suc` は任意の `n : ℕ` から別の要素 `suc n : ℕ` を作ります。構成規則は次のとおりです。 $$\frac{}{\mathsf{zero}:\mathbb{N}}\qquad\frac{n:\mathbb{N}}{\mathsf{suc}\,n:\mathbb{N}}.$$ `ℕ` のすべての要素は、この二つの構成子から生成されます。対応する帰納原理は、`zero` の場合と、`n` から `suc n` へ進む帰納段階からなります。 したがって、`ℕ` からの関数を再帰的に定義するには、`zero` での値と、すでに得られた `n` での値から `suc n` での値を作る方法を与えれば十分です。 ```agda open import Cubical.Data.Nat public using ( ℕ; zero; suc ) ``` ## 有限添字 `Fin` は自然数を添字とする型の族です。`Fin zero` には構成子がありません。添字が `suc n` のとき、構成子 `zero` が一つの要素を直接与え、`suc` は `Fin n` の各要素を `Fin (suc n)` の要素へ送ります。構成規則は次のとおりです。 $$\frac{}{\mathsf{zero}:\operatorname{Fin}(\operatorname{suc}\,n)}\qquad\frac{i:\operatorname{Fin}(n)}{\mathsf{suc}\,i:\operatorname{Fin}(\operatorname{suc}\,n)}$$ したがって `Fin n` はちょうど `n` 個の要素をもちます。添字が `zero` のとき要素はなく、`n` から `suc n` へ移ると、一つの新しい要素と、`Fin n` の各要素から `suc` で作られる要素が得られます。 ```agda open import Cubical.Data.FinData public using ( Fin; zero; suc ) ``` ## ベクトル ベクトル `Vec A n` は `A` の元からなるリストで、その長さが型の一部になっています。その二つの構成子は、次の推論式で表せます。 $$\frac{}{[]:\operatorname{Vec}(A,0)}\qquad\frac{a:A\quad v:\operatorname{Vec}(A,n)}{a∷v:\operatorname{Vec}(A,\operatorname{suc}\,n)}$$ 構成子 `[]` は `Vec A zero` の要素を与えます。`a : A` と `v : Vec A n` が与えられると、構成子 `_∷_` は `a ∷ v : Vec A (suc n)` を与えます。このように自然数の添字はベクトルとともに定まります。関数 `lookup` の型は `Fin n → Vec A n → A` であり、二つの引数は同じ添字 `n` を共有します。 ```agda open import Cubical.Data.Vec public using ( Vec; []; _∷_; lookup ) ``` ## 恒等関数 恒等関数 `id` は要素を受け取り、その要素を変更せずにそのまま返します。型は次のとおりです。 ```agda id : ∀ {ℓ} {A : Type ℓ} → A → A ``` ここで `ℓ` は任意の宇宙レベル、`A` はそのレベルの任意の型です。型シグネチャは `A` にほかの条件を課していないため、`id` は任意の型の要素に適用できます。 ```agda id x = x ``` 入力 `x` はすでに結果の型 `A` をもつので、そのまま結果として返せます。この定義は `x` を変更せず、`x` がどのように構成されたかを調べる必要もありません。 ## まとめ 本章では、本書で用いるホストレベルの基礎語彙を導入しました。 - `Type` と `Level` は型宇宙とそのレベルを記述します。 - Π 型は依存関数を、Σ 型は依存対を表します。 - レコード型は、名前付きフィールドと構成子によって、入れ子になった Σ 型を平坦に表します。 - `Lift` は型を宇宙レベル間で移します。 - パス型は等しさを表し、ホモトピーレベルは型に残る等しさの構造を記述します。 - `hProp` は命題の宇宙であり、`⟨_⟩` は命題の記述を取り出します。 - 真と偽、連言と選言、含意と否定、全称量化と存在量化が、命題の宇宙における論理演算を与えます。 - クラスは命題の宇宙に値をとる述語であり、`_∈ᶜ_` はクラスへの所属を表します。 - `ℕ`、`Fin`、`Vec` は、それぞれ帰納型と、自然数を添字とする二つの型族です。 - `⊥*` は空型であり、`id` は恒等関数です。 これらの概念が、本書で採用する基本的な形式言語を構成します。