小さな提示に対する Cantor–Schröder–Bernstein の定理

この章を読むか、読書案内と依存マップで別のルートを選べます。

二つの集合の小さな提示の間に双方向の単射があれば、全単射が得られます。まず排中律の下で小さな型について全単射を構成し、さらに任意の相互に読み出せる符号化された単射からそのような全単射を得る一般的な形にまとめます。

古典的な Cantor–Schröder–Bernstein の定理は、単射 $f : A → B$ と $g : B → A$ から全単射 $A → B$ が得られるというものです。この章では二つの型が同一の宇宙レベル ℓ を共有し、追加の仮定はそのレベルでの排中律、すなわちレベル ℓ に住む各命題に対する証明か反証かだけです。議論そのものは累積階層の集合ではなく指標型 $A$ と $B$ に属します。まさにそのおかげで、後で任意の小さな提示のメンバー型へそのまま再生できるのです。証明は命題を命題的切り詰めで作り、それを判定する必要があるため、以下の設定ではその古典的仮定と、それを適用する命題値の語彙の両方を固定します。

レベル ℓ での判定はここで一度だけまとめられ、章全体で再利用されます。LEM ℓ は命題 P : hProp ℓ を受け取り、⟨ P ⟩ の証明か、あるいは ⟨ P ⟩ を空型へ写す反証のどちらかを返します。したがってモジュールパラメータ lem はこの一レベルでの実例であって、すべてのレベルに及ぶ大域的な原理ではありません。章で構成されるものはすべてこれに対してパラメトリックであり、古典的な判定が使われる箇所では必ずこの仮定が明示的に現れます。

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM )

module V.CantorBernstein {ℓ : Level} (lem : LEM ℓ) where

open import Cubical.Functions.Embedding using ( Embedding-into-isSet→isSet )

証明は、存在を命題的切り詰めした命題をいくつも作ります。x が g の像に属するという主張は ∥ Σ[ y ∈ B ] (g y ≡ x) ∥₁ であり、選ばれた原像を持たず、存在することだけが保留されています。このような命題的切り詰めされた主張は squash₁ によって命題になり、その証明は命題値の対象へは消去できますが、任意のデータへはできません。この制限こそが古典的仮定を必要とする理由です。議論が選ばれた原像を要する場面で、単なる存在性を選ばれた原像へ変えるのに排中律を使います。

import Cubical.Data.Sum as Sum
open Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
open import Cubical.Data.Empty.Properties using ( isProp⊥ )
import Cubical.HITs.PropositionalTruncation as PT

この章を支配するのは二種類の命題です。g の像への所属と、有限の交互の鎖で到達できることです。どちらも hProp ℓ の要素として保存されます。hProp ℓ は基礎型と、それが命題であることの証明をひとまとめにするもので、⟨ P ⟩ が基礎型を取り出し、命題性の証明は第 2 成分に残ります。残りの import はその周辺の機構を供給します。良し悪しの場合分けのための非交和、反証側のための isProp⊥、第 2 成分が命題値であるような対を同一視するための Σ≡Prop、そして累積階層と、集合のメンバー型 ⟪ a ⟫ がある集合へ埋め込めるため h-集合であるという事実です。

open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪ )

互いに逆向きの二つの単射から、ひとつの全単射が得られます。この節は、同一の宇宙レベルにある二つの型 $A$ と $B$($A$ は h-集合) について、そのレベルの排中律の下でこれを証明します。構成は $A$ の各元を悪いか良いかに分類します。悪い元とは、g の像の外から始まる有限の交互の原像の鎖で到達できる元のことです。悪い元は f で前へ送り、良い元は g の選ばれた逆像に沿って送り戻します。排中律は二度使われます。一度は悪さの命題 C を判定するため、もう一度は命題的切り詰めされた像の主張から選ばれた原像を取り出すためです。鎖そのものは述語族 Cₙ であり、必要な構造的事実は $x ↦ g (f x)$ が悪さを保つことだけです。

構成はモジュール Bernstein にまとめられ、受け取るのはまさに古典的なデータです。二つの型、$A$ の h-集合としての構造、そして二つの単射で、各々は関数とその単射性の証明の組として与えられます。最初の材料は像の述語 imG x で、ある $y ∈ B$ が $g y ≡ x$ を満たすことを単に (単に) 主張します。ここで原像は選ばれません。命題的切り詰め ∥ ⋯ ∥₁ が証人を消して命題だけを残し、squash₁ がその命題性の証明書になります。

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

  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 の交互の鎖を記録します。

  C₀ : A → hProp ℓ
  C₀ x = ((⟨ imG x ⟩ → Empty.⊥) , 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 は悪くなります。ここでの命題的切り詰めは本質的で、階層の無限に多くの段を、後で排中律を適用できる単一の命題へと折りたたみます。

  Cₙ zero = C₀
  Cₙ (suc n) = C₊ (Cₙ n)

  C : A → hProp ℓ
  C x = (∥ Σ[ n ∈ ℕ ] ⟨ Cₙ n x ⟩ ∥₁ , squash₁)

階層を使う前に、小さな簿記の補題を一つ記録します。任意の固定レベル n での悪さの証明は、悪さの証明を与えるというものです。内容は単純で、対 (n , proof) が C を定義する命題的切り詰めされた存在文の証人であり、∣ ⋯ ∣₁ がその証人を命題的切り詰めへ注入する、というだけです。後で何らかの長さの鎖を作る議論はすべて、この写像を通ります。

  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) で終わる鎖です。入力が命題的切り詰めされているため、消去 PT.rec は出力の命題性を対象とします。C (g (f x)) は命題なのでこれは正当です。

  gf-closed : {x : A} → ⟨ C x ⟩ → ⟨ C (g (f x)) ⟩
  gf-closed {x} = PT.rec (snd (C (g (f x)))) 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 についてのケース分析が実際のデータであっても、そこへの消去は問題ありません。

  C-view : {x : A} → ⟨ C x ⟩
         → ∥ (⟨ C₀ x ⟩ ⊎ (Σ[ z ∈ A ] ((g (f z) ≡ x) × ⟨ C z ⟩))) ∥₁
  C-view {x} = PT.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 を作り出します。

    go : Σ[ n ∈ ℕ ] ⟨ Cₙ n x ⟩ → ∥ (⟨ C₀ x ⟩ ⊎ (Σ[ z ∈ A ] ((g (f z) ≡ x) × ⟨ C z ⟩))) ∥₁
    go (zero , c0) = ∣ inl c0 ∣₁
    go (suc n , cs) = PT.map inr (PT.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 ⟩ の元を作りますが、それはまだ存在することだけを述べており、まだ原像は選ばれていません。

  notC→imG : {x : A} → (⟨ C x ⟩ → Empty.⊥) → ⟨ imG x ⟩
  notC→imG {x} nC = Sum.rec {A = ⟨ imG x ⟩} {B = ⟨ imG x ⟩ → Empty.⊥} {C = ⟨ imG x ⟩}
    (λ h → h) (λ nC₀ → Empty.rec (nC (c-in {n = zero} nC₀)))
    (lem (imG x))

単なる像への所属を選ばれた原像に変えるには、その繊維型 Σ[ y ∈ B ] (g y ≡ x) 自身が命題である限り、命題的切り詰めをその型へ直接消去できます。ここで g と A に関する仮定が効きます。g の単射性は、g x へのパス p と p′ を使って任意の二つの原像 y と y′ が等しいことを示し、A の h-集合としての構造が A における等式を命題にするので、Σ≡Prop がこれを対全体へ拡げます。h-集合の仮定が必要なのはまさにこの一点だけで、構成の他のどこでもありません。

  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 は命題的切り詰めされた像の主張を繊維型へ消去するものです。対象が命題なので、PT.rec は繊維上の恒等写像を作用として適用できます。これは議論の中で、選ばれた原像が単にではなくデータとして存在する最初の地点です。それを開いたのは排中律と h-集合としての構造であって、命題的切り詰めそのものの性質ではありません。

  fiberG : (x : A) → ⟨ imG x ⟩ → Σ[ y ∈ B ] (g y ≡ x)
  fiberG x = PT.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 の逆の断片としての当然の振る舞いです。

  ginv : {x : A} → (⟨ C x ⟩ → Empty.⊥) → B
  ginv {x} nC = fiberG x (notC→imG nC) .fst

  ginv-spec : {x : A} (nC : ⟨ C x ⟩ → Empty.⊥) → 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 が与える実際の判定と結合されます。

  h : (x : A) → ⟨ C x ⟩ ⊎ (⟨ C x ⟩ → Empty.⊥) → B
  h x (inl _) = f x
  h x (inr 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′ が良いという判定と矛盾します。

  h-inj : (x x' : A) (dx : ⟨ C x ⟩ ⊎ (⟨ C x ⟩ → Empty.⊥)) (dx' : ⟨ C x' ⟩ ⊎ (⟨ C x' ⟩ → Empty.⊥))
        → h x dx ≡ h x' dx' → x ≡ x'
  h-inj x x' (inl cx) (inl cx') e = fi x x' e
  h-inj x x' (inl cx) (inr nCx') e =
    Empty.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-集合の仮定はどこにも使われず、単射性は判定についての純粋なケース分析です。

  h-inj x x' (inr nCx) (inl cx') e =
    Empty.rec (nCx (subst (λ w → ⟨ C w ⟩) (sym (cong g e) ∙ ginv-spec nCx) (gf-closed {x = x'} cx')))
  h-inj x x' (inr nCx) (inr 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 と同一視します。証人は命題的切り詰めされた対としてまとめられます。最終定理が単なる全射性しか主張しないからです。

  h-surj : (y : B) (d : ⟨ C (g y) ⟩ ⊎ (⟨ C (g y) ⟩ → Empty.⊥))
         → ∥ Σ[ x ∈ A ] Σ[ dx ∈ ⟨ C x ⟩ ⊎ (⟨ C x ⟩ → Empty.⊥) ] (h x dx ≡ y) ∥₁
  h-surj y (inr nCgy) = ∣ g y , inr 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 と同一視できるからです。両方の枝が証人を一つの命題的切り詰めの中で示すので、すでに仮定した判定以外の判定は消費されません。

  h-surj y (inl cgy) = PT.rec squash₁
    (λ { (inl c0) → Empty.rec (c0 ∣ y , refl ∣₁) ; (inr (z , gfy , cz)) → ∣ z , inl cz , gi (f z) y gfy ∣₁ })
    (C-view {x = g y} cgy)

最後の補題は設計全体への異議に答えます。h は判定に相対的に定義されましたが、定理には A 上の単一の関数が必要です。h-cons は判定の選び方が問題にならない、固定された x に対しては二つの出力が等しい、と言います。両方悪ければ反射律であり、どちらかが混在する場合は一方の判定が他方の証人を反証するので矛盾し、両方良いの場合は選ばれた原像の一意性に帰着します。fiberG が作る二つの繊維は、繊維型が命題であるため等しく、第 1 成分を取ることは合同性によってその等式を保ちます。この整合性こそが、判定依存の構成を写像の正当な定義にしているのです。

  h-cons : (x : A) (dx dx' : ⟨ C x ⟩ ⊎ (⟨ C x ⟩ → Empty.⊥)) → h x dx ≡ h x dx'
  h-cons x (inl cx) (inl cx') = refl
  h-cons x (inl cx) (inr nCx') = Empty.rec (nCx' cx)
  h-cons x (inr nCx) (inl cx) = Empty.rec (nCx cx)
  h-cons x (inr nCx) (inr nCx') = cong fst (fiberG-prop x (fiberG x (notC→imG nCx)) (fiberG x (notC→imG nCx')))

整合性が確立されれば、判定は一度だけ与えればよくなります。続く三行で定理が組み上がります。

  ĥ : A → B

写像 ĥ は h を標準的な判定 lem (C x) に適用したものです。排中律が各 x の悪さを判定し、h-cons が他のどんな判定でも同じ値になると保証します。ここでモジュールの仮定 lem が定義そのものとして消費されます。

  ĥ x = h x (lem (C x))

単射性は相対版からそのまま移ります。標準的な判定は判定引数の特定の選び方にすぎないからです。ĥ-inj x x' e はまさにそれらの判定における h-inj です。

  ĥ-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 の証人に変わります。主張全体は命題的切り詰めされたままです。定理は原像が単に存在すると主張するだけです。

  ĥ-surj : (y : B) → ∥ Σ[ x ∈ A ] (ĥ x ≡ y) ∥₁
  ĥ-surj y = PT.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、それぞれの単射性の証明とともに、明示的な仮定として取られます。

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 に対する命題的切り詰めされた原像の主張です。二つの側条件の非対称性は意図的なもので、抽象定理と呼応します。単射性は正味のデータとして、全射性は単なる存在として述べられます。主張のどこにも階層の段や所属についての量化はなく、すべては二つのメンバー型の内部で起こります。

    → Σ[ 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 が現れます。定義はそれらを三つ組に組み立てます。前節の仕事のすべてが、変更なしに再利用されるのです。

  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 成分がその関数の単射性の証明である対を返します。特に、取り出された単射は正味のデータであり、命題的切り詰めされた存在ではありません。

module MutualInj {ℓ₁ ℓ₂ : Level} (C : Type ℓ₁) (P : C → Type ℓ)
    (R : (a b : C) → Type ℓ₂)
    (setP : (a : C) → isSet (P a))
    (read : (a b : C) → R a b
          → Σ[ f ∈ (P a → P b) ] ((x y : P a) → f x ≡ f y → x ≡ y)) where

最初の入口は、符号化された二つの単射を明示的な引数として移行を述べます。R a b の前向きの符号と R b a の後ろ向きの符号から、前節とまったく同じ形で P a と P b の間の全単射の三つ組を返します。主張は関係の命題的切り詰めではなく元について量化するので、符号は全体を通じてデータとして手に入ります。

  mutual→bijection : (a b : C) → R a b → R b a
    → Σ[ h ∈ (P a → P b) ]
        (((x y : P a) → h x ≡ h y → x ≡ y)
      × ((y : P b) → ∥ Σ[ x ∈ P a ] (h x ≡ y) ∥₁))
  mutual→bijection a b fwd bwd = M.ĥ , ( M.ĥ-inj , M.ĥ-surj )

定義は Bernstein モジュールを A = P a、B = P b で実例化します。読み戻しが使われるのはまさにここです。前向きの符号 fwd は read a b によって関数と単射性の成分にほどかれ、後ろ向きの符号も同様ですが、R と read の引数の向きが逆になります。各成分は第 1、第 2 成分の射影で取り出されます。h-集合性の欄には setP a が渡ります。したがって Bernstein モジュールに届くのは正味の単射であり、そこで証明されたことはすべてそのまま適用されます。

    where
    module M = Bernstein {A = P a} {B = P b} (setP a)
      (read a b fwd .fst) (read a b fwd .snd)
      (read b a bwd .fst) (read b a bwd .snd)

二つ目の入口は入力を単なる存在まで弱めます。受け取るのは符号ではなく、そのような符号が単に存在するという命題的切り詰めされた主張です。結論もそれに応じて二度弱められます。全単射の主張自身が命題的切り詰めされており、全射性はもともと内部で命題的切り詰めされていました。したがって最終的な型が主張するのは、特定の全単射を名指せることではなく、全単射が単に存在することです。弱めることは不可逆です。入力の命題的切り詰めは全単射のデータへは消去できず、命題値の対象へしか消去できません。主張全体がちょうどそのような対象です。

  ∃bijection : (a b : C) → ∥ R a b ∥₁ → ∥ R b a ∥₁
    → ∥ Σ[ h ∈ (P a → P b) ]
        (((x y : P a) → h x ≡ h y → x ≡ y)
      × ((y : P b) → ∥ Σ[ x ∈ P a ] (h x ≡ y) ∥₁)) ∥₁
  ∃bijection a b fwd bwd = PT.rec squash₁

証明は二つの命題的切り詰めの消去を入れ子にします。fwd を消去すればある符号 w が得られ、bwd を消去すれば w′ が得られます。内側の消去の対象は全単射の主張全体の命題的切り詰めであり、squash₁ によって命題なので、mutual→bijection から明示的な三つ組を作り ∣ ⋯ ∣₁ で注入するのは正当です。二つの消去の順序は、どちらの対象も命題であるため問題になりません。

    (λ w → PT.rec squash₁ (λ w' → ∣ mutual→bijection a b w w' ∣₁) bwd)
    fwd