この章を読むか、対話型目次と依存グラフで別のルートを選べます。

本書では集合論を対象理論、立方型理論をメタ理論とする。立方型理論の中で集合論のモデルを構成し、その文を解釈して性質を証明する。Agda が構成と証明を検査し、Cubical ライブラリが基礎語彙を提供する。この環境をホストと呼ぶ。したがって、ホストの型や関数はメタ理論に属し、集合論のモデル内部の対象とは異なる。

本章では、その語彙を数学的な意味と使い方から紹介する。記号を一度に覚える必要はない。後の章では Base.Prelude からまとめて導入するので、必要なときにここへ戻り、意味を確かめればよい。

読書案内

まず文章を読み、直後のコードでその正確な形を確かめる。型宣言と定義等式を持つ定義には、終わりに ∎ が自動的に表示される。

対話型目次で学習ルートを選ぶことも、依存グラフで章どうしの前提関係を確かめることもできる。各章の冒頭にある学習ルートには、直接の前提となる章と次に読む候補の章が並ぶ。

印のある名前や式にポインタを重ねると型を確認でき、ポップアップ内の名前も同じように調べられる。

キーワードと構文記号には短い説明と Agda 公式文書へのリンクがあり、用語からは最初の導入箇所へ戻れる。基礎語彙はまず本章の説明へ導く。ライブラリの定義をさらに調べたいときは、表示されている Cubical の open import 文をたどって原文へ進める。

これを手掛かりに、本モジュールに集めた数学的な概念を見ていく。

宇宙レベル

型理論では、型の大きさを区別しなければならない。すべての型を量化する型があれば、それは自分自身を含んでしまう。そこでホストは、各レベル ℓ : Level に一つずつある宇宙 Type ℓ へ型を分類する。代数的には、宇宙レベルは後続演算を備えた最小元付き結び半束をなす。ℓ-zero が最小元、ℓ-suc が後続演算、ℓ-max が二項の結びである。元の式 ℓ-suc ℓ は、サイトでは簡潔な ℓ-suc ℓ と表示され、ホバーすると元のコードを確認できる。各宇宙はそれ自身も型である。

Type ℓ : Type (ℓ-suc ℓ)

本書が「すべての集合」や「すべての命題」のような全体を扱うとき、主張に付いたレベルが、その全体をどの大きさとして扱うかを記録する。

open import Cubical.Foundations.Prelude public
  using ( Type; Level; ℓ-zero; ℓ-suc; ℓ-max )

恒等関数 id は、どの宇宙レベルでも一様に使える定義の簡単な例である。任意のレベル ℓ と型 A : Type ℓ に対して、A の要素を受け取り、その要素をそのまま返す。

id : ∀ {ℓ} {A : Type ℓ} → A → A

レベルと型は暗黙引数なので、通常は要素だけを与えて使う。その要素はすでに結果の型 A をもつため、定義式は構成のされ方を調べずに、そのまま返す。

id x = x

レベル間の移動

ここで使う Agda の型宇宙は累積的ではない。Type ℓ の要素が自動的に Type (ℓ-suc ℓ) の要素になるわけではない。レベル間で型を移すには、明示的な演算 Lift が必要である。

Lift ℓ A は元の型 A の元を一つ包むレコード型である。a : A を与えると、関数 lift は 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 は型を決まった段数だけ持ち上げるのではなく、現在の二つのレベルにとって十分大きな宇宙へ型を置く。

型は常にこの方法で上へコピーできるが、一般には下へ動かせない。

open import Cubical.Foundations.Prelude public
  using ( Lift; lift; lower )

基本的な型

以下の四つの構成は、本書を通して用いるデータを組織する。これらを使うと、入力に応じて変わる出力を記述し、関連するデータをまとめ、選択肢を区別し、あるいは大きなデータのまとまりの各成分に名前を付けられる。それぞれの正確な名前と形は、以下で順に導入する。

Π 型

本書の後の多くの構成では、各対象に対して、それに依存するデータを与える必要がある。Π 型はこの関係を表す基本形である。

型 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 に依存するため、第一成分を定めて初めて、第二成分がどの型に属すべきかが決まる。

第二成分を、第一成分の性質を示す証明にすることもできる。本書では、後の議論でその性質を使えるよう対象とともに携える証明を証明書と呼ぶ。証明書は通常の Agda の証明であり、この名前は依存対の中で果たす役割を強調している。

B が x に依存しない場合、すべての第二成分は同じ型に属し、依存対は通常の積に特化する。

A × B = Σ[ _ ∶ A ] B

通常の積は互いに独立した二つの元を一緒にするが、Σ 型は、ある a と、対応する型 B a に属するデータを一緒にする。依存対は _,_ で作る。依存対 p に対し、p .fst と p .snd はそれぞれ第一成分と第二成分を取り出す。名前が一文字の場合、ページ上では p .fst と p .snd とコンパクトに表示する。ホバーすると元の Agda の書き方を確認できる。

open import Cubical.Data.Sigma public
  using ( Σ; _×_; _,_; fst; snd )

次のコードブロックで Σ 型の二つの束縛表記を定義する。最初は優先順位の宣言だけを示し、実装の詳細は展開して読める。Σ[ x ∶ A ] B x は第一成分の型を明示し、Σ[ x ] B x はその推論を Agda に任せる。両者は同じ依存対型を作る。

infix 2 Σ[]-syntax Σ[∶]-syntax

Σ[]-syntax : ∀ {ℓ ℓ'} {A : Type ℓ}
  → (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
Σ[]-syntax {A = A} B = Σ A B

Σ[∶]-syntax : ∀ {ℓ ℓ'} {A : Type ℓ}
  → (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
Σ[∶]-syntax = Σ[]-syntax

syntax Σ[∶]-syntax {A = A} (λ x → B) = Σ[ x ∶ A ] B
syntax Σ[]-syntax (λ x → B) = Σ[ x ] B

$$f : \prod_{x:A} B(x)$$

$$\begin{array}{rcl} x_1 : A & \longmapsto & f(x_1) : B(x_1) \\[8pt] x_2 : A & \longmapsto & f(x_2) : B(x_2) \\[4pt] \vdots & & \vdots \end{array}$$

$$(a,b) : \sum_{x:A} B(x)$$

$a : A$ $b : B(a)$ $(a,b)$

Π 型が扱うのは「すべての x に対して、x に依存するデータを与えること」である。Σ 型が扱うのは「一つの x を選び、それに依存するデータと一緒に収めること」である

直和型

直和 A ⊎ B は、二通りの構成法をもつ帰納型である。a : A から inl a : A ⊎ B を構成でき、b : B から inr b : A ⊎ B を構成できる。構成規則は次のとおりである。

$$\frac{a:A}{\operatorname{inl}\,a:A\mathbin{\uplus}B}\qquad\frac{b:B}{\operatorname{inr}\,b:A\mathbin{\uplus}B}$$

ここで inl と inr を構成子と呼ぶ。したがって直和の元は、どちら側が選ばれたかと、その側で与えられた元の両方を記録する。パターンマッチによって、その二つの情報を取り出せる。除去子 ⊎-rec は二つの構成子を別々に扱う。一方の枝は A を、他方の枝は B を受け取り、どちらも同じ目的の型を作らなければならない。

$$\mathsf{\uplus\text{-}rec}:(A\to C)\to(B\to C)\to A\mathbin{\uplus}B\to C$$

$$\mathsf{\uplus\text{-}rec}\;f\;g\;x= \begin{cases} f(a), & x=\operatorname{inl}\,a,\\ g(b), & x=\operatorname{inr}\,b \end{cases}$$

open import Cubical.Data.Sum public
  using ( _⊎_; inl; inr )
  renaming ( rec to ⊎-rec )

レコード型

レコード型は、複数の Σ 型を入れ子にしたものに対する構文糖と考えられる。たとえば、元 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 のレコード型の文書を参照してほしい。

等式とパス

通常の数学では、$x = y$ は二つの対象が等しいという主張である。本書ではこれを x ≡ y と書く。A の二つの要素 x と y に対して、これは両者の等しさの証明を要素とする型である。

= は判断的等しさ (judgmental equality) に用いる。これは型システムが定義と計算の規則に従って二つの式を同じものと認めることであり、id x = x がその例である。定義を与える式では、この = は通常の $\mathrel{:=}$ に相当するが、判断的等しさには計算から得られる等しさも含まれる。これは型システムが下す判断であって、それ自体が証明を与えるべき型なのではない。一方、x ≡ y は型であり、p : x ≡ y はその等しさの証明を与え、通常の数学で証明する $x = y$ に対応する。x と y が判断的に等しければ、以下で紹介する定値パス refl によって x ≡ y を証明できるが、両者の間にパスがあっても、一般には判断的に等しいとは限らない。

立方型理論では、この等しさの証明を x から y へのパスと呼び、x ≡ y をパス型と呼ぶ。したがって、パスは等しさとは別に置かれた関係ではない。パスが本書で使う等しさの証明であり、パス型が本書における等しさの表現である。パスには始点と終点があるため、向きを逆にしたり、端と端をつないだりできる。以下の基本操作はこの構造から生まれる。

$\operatorname{refl}_x$ $x$

$$\begin{gathered}\operatorname{refl}_x : x\equiv x\end{gathered}$$

refl は要素からそれ自身へのパスであり、等しさの反射性を与える。

$x$ $y$ $p$ $y$ $x$ $\operatorname{sym}\,p$ $\Big\downarrow\mathrlap{\;{\scriptstyle\operatorname{sym}}}$

$$\begin{gathered}p:x\equiv y,\quad\operatorname{sym}\,p:y\equiv x\end{gathered}$$

sym はパスの向きを逆にする。x から y へのパスは、これによって y から x へのパスになる。

$x$ $y$ $z$ $p$ $q$ $p\mathbin{\cdot}q$

$$\begin{gathered}p:x\equiv y,\quad q:y\equiv z\\[3pt]p\mathbin{\cdot}q:x\equiv z\end{gathered}$$

_∙_ は端点の一致するパスを合成する。x から y へ進み、続いて y から z へ進めば、x から z へのパスが得られる。

パスの三つの基本操作：反射、反転、合成

cong は関数をパスに作用させる。関数 f : A → B と入力の間のパス p : x ≡ y が与えられると、出力の間のパス cong f p : f x ≡ f y を構成する。したがって、f を固定すると、パスをパスへ送る関数が得られる。

cong f : x ≡ y → f x ≡ f y

ここでは二つの出力は同じ型 B に属する。図では、f が端点 x と y を f x と f y に送り、cong f が端点の間のパスを像の間のパスに送る。cong₂ は二つの入力を持つ関数に対する同様の操作である。

$$f : A\to B,\qquad p:x\equiv y$$

$x:A$ $y:A$ $p$ $f$ $f$ $f(x):B$ $f(y):B$ $\operatorname{cong}\,f\,p$

cong：関数はパスを、その端点の像の間のパスに送る

transport は型の間のパスを、それらの要素を移す関数に変える。同じ宇宙に属する型 A、B とパス p : A ≡ B が与えられると、A から B への関数 transport p を構成する。したがって、p を固定すると、要素を要素へ送る関数が得られる。

transport p : A → B

ここでは型そのものがパスの端点である。図では、transport がこのパスを関数に変え、その関数が要素 a : A を transport p a : B に送る。パス p は型の等しさを与え、transport p は要素を移す操作を行う。

$$p : A\equiv B$$

$$a : A$$

$$\xmapsto{\;\operatorname{transport}\,p\;}$$

$$b : B$$

$$\Big\uparrow\mathrlap{\;{\scriptstyle\operatorname{transport}}}$$

$$A : \operatorname{Type}_{\ell}$$

$p$

$$B : \operatorname{Type}_{\ell}$$

$$b := \operatorname{transport}\,p\,a$$

transport：型の間のパスから、要素を移す関数を得る

subst は型族の入力の間のパスを、対応する型の間の関数に変える。型族 B : A → Type ℓ とパス p : x ≡ y が与えられると、B x から B y への関数 subst B p を構成する。したがって、B と p を固定すると、要素を要素へ送る関数が得られる。

subst B p : B x → B y

ここではパスが入力 x と y を結び、移される要素は B x と B y に属する。図では、subst B p が u : B x を subst B p u : B y に送る。subst2 は二つの入力を持つ型族に対する同様の操作である。各入力のパスを与えると、新しい入力の組に対応する型へデータを移す。

$$B : A \to \operatorname{Type}_{\ell}, \qquad p : x \equiv y$$

$$u : B(x)$$

$$\xmapsto{\;\operatorname{subst}\,B\,p\;}$$

$$v : B(y)$$

$$x : A$$

$p$

$$y : A$$

$$v := \operatorname{subst}\,B\,p\,u$$

subst：添字の間のパスから、対応する型の間の関数を得る

これら三つの操作の関係を次の図で表す。各枠は型を表し、その型を枠の上部に記す。枠内の点はその要素を表し、枠の間の矢印は型の間の関数を表す。x ≡ y から B x → B y へは、直接 subst B を適用することも、まず cong B、次に transport を適用することもできる。

$$B : A \to \operatorname{Type}_{\ell}, \qquad x,y:A$$

$x\equiv y$ $B(x)\equiv B(y)$ $B(x)\to B(y)$ $p$ $\operatorname{cong}\,B\,p$ $\operatorname{cong}\,B$ $\operatorname{subst}\,B$ $\operatorname{transport}$ $\operatorname{subst}\,B\,p$ $\operatorname{transport}\,(\operatorname{cong}\,B\,p)$

各入力 p に対し、二つの経路から得られる関数は同じ型 B x → B y に属する。青い線は、これらの関数の間にパスが存在することを表す。ここでは証明を省略する

funExt は各点での等しさから関数の等しさを与える。すべての x について f x ≡ g x ならば、f ≡ g である。

$$f,g : A\to B$$

$$h : \prod_{x:A}\bigl(f(x)\equiv g(x)\bigr)$$

$f(x_1)$

$h(x_1)$

$g(x_1)$ $f(x_2)$

$h(x_2)$

$g(x_2)$ $\vdots$

$\vdots$

$\xmapsto{\operatorname{funExt}}$ $\Big\downarrow\mathrlap{\;{\scriptstyle\operatorname{funExt}}}$

$f$ $g$ $\operatorname{funExt}\,h$

$$\operatorname{funExt}\,h : f\equiv g$$

funExt：すべての入力におけるパスから、関数の間のパスを得る

パス自身も型の要素なので、二つのパスがさらに等しいかを考えられる。等しさの構造はこのように高い層へ続く。二つの要素が等しいかだけでなく、その等しさの証明どうしが等しいかも問えるのである。次節では、このような等しさの構造を型が何層まで保つかを測る階層的な分類を導入する。

Cubical Agda のパス型について詳しくは、Agda 2.8.0 マニュアルの Cubical の章を参照してほしい。本節では、後の構成を理解するために必要な基本的性質だけを使う。

open import Cubical.Foundations.Prelude public
  using ( _≡_; refl; sym; _∙_; cong; cong₂; transport; subst; subst2; funExt )

ホモトピーレベル

パス自身も型の要素なので、パスどうしの間にさらにパスを作れる。ホモトピーレベルは、このような等しさの証明に区別できる構造がどれだけ残るかによって型を分類する。型の大きさを測るものではない。大きさを扱うのは宇宙レベルであり、ホモトピーレベルが扱うのは要素とその等しさの証明をどこまで区別できるかである。

isContr A：A は可縮である。 これは A の中に中心を一つ選び、すべての x : A に対して中心から x へのパスを与えることを要求する。したがって A には要素が存在し、すべての要素が選ばれた中心と等しいので、等しさによって要素を区別できない。本書では isContr が持つこのデータを一意存在と読む。中心が存在を与え、すべての要素へのパスが一意性を与える。
isProp A：A は命題である。 これは A の任意の二要素が等しいことを要求する。中心を選ぶ必要はなく、A に要素が存在することさえ要求しない。A の証明が存在するなら、それらの間に区別が残らないことだけを述べる。したがって命題には証明がないことも、証明があることもあるが、互いに区別できる二つの証明はあり得ない。
isSet A：A は h-集合である。 通常、h は homotopy (ホモトピー) の頭文字である。本書では host (ホスト) を連想するための手掛かりともなる。h-集合はホストにおいて isSet を満たす型であり、後に扱う集合論の集合とは異なるからである。これは A の任意の二要素が等しいことを要求するのではなく、任意の二要素の間のパス型が命題であることを要求する。A の要素は互いに異なっていてよく、その一部を結ぶパスが存在してもかまわない。しかし始点と終点を同じものに固定すれば、その間の任意の二つのパスは等しくなる。要素の間には区別が残り得るが、等しさの証明の間には、それ以上区別できる構造が残らない。

$$\operatorname{isContr}(A)$$

$$c,x,y : A$$

$c$ $x$ $y$ $h(x)$ $h(y)$

$$c : A,\quad h : \prod_{x:A}(c\equiv x)$$

選ばれた中心を持ち、すべての元が中心とパスで結ばれる型。

$\Longrightarrow$ $\Downarrow$

$$\operatorname{isProp}(A)$$

$$x,y : A$$

$x$ $y$ $h(x,y)$

$$h : \prod_{x,y:A}(x\equiv y)$$

したがって命題には証明がないことも、証明があることもあるが、互いに区別できる二つの証明はあり得ない。

$\Longrightarrow$ $\Downarrow$

$$\operatorname{isSet}(A)$$

$$x,y : A,\quad p,q : x\equiv y$$

$x$ $y$ $p$ $q$ $p\equiv q$

$$h : \prod_{x,y:A}\operatorname{isProp}(x\equiv y)$$

等しさの型がすべて命題である型。元は互いに異なりうるが、同じ二元が等しいことの証明は互いに一致する。

中心の選択、要素の等しさ、パスの等しさ：これらの条件は順に弱くなる

isProp→isSet：すべての命題は h-集合である。 A が isProp を満たせば、isSet も満たす。これはホモトピーレベルを上向きに移す操作と見なせる。A を変えず、「任意の二要素が等しい」という強い条件から「任意の二つの等しさのパスが等しい」という弱い条件を導く。この点は Lift による宇宙レベルの移動と似ている。どちらも同じ数学的対象を、より高いレベルの要件のもとで扱えるようにするからである。ただし、作用する軸は異なる。

open import Cubical.Foundations.Prelude public
  using ( isProp; isSet; isContr; isProp→isSet )

宇宙レベル

$$\operatorname{Lift}\,\ell_2\,A : \operatorname{Type}_{\ell\text{-max}(\ell_1,\ell_2)}$$

$$\Big\uparrow\mathrlap{\;{\scriptstyle\operatorname{Lift}\,\ell_2}}$$

$$A : \operatorname{Type}_{\ell_1}$$

ホモトピーレベル

$$\operatorname{isContr}(A)$$

$$\Longrightarrow$$

$$\operatorname{isProp}(A)$$

$$\Longrightarrow$$

$$\operatorname{isSet}(A)$$

Lift は型を提示する宇宙を変え、同じデータをもつレコードのコピーを作る。isProp→isSet は型もその宇宙も変えず、一つの等しさの性質から別の性質を導くだけである

図の二つの軸は独立している。型を別の宇宙へ持ち上げても、そのホモトピーレベルは保たれる。関数 isOfHLevelLift は対応する証明を Lift A へ移す。最初の引数はホモトピーレベルを指定し、0 は可縮性、1 は命題性、2 は h-集合性を表す。したがって h : isProp A があれば isOfHLevelLift 1 h は isProp (Lift A) を証明し、h : isSet A があれば isOfHLevelLift 2 h は isSet (Lift A) を証明する。この数が指定するのは等しさの性質であり、Lift の移動先の宇宙ではない。

open import Cubical.Foundations.HLevels public using ( isOfHLevelLift )

型同値

パスは共通の型の要素を比較する。型そのものを、異なる宇宙に属する場合も含めて比較するには、A ≃ B を使う。これは、写像が両側の要素とパスの情報を保つことを表す。両方向の関数が存在するだけでは足りず、往復によって出発時の情報を復元できなければならない。その条件を以下で正確に述べる。

型 A と B について、A ≃ B は依存対である。その第一成分は写像 f : A → B、第二成分は f に依存する証明書である。この証明書を読むために、まず次の定義を見る。

固定した b : B 上の f のファイバーは、次の依存対型である。

Σ[ a ∶ A ] (f a ≡ b)

ファイバーの要素は二つの成分を持つ。第一成分は原像の候補 a : A、第二成分はその候補が実際に b へ写ることを示すパス f a ≡ b である。ファイバーが空なら b に原像はない。ファイバーにパスで同一視できない要素があれば、b から A へ戻る方法に本質的な違いが残っている。

open import Cubical.Foundations.Equiv public using ( _≃_ )

以下のアニメーションでは各ファイバーの可縮性を仮定する。すなわち、中心と、ファイバーの各依存対をその中心へ結ぶパスの族が存在する。

$$F_b=\sum_{a:A}\bigl(f(a)\equiv b\bigr)$$

$A$ $B$ $f$ $a_{00}$ $a_{01}$ $a_{02}$ $a_{03}$ $b_0$ $a_{10}$ $a_{11}$ $a_{12}$ $a_{13}$ $b_1$ $a_{20}$ $a_{21}$ $a_{22}$ $a_{23}$ $b_2$

点滅するファイバーをクリックすると収縮し、もう一度クリックすると広がる。各毛束のパスは $f(a_i)$ と $b_i$ を結ぶ一本のパス $p_i$ に合流し、原像の候補は $a_i$ に合流する。重なりはパスによる等しさを表す。各ファイバーが可縮であることが、$f$ が同値となる条件である

この型同値は同型と区別する必要がある。同型は写像 f : A → B、g : B → A と二つの往復則を明示的に与える。すなわち、各 a : A に対するパス g (f a) ≡ a と、各 b : B に対するパス f (g b) ≡ b である。構成子の引数は iso f g s r の順であり、s : (b : B) → f (g b) ≡ b、r : (a : A) → g (f a) ≡ a である。両者の関係は次のとおりである。iso はこれらのデータを Iso A B にまとめ、isoToEquiv は得られた同型を A ≃ B へ変換する。写像を明示する同型は具体例の構成に便利であり、Cubical ライブラリは型の構造を運ぶ共通のインターフェースとして型同値を用いる。

open import Cubical.Foundations.Isomorphism public using ( Iso; iso; isoToEquiv )

e : A ≃ B があれば、この同値を両方向に使える。関数 equivFun e : A → B はその第一成分であり、invEq e : B → A は可縮性の証明を用いて原像を復元する。両方向の合成は、パスの意味で入力に戻る。特に A と B が命題なら、これらの関数は一方の証明を他方の証明へ変換する。

open import Cubical.Foundations.Equiv public using ( equivFun; invEq )

型同値は要素間のパスも保つ。f = equivFun e と書くと、x y : A に対して congEquiv e は次の型同値を与える。

(x ≡ y) ≃ (f x ≡ f y)

その順写像は cong f、すなわち関数をパスに作用させる操作である。逆写像 invEq (congEquiv e) は像の間のパスから元の要素間のパスを復元する。したがって型同値ではパスを送ることも復元することもできるが、一般の関数に対する cong は順方向の操作だけを与える。

open import Cubical.Foundations.Equiv.Properties public using ( congEquiv )

最後に、型同値は Lift と同様にホモトピーレベルを保つ。h : isProp A なら isOfHLevelRespectEquiv 1 e h は isProp B を証明し、h : isSet A なら isOfHLevelRespectEquiv 2 e h は isSet B を証明する。引数 0 は同じく可縮性を移す。ここでは証明が同値に沿って A から B へ移り、両者の宇宙が異なってもよい。

open import Cubical.Foundations.HLevels public using ( isOfHLevelRespectEquiv )

したがって Iso で扱いやすい提示を構成し、isoToEquiv で変換すれば、得られた同値を使って要素、パス、ホモトピーレベルの証明を移せる。

命題

以下の構成では、主張を表す型を一般のデータ型から取り分ける。まず命題性を特徴づけ、次に命題の宇宙を作り、切り詰めによって存在情報を制御し、論理演算で命題を組み立て、最後に命題値の述語でクラスを記述する。

命題性

立方型理論では、命題とは isProp を満たす型である。この条件により、その型の任意の二つの元は等しくなる。したがって、証明どうしを区別せず、証明が存在するかどうかという論理的な情報だけが残る。型の元を構成すれば対応する命題が成り立つことが示され、元をまだ構成できなければ、その命題の証明はまだ得られていない。

後の章では、命題性に関する四つの閉性を繰り返し使う。

isPropΠ は、命題が Π 型に対して閉じていることを示す。すべての B x が命題なら、(x : A) → B x も命題である。したがって、命題の族を全称量化して得られる結果も命題である。
isProp→ は isPropΠ の依存しない特別な場合である。終域 B が命題なら、定義域 A が命題であることを仮定しなくても、関数型 A → B は命題になる。
isPropΣ は依存対を扱う。A と各 B x が命題なら、Σ[ x ∶ A ] B x も命題になる。
isProp× は isPropΣ の依存しない特別な場合である。A と B が命題なら、それぞれの証明を組にした型も命題である。そのような二つの組は成分ごとに等しくなる。

open import Cubical.Foundations.HLevels public
  using ( isPropΠ; isProp→; isPropΣ; isProp× )

命題性は、証明を携える依存対の等しさも制御する。可能な第二成分がすべて命題なら、Σ≡Prop により、二つの依存対は第一成分が等しいだけで全体として等しくなる。証明書にはそれ以上区別できる選択がないため、基礎となる対象の等しさが梱包全体の等しさを決定する。

open import Cubical.Data.Sigma public using ( Σ≡Prop )

命題の宇宙

命題を、それが命題であるという事実と一緒に収めるため、Cubical ライブラリでは hProp ℓ を使う。これは宇宙レベル ℓ にあるすべての命題の型である。言い換えれば、hProp ℓ はそのレベルの命題の宇宙である。P : hProp ℓ は二つの成分を含む。

第一成分は命題の基礎型、すなわち命題を表す型であり、命題の記述そのものである。
第二成分は、その型が確かに isProp を満たすという証明書である。

したがって、P : hProp ℓ は命題を表すが、その命題がすでに証明されているとは主張しない。P が持つ証明書は、第一成分が命題であることだけを示し、第一成分に元が存在するとは主張しない。

命題の宇宙自身は h-集合である。isSetHProp は異なる命題を区別できるままにしつつ、命題間の等しさの証明には区別できる高次の構造が残らないことを保証する。

open import Cubical.Foundations.HLevels public
  using ( hProp; isSetHProp )

射影 ⟨_⟩ は命題の記述を取り出す。P : hProp ℓ に対して、⟨ P ⟩ はその第一成分である。P が表す命題を証明するには、⟨ P ⟩ の元を構成しなければならない。記法 ⟨ P ⟩isProp は、この基礎型が isProp を満たすことの証明を取り出す。

P は命題の記述とその命題性の証明書を一つの対象にまとめるため、全体を関数の引数や返り値として渡したり、レコードのフィールドに格納したりできる。命題を述べたり証明したりするときは、⟨ P ⟩ を通して対応する型を取り出す。下図では、基礎型が空である例と元をもつ例を示す。どちらも命題性の証明書をもつ。

open import Cubical.Foundations.Structure public
  using ( ⟨_⟩ )

⟨_⟩isProp : ∀ {ℓ} (P : hProp ℓ) → isProp ⟨ P ⟩
⟨ P ⟩isProp = P .snd

$$P=(\langle P\rangle,h_P):\operatorname{hProp}\,\ell$$

$$\langle P\rangle:\operatorname{Type}_{\ell}$$

(元がない)

$$h_P:\operatorname{isProp}\langle P\rangle$$

$$Q=(\langle Q\rangle,h_Q):\operatorname{hProp}\,\ell$$

$$\langle Q\rangle:\operatorname{Type}_{\ell}$$

$p$ $q$ $h_Q\,p\,q$

$$h_Q:\operatorname{isProp}\langle Q\rangle$$

証明書 $h_Q$ は任意の二つの証明にパスを与える。右図の曲線は、その $p$、$q$ における値 $h_Q\,p\,q$ を表す

命題的切り詰め

型は、命題が保持すべき情報より多くの情報をもつことがある。命題的切り詰め ∥ A ∥₁ は、A に要素があることを記録しつつ、それがどの要素かを意図的に忘れる。これは高階帰納型、略して HIT である。その生成子には点だけでなく、点の間のパスも含まれる。点構成子 ∣_∣₁ は各 a : A を ∣ a ∣₁ : ∥ A ∥₁ へ送り、パス構成子 squash₁ は切り詰めの任意の二要素を同一視する。その定義規則は次のとおりである。

$$\frac{a:A}{|a|_1:\|A\|_1}\qquad\frac{x,y:\|A\|_1}{\mathsf{squash}_1(x,y):x=y}$$

したがって A が区別可能なデータをもっていても、∥ A ∥₁ は常に命題である。

本書で A の要素の単なる存在と言うときは、A の特定の要素ではなく、∥ A ∥₁ の要素が与えられることを意味する。同様に、P x を満たす x : A が単に存在するとは、∥ Σ[ x ∶ A ] P x ∥₁ に要素があることを意味する。P x が命題であるとき、この切り詰められた型が、後で導入する論理的な存在量化 ∃[ x ∶ A ] P x の基礎となる型である。

$A$ $a$ $b$ $\lvert{-}\rvert_1$ $\|A\|_1$ $\lvert a\rvert_1$ $\lvert b\rvert_1$ $\operatorname{squash}_1\,\lvert a\rvert_1\,\lvert b\rvert_1$

a b : A が与えられると、切り詰めでの像は図のパスで結ばれる。二つの像が判断的に等しいとは限らず、squash₁ がその等しさの証明を与える

切り詰められた値の使い方には、二つの標準的な方法がある。再帰子 rec₁ が代表を局所的に取り出せるのは、行き先が命題であるとすでに証明されている場合だけである。この制限により、隠された選択が通常のデータとして外へ出ることを防ぐ。

rec₁ : isProp P → (A → P) → ∥ A ∥₁ → P

$$h : \operatorname{isProp}(P), \qquad f : A \to P$$

$A$ $\|A\|_1$ $P$ $|{-}|_1$ $f$ $\operatorname{rec}_1\,h\,f$

$$\operatorname{rec}_1\,h\,f\,(|a|_1) = f(a) \qquad (a : A)$$

P が命題ならば、rec₁ によって f : A → P は切り詰めを経由して分解される。代表 a に対し、どちらの経路も f a を与える

写像 map₁ は切り詰めの内側で関数 A → B を適用し、再び切り詰められた値を返す。

map₁ : (A → B) → ∥ A ∥₁ → ∥ B ∥₁

import Cubical.HITs.PropositionalTruncation as PT
open PT public
  using ( ∥_∥₁; ∣_∣₁; squash₁ )
  renaming ( rec to rec₁; map to map₁ )

論理演算

命題の宇宙は通常の論理演算について閉じている。以下では、すでに導入した型の構成法から各演算を組み立て、どの場合に命題的切り詰めが必要かを説明する。

真

単元型は自明な証拠を表す。Type₀ にあるレベル 0 の形を ⊤₀、任意の宇宙レベル ℓ へ持ち上げた形を ⊤* {ℓ} と書き、それぞれの唯一の要素を tt と tt* と書く。単元型の任意の二要素は等しいため、isProp⊤* は ⊤* が命題であることを証明する。

open import Cubical.Data.Unit public
  using ( tt; tt* )
  renaming ( Unit to ⊤₀; Unit* to ⊤*; isPropUnit* to isProp⊤* )

真の命題 ⊤ と単元型は、同じ自明な真理を異なる構造のレベルで表す。単元型は ⊤ の基礎型である。⊤* とその命題性の証明 isProp⊤* を対にすれば、必要な宇宙レベルの真の命題としてまとめられる。したがって真は命題の宇宙に属する。基礎となる単元型には要素があり、そのすべての要素が等しいからである。

open import Cubical.Functions.Logic public using ( ⊤ )

偽

空型は不可能性を表す。Type₀ にあるレベル 0 の形を ⊥₀、任意の宇宙レベル ℓ へ持ち上げた形を ⊥* {ℓ} と書く。どちらにも要素も構成子もない。それでも論証のある分岐で x : ⊥* が得られたなら、その分岐の仮定は成立しえず、x を任意の型へ消去できる。

⊥₀-rec : ⊥₀ → A

⊥*-rec : ⊥* → A

消去子 ⊥₀-rec と ⊥*-rec は、実際のデータから A の要素を計算するものではない。処理すべき構成子の場合が一つもないことを述べている。isProp⊥ は ⊥₀ の、isProp⊥* は ⊥* の命題性を示す。理由は同じで、等しさを証明すべき二要素が存在しない。

open import Cubical.Data.Empty public
  using ( ⊥*; isProp⊥* )
  renaming ( ⊥ to ⊥₀; rec to ⊥₀-rec; rec* to ⊥*-rec )

open import Cubical.Data.Empty.Properties public using ( isProp⊥ )

偽の命題 ⊥ と空型は、同じ不可能性を異なる構造のレベルで表す。空型は ⊥ の基礎型である。⊥* とその命題性の証明 isProp⊥* を対にすれば、必要な宇宙レベルの偽の命題としてまとめられる。したがって偽は命題の宇宙に属する。基礎となる空型には要素がないため、そのすべての要素が空虚に等しいからである。

⊥ : ∀ {ℓ} → hProp ℓ
⊥ = ⊥* , isProp⊥*

全称量化

命題族 P : A → hProp ℓ' に対する全称量化は、先に導入した Π 型である。その証明は、各 x : A に P x の証明を与える依存関数である。∀[ x ] P x と書けば x の型を Agda が推論し、∀[ x ∶ A ] P x と書けばその型を明示できる。ここでは命題的切り詰めは不要である。各 P x が命題なので、任意の二つの依存関数は各点で等しく、関数外延性によって関数そのものも等しくなる。これが isPropΠ の表す閉性である。

open import Cubical.Functions.Logic public using ( ∀[]-syntax; ∀[∶]-syntax )

含意

P ⇒ Q は含意を表す。その証拠は P の各証明を Q の証明へ送る関数なので、いま導入した全称量化の、依存しない特別な場合である。ここでは命題的切り詰めは不要である。Q が命題であるため、任意の二つの関数は各入力で等しい結果を与え、関数外延性によって関数そのものも等しくなる。したがって P に証明がいくつあっても、この関数型はすでに命題である。

open import Cubical.Functions.Logic public using ( _⇒_ )

否定

否定 ¬ P は、P から偽命題の基礎にある空型への特別な含意であり、P のどの証明からも不可能性が導かれることを述べる。一般の二項含意とは異なり、否定は P と同じ宇宙レベルにある。否定が命題について閉じることは、先に導入した二つの証明書から直接分かる。まず isProp⊥ は、レベル 0 の空な終域が命題であることを示す。次に isProp→ は、終域が命題なら、定義域の命題性を仮定せずとも関数型が命題になることを示す。したがって isProp→ を isProp⊥ に適用すれば、¬ P の基礎型が命題であることが証明される。命題的切り詰めは必要ない。

open import Cubical.Functions.Logic public using ( ¬_ )

命題外延性

命題間の双方向の含意を論理的同値と呼ぶ。命題外延性は、それを命題の宇宙における等しさへ変える。双方向の含意は、先に導入した含意を二つまとめたものである。一方の関数は P から Q へ、もう一方は Q から P へ進む。この組は積、すなわち Σ 型の依存しない特別な場合である。⇔toPath はこの二つの関数からパス P ≡ Q を作る。ここでも命題的切り詰めは不要である。P と Q は命題なので、その証明に区別できるデータはなく、二方向の含意が両者の等しさに必要な情報をすべて表すからである。さらに hProp は集合なので、得られるパス型も命題である。

open import Cubical.Functions.Logic public using ( ⇔toPath )

存在量化

存在量化は、先に導入した Σ 型から始まる。その依存対は、証人 x : A と P x の証明をともに含む。各 P x が命題でも、A の証人どうしは区別できるかもしれないため、この Σ 型は命題とは限らない。そこで、この記法はさらに命題的切り詰めを施す。∃[ x ] P x は証人の型を Agda に推論させ、∃[ x ∶ A ] P x はその型を明示するが、どちらも選ばれた証人を忘れ、何らかの証人が存在することだけを残す。したがって、切り詰める前の証拠が A の任意の要素を含むため、存在量化には切り詰めが必要である。先に見た全称量化と含意には、このような余分なデータはない。

open import Cubical.Functions.Logic public using ( ∃[]-syntax; ∃[∶]-syntax )

連言

Σ 構成に対応する依存しない特別な場合が連言である。命題 P と Q に対して、P ⊓ Q の証明は、P の証明と Q の証明を一つずつ収めた対である。上の一般的な存在量化とは異なり、ここでは命題的切り詰めは不要である。各成分がすでに命題なので、二つの第一成分は等しく、二つの第二成分も等しくなり、したがって二つの対も等しくなる。これが isProp× の表す閉性である。連言は両方の証明を保持したまま命題であり、その宇宙レベルは二つの入力レベルの最大値になる。

open import Cubical.Functions.Logic public using ( _⊓_ )

選言

もう一つの二項演算が選言 P ⊔ Q である。切り詰める前の証拠は、先に導入した直和型である。inl p は P の証明 p を、inr q は Q の証明 q を記録する。P と Q がともに命題でも、この直和型は命題とは限らない。両方が成り立つとき、左右の構成子はなお区別できる選択を記録するからである。そこで選言はこの直和型を命題的に切り詰め、選ばれた構成子とその証明を忘れ、少なくとも一方が成り立つことだけを残す。この切り詰めによって、選言は命題値になる。

open import Cubical.Functions.Logic public using ( _⊔_ )

クラスと所属関係

対象に依存する命題を使うと、与えられた対象のうち、その命題が成り立つものだけを選び出せる。集合論では、このように性質によって定められる対象の範囲をクラスと呼ぶ。

ここでいうクラスは集合論における 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 ⟩ の証明を構成することである。上付きの ᶜ は、ここでクラスへの所属を使っていることを示す。これはホストレベルの述語を、後に集合論のモデルで解釈する集合間の所属関係から区別する。前者は対象がある性質を満たすかを述べ、後者は対象言語の関係である。

open import Cubical.Foundations.Powerset public
  using () renaming ( _∈_ to _∈ᶜ_ )

クラスからは、その元のホスト側の型 Σ[ x ∶ A ] (x ∈ᶜ M) も得られる。その元は対象 x と、それが M を満たす証拠の対であり、この型は対象理論の内部で M を表す集合ではない。A が h-集合なら、各 M x の基礎型は命題なので、Cubical の補題 isSetΣSndProp により、この Σ 型も h-集合となる。本書では、この補題を isSetClass と改名して公開する。

open import Cubical.Foundations.HLevels public
  using () renaming ( isSetΣSndProp to isSetClass )

その他の帰納型

残る基本的なデータ型は、帰納的構成のいくつかの形を示す。判定は二つの答えの一方について証拠を記録し、ブール型はデータを伴わない二つのラベルを与え、自然数は再帰を支え、添字付き族 Fin と Vec は数値的な境界を型に記録する。

判定可能性

型 A を判定するとは、A に要素があるかどうかを確定する証拠を与えることである。肯定的な答えは要素 a : A を運び、否定的な答えは反証 n : A → ⊥₀ を運ぶ。後者は、A の要素を仮定すれば不可能性が導かれることを示す。帰納型 Dec A は、ちょうどこの二つの答えを構成子としてまとめる。構成規則は次のとおりである。

$$\frac{a:A}{\mathsf{yes}\,a:\operatorname{Dec}(A)}\qquad\frac{n:A\to\bot_{0}}{\mathsf{no}\,n:\operatorname{Dec}(A)}$$

したがって yes a は肯定的な答えとその証人を記録し、no n は否定的な答えとその反証を記録する。命題的な選言と異なり、Dec A は切り詰められない。プログラムは返された構成子を調べ、それが運ぶ証拠を使える。有限な比較の判定は、完全に構成的に作れる。後の章で導入する古典原理がより強いのは、指定した宇宙レベルのすべての命題に、このような判定を一様に与えるからである。

任意の型 A に対して、Dec A が命題とは限らない。二つの肯定的な判定が、A の区別できる元を運びうるからである。しかし A が命題なら、isPropDec はその判定も命題であることを示す。そのとき、肯定的な答えが運ぶ証人は等しく、否定的な答えは反証が命題値であるため等しく、肯定と否定は同時に成り立たない。

open import Cubical.Relation.Nullary public
  using ( Dec; yes; no; isPropDec )

すでに得た判定を変換することもできる。Dec A から Dec B を得るには、肯定の場合を扱う関数 f : A → B と、否定の場合を扱う関数 g : (A → ⊥₀) → (B → ⊥₀) が必要になる。mapDec f g はこの変換を行い、yes a を yes (f a) に、no n を no (g n) に送る。A の反証から一般に B の反証が得られるわけではないので、肯定側の関数だけでは足りない。関数 r : B → A もあれば、λ n b → n (r b) を否定側の変換に使える。

open import Cubical.Relation.Nullary public using ( mapDec )

ブール型

帰納型 Bool は、ちょうど二つの構成子 true と false をもつ。一般の直和型の構成子と異なり、どちらも追加のデータを運ばない。構成規則は次のとおりである。

$$\frac{}{\mathsf{true}:\operatorname{Bool}}\qquad\frac{}{\mathsf{false}:\operatorname{Bool}}$$

したがって Bool からの関数を定めるには、true の場合と false の場合の結果を一つずつ与えればよい。ブール値は、有限な判定やマスクのように、計算が区別できる二つのラベルの一方を返すときに役立つ。上で導入した真と偽の命題とは区別しなければならない。true と false は通常のデータ型 Bool の二つの値であり、命題の証明ではない。

open import Cubical.Data.Bool public using ( Bool; true; false )

自然数

自然数 ℕ は帰納型であり、Agda における元の構成子は 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、suc zero、suc (suc zero) は、Agda ではそれぞれ数値リテラル 0、1、2 と書ける。変数を含む元の式 suc (suc (suc n)) も、ここでは suc (suc (suc n)) のように簡潔に表示できる。この表記をホバーすると元の Agda コードを確認できる。

したがって、ℕ からの関数を再帰的に定義するには、zero での値と、すでに得られた n での値から suc n での値を作る方法を与えれば十分である。

加法 _+_ は二つの自然数の大きさを合わせる。後の構文の章では、文脈を拡張したり連結したりした後に使える変数の個数を計算するために用いる。

$$\mathord{+}:\mathbb N\to\mathbb N\to\mathbb N$$

$$m+n= \begin{cases} n, & m=0,\\ \operatorname{suc}(m'+n), & m=\operatorname{suc}(m') \end{cases}$$

open import Cubical.Data.Nat public
  using ( ℕ; zero; suc; _+_ )

有限添字

Fin は自然数を添字とする帰納型の族である。Agda は構成子のオーバーロードを許す。Fin の構成子 zero と suc は、ℕ の構成子と同じ名前である。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 で作られる要素が得られる。

型が Fin 3 である元について、元の式 zero、suc zero、suc (suc zero) は、それぞれ zero、suc zero、suc (suc zero) と簡潔に表示される。ホバーすると元の構成子の式と明示した型を確認できる。

関数 toℕ は上界を忘れ、有限添字を自然数として読む。この忘却写像は数としての位置を保つが、結果の型には元の上界が記録されない。

$$\operatorname{to\mathbb N}:\operatorname{Fin}(n)\to\mathbb N$$

$$\operatorname{to\mathbb N}(i)= \begin{cases} 0, & i=\mathsf{zero},\\ \operatorname{suc}(\operatorname{to\mathbb N}(j)), & i=\mathsf{suc}\,j \end{cases}$$

open import Cubical.Data.FinData public
  using ( Fin; zero; suc; toℕ )

ベクトル

ベクトル Vec A n は A の元からなるリストで、その長さが型の一部になっている。両方の引数が一文字のとき、ウェブ版ではこの型を Vec A n と表示し、「A の n 乗」と読む。これは表示上の約束にすぎず、カーソルを合わせるかタップすると元の Agda コードを確認できる。その二つの構成子は、次の推論式で表せる。

$$\frac{}{[]:A^{0}}\qquad\frac{a:A\quad v:A^{n}}{a∷v:A^{n^{+}}}$$

構成子 [] は Vec A zero の要素を与える。a : A と v : Vec A n が与えられると、構成子 _∷_ は a ∷ v : Vec A (suc n) を与える。このように自然数の添字はベクトルとともに定まる。関数 lookup の型は Fin n → Vec A n → A であり、二つの引数は同じ添字 n を共有する。

成分をすべて書き並べた短いベクトルでは、ウェブ版は a ∷ b ∷ c ∷ [] を a ∷ b ∷ c ∷ [] と表示する。この角括弧の記法にカーソルを合わせるかタップすると、元の構成子による表記と型を確認できる。末尾の成分を列挙していない a ∷ v などは元の表記を保つ。

これらの添字により、標準的なベクトル操作そのものが有用な保証を伴う。lookup の添字は Fin n の元でなければならないため、範囲外の参照はそもそも記述できない。

$$\operatorname{lookup}:\operatorname{Fin}(n)\to A^{n}\to A$$

$$\operatorname{lookup}(i,a\mathbin{∷}v)= \begin{cases} a, & i=\mathsf{zero},\\ \operatorname{lookup}(j,v), & i=\mathsf{suc}\,j \end{cases}$$

下図では有限添字を用い、長さ三のベクトルから位置を選ぶ。

$$v=a\mathbin{∷}b\mathbin{∷}c\mathbin{∷}[]:A^{3}$$

$a$$b$$c$

$$i\mapsto\operatorname{lookup}\,i\,v$$

$\operatorname{Fin}(3)$ $0$ $1$ $2$ $A$ $a$ $b$ $c$

各列はベクトルの一つの位置、その添字、参照結果を揃えている。Fin 3 が与えるのは三つの有効な添字だけであり、成分 a、b、c 自体は同じでもよい

関数 map は長さを変えずに各成分へ同じ関数を適用する。

$$\operatorname{map}:(A\to B)\to A^{n}\to B^{n}$$

$$\operatorname{map}(f,v)= \begin{cases} [], & v=[],\\ f(a)\mathbin{∷}\operatorname{map}(f,w), & v=a\mathbin{∷}w \end{cases}$$

open import Cubical.Data.Vec public
  using ( Vec; []; _∷_; lookup; map )

まとめ

本章では、本書で用いるホストレベルの基礎語彙を導入した。

Type と Level は型宇宙とそのレベルを記述する。
Π 型は依存関数を、Σ 型は依存対を表し、直和型は二つの入力型のどちら側から構成された元かを区別する。
レコード型は、名前付きフィールドと構成子によって、入れ子になった Σ 型を平坦に表す。
Lift は型を宇宙レベル間で移す。
パス型は等しさを表し、transport、subst、その二引数への一般化 subst2 はパスに沿ってデータを移す。
ホモトピーレベルは型に残る等しさの構造を記述する。命題性は Π 型、Σ 型、積について閉じ、Σ≡Prop は証明を携える依存対の等しさを第一成分の等しさへ帰着させる。
型同値 A ≃ B は写像の各ファイバーが可縮であることを表す。Iso は明示的な写像と往復則から同値を構成し、得られた同値が型の間で要素、パス、ホモトピーレベルを移す。
hProp は命題の宇宙であり、isSetHProp はその等しさの構造を記述し、⟨_⟩ は命題の記述を取り出す。
命題的切り詰め ∥ A ∥₁ は A に要素があるかを保ちつつ、具体的な証人を忘れる。rec₁ はそれを命題へ除去し、map₁ は別の切り詰めへ写す。
真と偽、連言と選言、含意と否定、全称量化と存在量化が、命題の宇宙における論理演算を与える。命題外延性は二方向の含意を命題の等しさへ変える。
クラスは命題の宇宙に値をとる述語であり、_∈ᶜ_ はクラスへの所属を表す。
Dec A は A の元または反証のいずれかを保持する。任意の命題にこの判定を一様に与えるには、さらなる原理が必要である。
Bool は二要素のデータ型であり、構成子 true と false が区別できる計算上のラベルを与える。
ℕ は自然数と加法を、Fin n は n 未満の添字を、Vec A n は範囲外参照を許さず写像で長さを保つ長さ付き列を与える。

これらの概念が、本書で採用する基本的な形式言語を構成する。