```agda
module Bernstein {A B : Type ℓ} (setA : isSet A)
(f : A → B) (fi : (x y : A) → f x ≡ f y → x ≡ y)
(g : B → A) (gi : (x y : B) → g x ≡ g y → x ≡ y) where
```
```agda
imG : A → hProp ℓ
imG x = (∥ Σ[ y ∶ B ] (g y ≡ x) ∥₁ , squash₁)
```
悪さの階層の底辺は、x が g の像にまったく属さないとき x がレベル 0 で悪いと言う。`imG x` の反証とは `⟨ imG x ⟩` から空型への写像なので `C₀ x` は関数型であり、命題への写像はふたたび命題であるため、これは命題である。ステップ演算 `C₊ C x` は、x がどこかの悪い元から一段後退りで到達できること、つまり $g y ≡ x$、$f z ≡ y$、かつ z が C に対してすでに悪いような $y ∈ B$ と $z ∈ A$ が単に存在することを言う。`C₀` からこの演算を繰り返して `Cₙ` が得られ、したがって `Cₙ n x` の元は、x = g y、y = f z、z は一段下で悪い、という長さ n の交互の鎖を記録する。
```agda
C₀ : A → hProp ℓ
C₀ x = ((⟨ imG x ⟩ → ⊥₀) , isPropΠ (λ _ → isProp⊥))
C₊ : (A → hProp ℓ) → A → hProp ℓ
C₊ C x = (∥ Σ[ y ∶ B ] Σ[ z ∶ A ] ((g y ≡ x) × ((f z ≡ y) × ⟨ C z ⟩)) ∥₁ , squash₁)
Cₙ : ℕ → A → hProp ℓ
```
`Cₙ` の二つの定義等式は計算規則である。添字がゼロなら基底の述語であり、後続ならステップを一度適用する。完全な悪さの命題 `C x` は、すべての鎖の長さにわたって一度に命題的切り詰めする。ある `Cₙ n x` が単に成り立つなら x は悪くなる。ここでの命題的切り詰めは本質的で、階層の無限に多くの段を、後で排中律を適用できる単一の命題へと折りたたむ。
```agda
Cₙ 0 = C₀
Cₙ (suc n) = C₊ (Cₙ n)
C : A → hProp ℓ
C x = (∥ Σ[ n ∶ ℕ ] ⟨ Cₙ n x ⟩ ∥₁ , squash₁)
```
階層を使う前に、小さな簿記の補題を一つ記録する。任意の固定レベル n での悪さの証明は、悪さの証明を与えるというものである。内容は単純で、対 (n , proof) が `C` を定義する命題的切り詰めされた存在文の証人であり、∣ ⋯ ∣₁ がその証人を命題的切り詰めへ注入する、というだけである。後で何らかの長さの鎖を作る議論はすべて、この写像を通る。
```agda
c-in : {x : A} {n : ℕ} → ⟨ Cₙ n x ⟩ → ⟨ C x ⟩
c-in {x} {n} h = ∣ n , h ∣₁
```
冒頭で約束した構造的事実がここで証明される。x が悪ければ g (f x) も悪くなる。長さ n で x で終わる鎖が与えられれば、一段後ろへ延ばすだけである。x 自身が元 z として、f x が元 y として働き、必要なパス g (f x) ≡ g (f x) と f x ≡ f x はどちらも反射性であり、古い鎖が尾になる。結果は長さ suc n で g (f x) で終わる鎖である。入力が命題的切り詰めされているため、消去 `rec₁` は出力の命題性を対象とする。`C (g (f x))` は命題なのでこれは正当である。
```agda
gf-closed : {x : A} → ⟨ C x ⟩ → ⟨ C (g (f x)) ⟩
gf-closed {x} = rec₁ ((C (g (f x))) .snd) go
where
go : Σ[ n ∶ ℕ ] ⟨ Cₙ n x ⟩ → ⟨ C (g (f x)) ⟩
go (n , cx) = c-in {x = g (f x)} {n = suc n} ∣ f x , x , (refl , (refl , cx)) ∣₁
```
g ∘ f による閉性は悪さが前へ伝わることを教えるが、元を h で振り分けるには一段後ろも見る必要がある。悪さの証明は、レベル 0 で底を突くか、さもなくば x は g (f z) の形で z が悪いかのどちらかである。これこそ `C-view` が与えるものである。対象自身が命題的切り詰めされているので、鎖の長さ n についてのケース分析が実際のデータであっても、そこへの消去は問題ない。
```agda
C-view : {x : A} → ⟨ C x ⟩
→ ∥ (⟨ C₀ x ⟩ ⊎ (Σ[ z ∶ A ] ((g (f z) ≡ x) × ⟨ C z ⟩))) ∥₁
C-view {x} = rec₁ squash₁ go
where
```
証明は記録された長さについて場合分けする。長さ 0 なら鎖は x が g の像の外であると主張するだけで、これは左の選言肢そのものである。長さ suc n なら保存された証人は y と z の組で、g y ≡ x、f z ≡ y、そして z の長さ n の悪さの証明が成り立つ。二つのパスを g を経由して合成すれば g (f z) ≡ x が得られ、より短い鎖は `c-in` で取り込まれる。右の選言肢はちょうど対 (z，そのパス，その短い証明) の命題的切り詰めである。この補題は後の全射性の中核である。g y に適用すると、悪さを直接反証するか、さもなくば原像 z を作り出す。
```agda
go : Σ[ n ∶ ℕ ] ⟨ Cₙ n x ⟩ → ∥ (⟨ C₀ x ⟩ ⊎ (Σ[ z ∶ A ] ((g (f z) ≡ x) × ⟨ C z ⟩))) ∥₁
go (0 , c0) = ∣ inl c0 ∣₁
go (suc n , cs) = map₁ inr (map₁ (λ { (y , z , gy , fz , cz) →
z , ((cong g fz ∙ gy) , c-in {x = z} {n = n} cz) }) cs)
```
排中律の二度目の使用は、良さを像への所属に変える。x が良いとする。ここでは `C x` が反証を許すという強い意味で取る。命題 `imG x` を判定すると、原像が得られるか、望むところである。あるいは像への所属の反証、すなわち `C₀ x` の証明が得られる。しかしレベル 0 は `c-in` を経由して悪さを含意し、仮定された `C x` の反証と矛盾する。この矛盾から何でも出る。したがって `notC→imG` は `⟨ imG x ⟩` の元を作るが、それはまだ存在することだけを述べており、まだ原像は選ばれていない。
```agda
notC→imG : {x : A} → (⟨ C x ⟩ → ⊥₀) → ⟨ imG x ⟩
notC→imG {x} nC with lem (imG x)
... | yes h = h
... | no nC₀ = ⊥₀-rec (nC (c-in {n = zero} nC₀))
```
単なる像への所属を選ばれた原像に変えるには、その繊維型 `Σ[ y ∶ B ] (g y ≡ x)` 自身が命題である限り、命題的切り詰めをその型へ直接消去できる。ここで `g` と `A` に関する仮定が効く。`g` の単射性は、`g x` へのパス `p` と `p′` を使って任意の二つの原像 `y` と `y′` が等しいことを示し、`A` の h-集合としての構造が `A` における等式を命題にするので、`Σ≡Prop` がこれを対全体へ拡げる。h-集合の仮定が必要なのはまさにこの一点だけで、構成の他のどこでもない。
```agda
fiberG-prop : (x : A) → isProp (Σ[ y ∶ B ] (g y ≡ x))
fiberG-prop x (y , p) (y' , p') = Σ≡Prop {A = B} {B = λ y → g y ≡ x}
(λ y → setA (g y) x) (gi y y' (p ∙ sym p'))
```
繊維の命題性が手に入れば、`fiberG` は命題的切り詰めされた像の主張を繊維型へ消去するものである。対象が命題なので、`rec₁` は繊維上の恒等写像を作用として適用できる。これは議論の中で、選ばれた原像が単にではなくデータとして存在する最初の地点である。それを開いたのは排中律と h-集合としての構造であって、命題的切り詰めそのものの性質ではない。
```agda
fiberG : (x : A) → ⟨ imG x ⟩ → Σ[ y ∶ B ] (g y ≡ x)
fiberG x = rec₁ (fiberG-prop x) (λ w → w)
```
良い元 x に対しては、選ばれた原像を `ginv x` と名付けられる。これは `notC→imG` から `fiberG` が作る繊維の第 1 成分である。仕様 `ginv-spec` は g (ginv x) ≡ x を記録し、同じ繊維の第 2 成分から取られる。したがって良い側では h は x を、g による像がちょうど x である B の点へ送り返す。g の逆の断片としての当然の振る舞いである。
```agda
ginv : {x : A} → (⟨ C x ⟩ → ⊥₀) → B
ginv {x} nC = fiberG x (notC→imG nC) .fst
ginv-spec : {x : A} (nC : ⟨ C x ⟩ → ⊥₀) → g (ginv nC) ≡ x
ginv-spec {x} nC = fiberG x (notC→imG nC) .snd
```
候補となる全単射 h は、A に直接ではなく仮想的な判定の上で定義される。x と悪さの命題 `C x` の判定 d が与えられると、悪いの場合は x を f x へ、良いの場合は `ginv x` へ送る。判定を明示的な引数として扱うことでケース分析は誠実に保たれ、続く二つの補題、判定に相対的な単射性と全射性は、節の最後で `lem` が与える実際の判定と結合される。
```agda
h : (x : A) → Dec ⟨ C x ⟩ → B
h x (yes _) = f x
h x (no nC) = ginv nC
```
h の単射性は判定の対について四つの場合で証明する。両側が悪いのときは h は両側で f であり、f の単射性ですぐ終わる。x が悪く x′ が良いのとき、仮定 h x dx ≡ h x′ dx′ は g (f x) ≡ ginv x′ を言い、g を施して ginv の仕様を使えば g (g (f x)) ≡ x′ が得られる。悪さは g ∘ f に沿って伝わるので、x が悪ければ g (f x) も悪くなる。`subst` で g (f x) の悪さをそのパスに沿って輸送すれば x′ が悪いとなり、x′ が良いという判定と矛盾する。
```agda
h-inj : (x x' : A) (dx : Dec ⟨ C x ⟩) (dx' : Dec ⟨ C x' ⟩)
→ h x dx ≡ h x' dx' → x ≡ x'
h-inj x x' (yes cx) (yes cx') e = fi x x' e
h-inj x x' (yes cx) (no nCx') e =
⊥₀-rec (nCx' (subst (λ w → ⟨ C w ⟩) (cong g e ∙ ginv-spec nCx') (gf-closed {x = x} cx)))
```
鏡像の場合、x が良く x′ が悪いのときは対称である。輸送は逆向きのパスに沿って行われ、消されるのは x の方である。最後の場合は両側が良く、h は両側で ginv となり、等式は ginv x ≡ ginv x′ と読める。g を施せば g (ginv x) ≡ g (ginv x′) となり、その前後で ginv の二つの仕様をつなげば x ≡ x′ が直接得られる。この補題では h-集合の仮定はどこにも使われず、単射性は判定についての純粋なケース分析である。
```agda
h-inj x x' (no nCx) (yes cx') e =
⊥₀-rec (nCx (subst (λ w → ⟨ C w ⟩) (sym (cong g e) ∙ ginv-spec nCx) (gf-closed {x = x'} cx')))
h-inj x x' (no nCx) (no nCx') e = sym (ginv-spec nCx) ∙ cong g e ∙ ginv-spec nCx'
```
判定に相対的な全射性は各 y ∈ B について述べられ、判定は B の元ではなく A の元 g y に対して取られる。良いの場合は原像は単純に g y 自身である。仮定によりそれは良く、h はそれを `ginv (g y)` に送り、ginv の仕様と g の単射性でその値を y と同一視する。証人は命題的切り詰めされた対としてまとめられる。最終定理が単なる全射性しか主張しないからである。
```agda
h-surj : (y : B) (d : Dec ⟨ C (g y) ⟩)
→ ∥ Σ[ x ∶ A ] Σ[ dx ∶ Dec ⟨ C x ⟩ ] (h x dx ≡ y) ∥₁
h-surj y (no nCgy) = ∣ g y , no nCgy , gi (ginv nCgy) y (ginv-spec nCgy) ∣₁
```
g y が悪いの場合は `C-view` が悪さの証明を二つの選択肢に分解する。第一は g y が g の像の外にあるというもので、しかし y 自身がパス反射律で像への所属の証人となり、矛盾から何でも、特に必要な命題的切り詰めされた主張が出る。第二は g (f z) ≡ g y かつ z が悪いような z ∈ A を作り出す。このとき z は原像である。h z = f z であり g (f z) は g y に等しく、g の単射性で f z を y と同一視できるからである。両方の枝が証人を一つの命題的切り詰めの中で示すので、すでに仮定した判定以外の判定は消費されない。
```agda
h-surj y (yes cgy) = rec₁ squash₁
(λ { (inl c0) → ⊥₀-rec (c0 ∣ y , refl ∣₁) ; (inr (z , gfy , cz)) → ∣ z , yes cz , gi (f z) y gfy ∣₁ })
(C-view {x = g y} cgy)
```
最後の補題は設計全体への異議に答える。h は判定に相対的に定義されたが、定理には A 上の単一の関数が必要である。`h-cons` は判定の選び方が問題にならない、固定された x に対しては二つの出力が等しい、と言う。両方悪ければ反射律であり、どちらかが混在する場合は一方の判定が他方の証人を反証するので矛盾し、両方良いの場合は選ばれた原像の一意性に帰着する。`fiberG` が作る二つの繊維は、繊維型が命題であるため等しく、第 1 成分を取ることは合同性によってその等式を保つ。この整合性こそが、判定依存の構成を写像の正当な定義にしているのである。
```agda
h-cons : (x : A) (dx dx' : Dec ⟨ C x ⟩) → h x dx ≡ h x dx'
h-cons x (yes cx) (yes cx') = refl
h-cons x (yes cx) (no nCx') = ⊥₀-rec (nCx' cx)
h-cons x (no nCx) (yes cx) = ⊥₀-rec (nCx cx)
h-cons x (no nCx) (no nCx') = cong (λ p → p .fst) (fiberG-prop x (fiberG x (notC→imG nCx)) (fiberG x (notC→imG nCx')))
```
整合性が確立されれば、判定は一度だけ与えればよくなる。続く三行で定理が組み上がる。
```agda
ĥ : A → B
```
写像 `ĥ` は h を標準的な判定 `lem (C x)` に適用したものである。排中律が各 x の悪さを判定し、h-cons が他のどんな判定でも同じ値になると保証する。ここでモジュールの仮定 `lem` が定義そのものとして消費される。
```agda
ĥ x = h x (lem (C x))
```
単射性は相対版からそのまま移る。標準的な判定は判定引数の特定の選び方にすぎないからである。`ĥ-inj x x' e` はまさにそれらの判定における `h-inj` である。
```agda
ĥ-inj : (x x' : A) → ĥ x ≡ ĥ x' → x ≡ x'
ĥ-inj x x' e = h-inj x x' (lem (C x)) (lem (C x')) e
```
全射性にはもう一段必要である。g y に対する標準的な判定に相対補題 `h-surj` を適用すると、命題的切り詰めされた三つ組 x、dx とパス h x dx ≡ y が得られるが、その最初の二つの成分は仮想的な h x dx についてのもので、`ĥ x` についてのものではない。二つの値を同一視する `h-cons x dx (lem (C x))` に沿って書き換え、対称パスを前につなげれば、三つ組は `ĥ x ≡ y` の証人に変わる。主張全体は命題的切り詰めされたままである。定理は原像が単に存在すると主張するだけである。
```agda
ĥ-surj : (y : B) → ∥ Σ[ x ∶ A ] (ĥ x ≡ y) ∥₁
ĥ-surj y = map₁ (λ { (x , dx , e) → x , sym (h-cons x dx (lem (C x))) ∙ e })
(h-surj y (lem (C (g y))))
```
抽象的な構成を、いよいよ累積階層そのものに適用する。V の各元 a はメンバー型 ⟪ a ⟫、すなわちそのメンバーの型を伴う。Bernstein の構成は第一の型が h-集合であることを要求するので、最初の一歩は ⟪ a ⟫ がそうであることの証明である。埋め込み ⟪ a ⟫↪ は各メンバーの指標を、V の中でそれが指すメンバーへ送る。V は h-集合であり、この写像は埋め込みなので、その定義域は h-集合性を受け継ぐ。この一事実があれば、⟪ a ⟫ と ⟪ b ⟫ の間の相互の単射から、依存する三つ組としてまとめられた全単射が得られる。
h-集合性の証明書は、取り込まれた二つの事実を合成したものである。写像 ⟪ a ⟫↪ は V への埋め込み、つまりすべての繊維が命題であるような写像であり、階層 V はその構成子 setIsSet により h-集合である。h-集合へ埋め込まれる型はそれ自身 h-集合になる。定義域の等式は埋め込みを施した後に比較できるからである。続くシグニチャは、抽象定理と同じ形で集合論的な帰結を述べる。⟪ a ⟫ から ⟪ b ⟫ への単射 f と戻りの単射 g、それぞれの単射性の証明とともに、明示的な仮定として取られる。
```agda
small-set : (a : V ℓ) → isSet (⟪ a ⟫)
small-set a = Embedding-into-isSet→isSet (⟪ a ⟫↪ , isEmb⟪ a ⟫↪) setIsSet
cantor-bernstein : (a b : V ℓ) (f : ⟪ a ⟫ → ⟪ b ⟫)
→ ((x y : ⟪ a ⟫) → f x ≡ f y → x ≡ y)
→ (g : ⟪ b ⟫ → ⟪ a ⟫) → ((x y : ⟪ b ⟫) → g x ≡ g y → x ≡ y)
```
結果の型はレコードではなく明示的な依存する三つ組である。⟪ a ⟫ から ⟪ b ⟫ への関数 h、その単射性を命題値の成分として、そして単なる全射性、すなわち ⟪ b ⟫ の各 y に対する命題的切り詰めされた原像の主張である。二つの側条件の非対称性は意図的なもので、抽象定理と呼応する。単射性は正味のデータとして、全射性は単なる存在として述べられる。主張のどこにも階層の段や所属についての量化はなく、すべては二つのメンバー型の内部で起こる。
```agda
→ Σ[ h ∶ (⟪ a ⟫ → ⟪ b ⟫) ]
(((x y : ⟪ a ⟫) → h x ≡ h y → x ≡ y)
× ((y : ⟪ b ⟫) → ∥ Σ[ x ∶ ⟪ a ⟫ ] (h x ≡ y) ∥₁))
cantor-bernstein a b f fi g gi = M.ĥ , ( M.ĥ-inj , M.ĥ-surj )
where
```
証明は一回のインスタンス化だけである。モジュール `Bernstein` を A = ⟪ a ⟫、B = ⟪ b ⟫ で実例化し、A に h-集合性の証明書を供給し、二つの単射をそのまま渡せば、成分 ĥ、ĥ-inj、ĥ-surj が現れる。定義はそれらを三つ組に組み立てる。前節の仕事のすべてが、変更なしに再利用されるのである。
```agda
module M = Bernstein {A = ⟪ a ⟫} {B = ⟪ b ⟫} (small-set a) f fi g gi
```
上の帰結は V のメンバー型に固定されている。より再利用しやすい形は、設定を抽象的に保つ。符号の台 `C`、各符号に小さな型を割り当てる `P`、そして a が P a から P b への単射を符号化していることを表す関係 `R a b` である。この抽象を前節と結びつけるのが読み戻し `read` である。R a b の元から、実際の関数とその単射性の証明を取り出す。両方向にそのような読み戻しがあれば、Bernstein の構成はそのまま適用できる。入口は二つ用意されている。一方は符号化された単射の対をデータとして受け取り、もう一方は単なる存在として受け取り、その場合は全単射も単に存在するだけになる。
パラメータは必要な強さを正確に列挙する。台 C はそれ自身のレベル ℓ₁ に、関係 R は ℓ₂ に住むので、符号やその関係は小さくなくて構わない。小さくなければならないのは各 P a で、排中律が使える固定レベル ℓ に住む。各 a について P a は h-集合だと仮定され、Bernstein モジュールの h-集合性の仮定に対応する。関係 R 自身は型としてまったく任意である。読み戻し以外には何も仮定しない。読み戻しは R a b の元から、第 1 成分が関数 P a → P b、第 2 成分がその関数の単射性の証明である対を返す。特に、取り出された単射は正味のデータであり、命題的切り詰めされた存在ではない。