Mostowski 崩壊

再帰的な崩壊

各集合 x に対し、写像 π は、x の要素のうち台 X にも属するものの崩壊値からなる集合へ x を送るべきである。これは所属に関する再帰による定義である。π x を知るには x の要素 y に対する π y が分かれば足りる。周囲の階層における所属の整礎性が、まさにこの形の定義を可能にし、その計算規則も与えてくれる。

インデックス型 Fiber x はフィルタリングされた要素を選ぶ。x の提示におけるインデックス m で、名指しされた要素 ⟪ x ⟫↪ m が X の小所属を持つものである。フィルタはそれ自身レベル ℓ の命題である小所属を使うので、インデックス型は Type ℓ に属し、得られる集合は正当に小さくなる。再帰のステップは新しい集合を提示する。インデックスがインデックスの組であり、各インデックスは、x の対応する要素 ⟪ x ⟫↪ m への rec の適用を名指す。再帰呼び出しを正当化するため、所属証明 member x m も添えられる。情報の流れの向きに注意してほしい。ここでは fiber は使われず、台への所属の証拠はデータとしてインデックスの組の中に担われている。

Fiber : S → Type ℓ
Fiber x = Σ[ m ∶ ⟪ x ⟫ ] ⟨ ⟪ x ⟫↪ m ∈ₛ X ⟩

step : (x : S) → (∀ y → y ∈ᵗ x → S) → S
step x rec = sett (Fiber x) (λ p → rec (⟪ x ⟫↪ (p .fst)) (member x (p .fst)))

∈ 再帰の原理を step で具体化すると崩壊写像 π が得られる。再帰定理は、π x を step x が提示する集合へと展開する等式も与える。以後の議論が実際に使うのはこの等式である。

定義 π = ∈-induction step は、階層の章の再帰原理への一度の呼び出しである。所属が整礎であるため、この再帰ステップで定まる関数が S 全体に存在する。opaque ブロックは π を封印として印付ける。型検査器は使用箇所で自動的には展開しなくなり、π に言及する証明項が小さく保たれる。

opaque
  π : S → S
  π = ∈-induction step

opaque
  unfolding π

封印だけでは定義が隠れてしまうため、第二のブロックは π の展開を明示的に許し、計算規則を記録する。π x が、再帰呼び出しを π y とした step x の提示する集合とパスで等しい、というものである。この規則は同じ再帰原理の伴う定理 ∈-induction-compute がそのまま供給するので、新たな証明は要らない。以後の節では定義を展開する代わりに、このパスに沿って所属の証明を輸送する。

  π-compute : (x : S) → π x ≡ step x (λ y _ → π y)
  π-compute = ∈-induction-compute step

π の最初の性質はその要素を特徴づける。z が π x に属するなら、台のある要素の崩壊が z に等しいことが単に存在する。この主張は切り詰められている。そのような要素を選ぶのではなく、そのような組の型が住まれていることだけを示すのである。

証明は所属の証拠 z∈ から出発し、π の計算規則に沿って輸送する。π x を sett (Fiber x) ⋯ に書き換えると、提示された集合の所属の型からインデックスを読み取れる。インデックスの組 p と、名指しされた要素の π の値が z に等しいというパスである。こうして計算規則は抽象的な所属を具体的な再帰のデータへ変える。

π-member : (x z : S) → ⟨ z ∈ˢ π x ⟩
         → ∥ Σ[ y ∶ S ] (⟨ y ∈ˢ X ⟩ × (π y ≡ z)) ∥₁
π-member x z z∈ = map₁ mk (subst (λ w → ⟨ z ∈ˢ w ⟩) (π-compute x) z∈)
  where
  mk : Σ[ p ∶ Fiber x ] (π (⟪ x ⟫↪ (p .fst)) ≡ z)

補助関数 mk はこの再帰データを約束された形に作り替える。証拠 ⟪ x ⟫↪ (p .fst) はインデックスの組が名指す x の要素そのものである。第二成分 ∈∈ₛ ⋯ .snd はインデックスの組の台への所属の証拠を本来の所属から小所属へ変換し、パス q はそのまま再利用する。結果は map₁ で構成される切り詰められた組であり、各成分が明示的でも、結論はあくまで存在の主張のままである。

     → Σ[ y ∶ S ] (⟨ y ∈ˢ X ⟩ × (π y ≡ z))
  mk (p , q) = ⟪ x ⟫↪ (p .fst)
             , ( ∈∈ₛ {a = ⟪ x ⟫↪ (p .fst)} {b = X} .snd (p .snd)
               , q )

推移的な像

台の上での崩壊の像は、それ自身ひとつの集合であるべきである。πX は X のインデックス型で提示して定義する。その要素は台の要素の崩壊値 π (⟪ X ⟫↪ m) である。この節では、任意の崩壊値の要素が再び台の要素の崩壊である、すなわち π-member の内容だけを使って、πX が推移的であることを示す。

集合 πX は π を X に制限した像であり、台そのものの提示のインデックス型 ⟪ X ⟫ の上に sett で構成される。その要素に関する補題はこの提示をそのまま読んだものである。πX の要素は、X のある y に対する π y が単に存在することを述べる。証明はインデックス m をほどき、パス π (⟪ X ⟫↪ m) ≡ z と、提示の忠実性が与える所属の証拠 member X m を組み立て直すだけである。

πX : S
πX = sett ⟪ X ⟫ (λ m → π (⟪ X ⟫↪ m))

πX-member : (z : S) → ⟨ z ∈ˢ πX ⟩
          → ∥ Σ[ y ∶ S ] (⟨ y ∈ˢ X ⟩ × (π y ≡ z)) ∥₁
πX-member z z∈ = map₁ mk z∈

逆の導入は、πX が持つべき崩壊値をすべて含むことを述べる。y が X の要素なら π y は πX の要素である。ここで提示の章の補題 fiber が決定的である。所属の証拠 y∈X は実際のインデックス m とパス ⟪ X ⟫↪ m ≡ y を与え、そのパスに cong π を施すことで π y がインデックス m における崩壊値として現れる。π-member と違ってこの向きの入力は切り詰められておらず、提示された集合への所属が切り詰められているため出力だけが ∥_∥₁ に包まれる。

  where
  mk : Σ[ m ∶ ⟪ X ⟫ ] (π (⟪ X ⟫↪ m) ≡ z)
     → Σ[ y ∶ S ] (⟨ y ∈ˢ X ⟩ × (π y ≡ z))
  mk (m , q) = ⟪ X ⟫↪ m , ( member X m , q )

πX-intro : (y : S) → ⟨ y ∈ˢ X ⟩ → ⟨ π y ∈ˢ πX ⟩

πX の推移性は isTrans が要求する形を取る。y が x の要素であり x が像に属するなら、y も像に属する。証明は切り詰められた仮定 x∈πX を rec₁ で消去する。目標の ⟨ y ∈ˢ πX ⟩ が命題であるため、これは正当である。π z ≡ x かつ z ∈ X を満たす各証拠 z は、問題を y ∈ π z の証明に帰着させる。

πX-intro y y∈X = ∣ fiber X y∈X .fst , cong π (fiber X y∈X .snd) ∣₁

πX-trans : isTrans πX
πX-trans {x} {y} y∈x x∈πX = rec₁ ((y ∈ˢ πX) .snd) go (πX-member x x∈πX)
  where
  go : Σ[ z ∶ S ] (⟨ z ∈ˢ X ⟩ × (π z ≡ x)) → ⟨ y ∈ˢ πX ⟩

内側のステップでは、まず y∈x をパス π z ≡ x に沿って輸送して y ∈ᵗ π z を得て、次に π-member を適用して、y が X のある w の崩壊として単に存在することを示す。古典的な描像との非対称に注意してほしい。この推移性の証明は y についての帰納を必要としない。提示された集合 π z への所属が、崩壊のデータをすでに直接明け渡すからである。

  go (z , z∈X , pzx) = rec₁ ((y ∈ˢ πX) .snd) go₂ (π-member z y y∈πz)
    where
    y∈πz : y ∈ᵗ π z
    y∈πz = subst (λ w → y ∈ᵗ w) (sym pzx) y∈x
    go₂ : Σ[ w ∶ S ] (⟨ w ∈ˢ X ⟩ × (π w ≡ y)) → ⟨ y ∈ˢ πX ⟩

最後に go₂ は、求める所属をパス π w ≡ y に沿って輸送する。w は X に属するので πX-intro が ⟨ π w ∈ˢ πX ⟩ を与え、このパスが π w と y を同一視する。これで πX-trans が完成し、崩壊の像は真の推移的集合になる。

    go₂ (w , w∈X , pwy) = subst (λ v → ⟨ v ∈ˢ πX ⟩) pwy (πX-intro w w∈X)

順方向の補題は、台の要素の間の所属が崩壊によってどう保たれるかを記録する。y が x の要素であり、両者が台 X に属するなら、π y は小関係において π x の要素である。この補題は同型証明の主力であり、単射性の証明に現れる両方の包含がこれに帰着する。切り詰められた π-member と違い、所属 y ∈ᵗ x そのものが証拠を名指すため、ここではすべてのデータが明示的である。

最初の材料は、所属の証明から復元した、提示写像の y 上のファイバーの要素である。fiber x を yx : y ∈ᵗ x に適用すると、x の提示における実際のインデックス m と、パス ⟪ x ⟫↪ m ≡ y が得られる。これは πX-intro に証拠を与えたのと同じ明示的構成の補題である。埋め込みのファイバーが命題値なので、切り詰められた所属をこの組の型へ消去できる。

π∈-fwd : (x y : S) → y ∈ᵗ x → y ∈ᵗ X → ⟨ π y ∈ˢ π x ⟩
π∈-fwd x y yx yu = subst (λ w → ⟨ π y ∈ˢ w ⟩) (sym (π-compute x)) wit
  where
  fib : Σ[ m ∶ ⟪ x ⟫ ] (⟪ x ⟫↪ m ≡ y)
  fib = fiber x yx

台への所属 yu は y についての主張であるが、組は ⟪ x ⟫↪ m から組み立てられるので、証明はパス p に沿って yu を逆に輸送して ⟪ x ⟫↪ m ∈ˢ X を得る。さらに ∈∈ₛ の順方向の半分で、この本来の小所属の証拠を小関係の所属へ変換する。二つの所属が直接出会うのはこの一点だけで、∈∈ₛ がまさにその橋である。

  m : ⟪ x ⟫
  m = fib .fst
  p : ⟪ x ⟫↪ m ≡ y
  p = fib .snd
  sm : ⟨ ⟪ x ⟫↪ m ∈ₛ X ⟩

組 (m , sm) が Fiber x を住むようになると、証拠 wit は π y を step x の提示する集合の要素として示す。インデックスはこの組そのものであり、パス成分は cong π p で、π (⟪ x ⟫↪ m) を π y と同一視する。π x の計算規則に沿って輸送すれば、この所属は π x 自身の下に置かれ、順方向の補題が完成する。

  sm = ∈∈ₛ {a = ⟪ x ⟫↪ m} {b = X} .fst (subst (λ w → ⟨ w ∈ˢ X ⟩) (sym p) yu)
  wit : ⟨ π y ∈ˢ sett (Fiber x) (λ q → π (⟪ x ⟫↪ (q .fst))) ⟩
  wit = ∣ (m , sm) , cong π p ∣₁

外延性と崩壊同型

推移的な像が整ったところで、残る問いは、台が崩壊によって融合せずに済むかどうかである。この節では台の構造外延性 isExt X を仮定し、π が X 上で単射であること、したがって台の要素間の所属が崩壊値の間の所属と双方向に一致することを示す。鍵となるのは復元の補題である。⟨ π z ∈ˢ π x ⟩ と比較の原理から z ∈ᵗ x を再構成する。ここで使われるのは外延性だけで、台の推移性は不要である。推移性の議論が供給するはずだった所属は、すでにインデックスの組あるいは isExt X の内部の量化によって担われているからである。

復元の補題は二つの入力を取る。第一は切り詰められた主張 ⟨ π z ∈ˢ π x ⟩、第二は比較の原理 same で、x ∩ X に属し π b ≡ π z を満たす任意の b が z と等しいと述べる。目標の z ∈ᵗ x は命題なので、rec₁ による切り詰めの消去は正当である。仮定を π x の計算規則に沿って輸送すると、それは step x の提示する集合への所属になり、その要素は Fiber x で添字づけられる。

private
  π∈-recover : (x z : S) → ⟨ π z ∈ˢ π x ⟩
             → ((b : S) → b ∈ᵗ x → b ∈ᵗ X → π b ≡ π z → b ≡ z)
             → z ∈ᵗ x
  π∈-recover x z h same = rec₁ ((z ∈ˢ x) .snd)

x の要素として b = ⟪ x ⟫↪ (p .fst) を名指すインデックスの組 p と崩壊のパス π b ≡ π z が与えられると、比較の原理が発動する。その仮定は直接満たされる。member x (p .fst) が b ∈ᵗ x を証明し、∈∈ₛ の第二成分がインデックスの組の台への所属の証拠を b ∈ᵗ X に変換する。結論の b ≡ z は所属の証拠 b ∈ᵗ x を z ∈ᵗ x へと輸送し、これがまさに目標である。

    (λ { (p , q) → subst (λ w → ⟨ w ∈ˢ x ⟩)
      (same (⟪ x ⟫↪ (p .fst)) (member x (p .fst))
        (∈∈ₛ {a = ⟪ x ⟫↪ (p .fst)} {b = X} .snd (p .snd)) q)
      (member x (p .fst)) })
    (subst (λ w → ⟨ π z ∈ˢ w ⟩) (π-compute x) h)

外延性に依存する材料は、Xext : isExt X を引数とするモジュールの中に置かれ、仮定が明示され、他の場所で黙って使えることはない。その内部では、帰納の述語 P が台を基準にした単射性の主張そのものである。X に属する x に対し、同じ崩壊値を持つ X の任意の y がパスによって x と等しい、というものである。これが、所属帰納が x のすべての要素に対して同時に確立すべき性質である。

module InjExt (Xext : isExt X) where

P : S → Type (ℓ-suc ℓ)
P x = (y : S) → x ∈ᵗ X → y ∈ᵗ X → π x ≡ π y → x ≡ y

in⊆ : (x y z : S) → x ∈ᵗ X → y ∈ᵗ X → z ∈ᵗ x → z ∈ᵗ X
    → π x ≡ π y
    → ((a : S) → a ∈ᵗ x → P a)
    → ⟨ z ∈ˢ y ⟩
in⊆ x y z xu yu zx zu e IH = π∈-recover y z

  (subst (λ w → ⟨ π z ∈ˢ w ⟩) e (π∈-fwd x z zx zu))
  (λ b by bu q → sym (IH z zx b zu bu (sym q)))

out⊆ : (x y z : S) → x ∈ᵗ X → y ∈ᵗ X → z ∈ᵗ y → z ∈ᵗ X
     → π y ≡ π x
     → ((a : S) → a ∈ᵗ x → P a)
     → ⟨ z ∈ˢ x ⟩
out⊆ x y z xu yu zy zu e IH = π∈-recover x z

  (subst (λ w → ⟨ π z ∈ˢ w ⟩) e (π∈-fwd y z zy zu))
  (λ b bx bu q → IH b bx z bu zu q)

step-inj : (x : S) → ((a : S) → a ∈ᵗ x → P a) → P x
step-inj x IH y xu yu e = Xext x y xu yu to from
  where

  to : (z : S) → z ∈ᵗ X → ⟨ z ∈ˢ x ⟩ → ⟨ z ∈ˢ y ⟩
  to z zu zx = in⊆ x y z xu yu zx zu e IH
  from : (z : S) → z ∈ᵗ X → ⟨ z ∈ˢ y ⟩ → ⟨ z ∈ˢ x ⟩
  from z zu zy = out⊆ x y z xu yu zy zu (sym e) IH

π-inj : (x y : S) → x ∈ᵗ X → y ∈ᵗ X → π x ≡ π y → x ≡ y
π-inj = ∈-induction step-inj

π∈-bwd : (x y : S) → x ∈ᵗ X → y ∈ᵗ X → ⟨ π y ∈ˢ π x ⟩ → y ∈ᵗ x
π∈-bwd x y xu yu h = π∈-recover x y h
  (λ b bx bu q → π-inj b y bu yu q)

iso : (x y : S) → x ∈ᵗ X → y ∈ᵗ X
    → (⟨ y ∈ˢ x ⟩ → ⟨ π y ∈ˢ π x ⟩) × (⟨ π y ∈ˢ π x ⟩ → ⟨ y ∈ˢ x ⟩)
iso x y xu yu = (λ yx → π∈-fwd x y yx yu) , π∈-bwd x y xu yu

再帰等式 π x ≡ step x (λ y _ → π y) は、∈-induction が構成した特定の関数の性質にとどまらず、パスの意味で崩壊を特徴づける。同じ再帰等式を、再帰呼び出しでも f 自身を用いて満たす任意の関数 f は、π とどこでも一致する。この一意性により、崩壊は構成の多数の出力のひとつではなく、well-defined な対象になる。

主張は、計算規則 h : f x ≡ sett (Fiber x) (λ p → f (⟪ x ⟫↪ (p .fst))) を備えたすべての f : S → S を量化する。その形に注意してほしい。π 自身の法則と同じく、右辺は x のフィルタリングされた要素の f 像を要素とする集合を提示する。結論はパスの族 π x ≡ f x であり、x の要素での等式が分かれば x での等式が定まるため、∈ 帰納で証明される。

unique : (f : S → S)
       → ((x : S) → f x ≡ sett (Fiber x) (λ p → f (⟪ x ⟫↪ (p .fst))))
       → (x : S) → π x ≡ f x
unique f h = ∈-induction stepU
  where

帰納ステップは三つのパスを連結する。π-compute x から出発すると、左辺は再帰呼び出しに π を使う step x の提示する集合になる。途中のパス step-eq は再帰呼び出しを π から f へ替え、sym (h x) が f x を展開する。合成のパスは帰納法の仮定だけから π x ≡ f x を示す。

  stepU : (x : S) → ((y : S) → y ∈ᵗ x → π y ≡ f y) → π x ≡ f x
  stepU x IH = π-compute x ∙ step-eq ∙ sym (h x)
    where
    step-eq : sett (Fiber x) (λ p → π (⟪ x ⟫↪ (p .fst)))
            ≡ sett (Fiber x) (λ p → f (⟪ x ⟫↪ (p .fst)))

途中のパスそのものは、提示する関数への同一性 (congruence) の適用である。sett を固定したまま、インデックス関数を λ p → π (⋯) から λ p → f (⋯) へ替え、funExt がこの二つの関数の各点での等しさを供給する。各点は帰納法の仮定の具体例であり、インデックスの組 p が名指す要素に適用され、所属の証拠 member x (p .fst) が再帰呼び出しを正当化する。これは整礎再帰による定義の標準的な一意性の議論を、集合を提示する構成子に合わせたものである。

    step-eq = cong (sett (Fiber x)) (funExt ih')
      where
      ih' : (p : Fiber x) → π (⟪ x ⟫↪ (p .fst)) ≡ f (⟪ x ⟫↪ (p .fst))
      ih' p = IH (⟪ x ⟫↪ (p .fst)) (member x (p .fst))

崩壊はいつ何も変えないのであろうか。Y が台の推移的な部分集合、つまり Y の要素の要素が再び Y に属するなら、崩壊を定めるフィルタは Y の要素の上で完全であり、何も捨てられない。したがって各 y ∈ᵗ Y に対して π y ≡ y が成り立つ。この不動点の主張は y についての ∈ 帰納で証明され、π y と y の比較には階層自身の外延性の原理を使う。

主張は台の側の二つのデータを組み合わせる。小関係における包含 ⟨ Y ⊆ X ⟩ と、推移性 isTrans Y、すなわち Y の要素の要素についての閉性である。帰納法の仮定は両方の所属を見える形で述べる。y の要素のうち Y にも属する m に対してのみ π m ≡ m を主張しており、証明で出会う状況にちょうど合致する。

fixes : (Y : S) → ⟨ Y ⊆ X ⟩ → isTrans Y → (y : S) → y ∈ᵗ Y → π y ≡ y
fixes Y YX Ytr = ∈-induction stepF
  where
  stepF : (y : S) → ((m : S) → m ∈ᵗ y → m ∈ᵗ Y → π m ≡ m)
        → y ∈ᵗ Y → π y ≡ y

ステップは extensionalV、すなわち階層そのものの外延性の原理によって二つの集合を比較する。要素が同じなら集合は等しいというもので、ここでは双条件から作られるパスの族として定式化されている。向き to は、崩壊された集合の要素がすでに y の要素であることを示し、まず切り詰められた所属 xπ を計算規則に沿って輸送してから消去し、Fiber y のインデックスの組と、名指しされた要素の π 値が x に等しいパスを取り出す。

  stepF y IH yY = extensionalV (λ x → ⇔toPath (to x) (from x))
    where
    to : (x : S) → ⟨ x ∈ˢ π y ⟩ → x ∈ᵗ y
    to x xπ = rec₁ ((x ∈ˢ y) .snd) go
      (subst (λ w → ⟨ x ∈ˢ w ⟩) (π-compute y) xπ)

そのようなインデックスの組が与えられると、名指しされた要素 ⟪ y ⟫↪ (p .fst) は y の要素であり、推移性により Y にも属するので、帰納法の仮定が適用されてそれを固定する。つまりその π 値はそれ自身と等しい。この不動点のパスの対称と崩壊のパス q を合成すれば、名指しされた要素から x へのパスが得られ、所属の証拠をそれに沿って輸送すれば x ∈ᵗ y に着地する。

      where
      go : Σ[ p ∶ Fiber y ] (π (⟪ y ⟫↪ (p .fst)) ≡ x) → x ∈ᵗ y
      go (p , q) = subst (λ w → ⟨ w ∈ˢ y ⟩) (sym ih' ∙ q) (member y (p .fst))
        where
        ih' : π (⟪ y ⟫↪ (p .fst)) ≡ ⟪ y ⟫↪ (p .fst)

向き from は、y のすべての要素が崩壊を生き延びることを示す。まず Y の推移性を使って x 自身が Y に属することを確認し、次に帰納法の仮定からパス π x ≡ x が得られる。順方向の補題の結論 ⟨ π x ∈ˢ π y ⟩ をこのパスに沿って輸送すれば、所属は x 自身の場所に移り、⟨ x ∈ˢ π y ⟩ が得られる。

        ih' = IH (⟪ y ⟫↪ (p .fst)) (member y (p .fst))
          (Ytr {x = y} {y = ⟪ y ⟫↪ (p .fst)} (member y (p .fst)) yY)

    from : (x : S) → x ∈ᵗ y → ⟨ x ∈ˢ π y ⟩
    from x xy = subst (λ w → ⟨ w ∈ˢ π y ⟩) (IH x xy x∈Y)
      (π∈-fwd y x xy x∈X)

二つの補助的事実は互いに鏡像である。x の Y への所属は、推移性を x ∈ᵗ y と y ∈ᵗ Y に適用して得られる。そこから台 X への所属は、小さな二段階で従う。∈∈ₛ の逆向きの半分が x ∈ᵗ Y を小所属の主張に変え、仮定 YX がその主張を包含に沿って X へ運び、∈∈ₛ の順方向の半分が通常の所属の証明に戻す。

      where
      x∈Y : x ∈ᵗ Y
      x∈Y = Ytr {x = y} {y = x} xy yY
      x∈X : x ∈ᵗ X
      x∈X = ∈∈ₛ {a = x} {b = X} .snd

両方向が確立されれば、⇔toPath が各 x での双条件をパスに変換し、extensionalV が得られたパスの族を π y ≡ y へと組み立てる。y は Y の任意の要素だったので、崩壊は Y を各点で固定し、帰納が閉じる。

        (YX x (∈∈ₛ {a = x} {b = Y} .fst x∈Y))