任意の L 基数より大きい順序数 L 基数

module Col (w : WFR) where

このような関係 w を一つ固定する。第一成分はブール関係 R であり、残りの成分が推移性と整礎性を保証する。崩壊の議論ではこれらの役割を分ける。関係が所属を定め、証明が再帰の正当性と順序数の推移性を与えるからである。

R : Rel
R = w .fst

崩壊の側では、関係は、ブールが成立することを持ち上げた形で読まれる。これで、Mostowski の展開が期待するレベルに合うのである。

_≺_ : ⟪ a ⟫ → ⟪ a ⟫ → Type ℓ
x ≺ y = Lift (Holds R x y)

持ち上げた関係は、もとの Bool 値関係から推移性を受け継ぐ。二つの仮定をいったん下ろすと、w に収められた推移性で合成できるブール等式が得られ、その結果を再び持ち上げれば、崩壊が要求する宇宙レベルに戻る。

≺-trans : {x y z : ⟪ a ⟫} → x ≺ y → y ≺ z → x ≺ z
≺-trans p q = lift ((w .snd) .fst (lower p) (lower q))

同じ宇宙レベルの変更によって整礎性も保たれる。go は Bool 値関係の到達可能性の木から出発し、各前者の辺を持ち上げた辺に再帰的に置き換えて、_≺_ の到達可能性の木を作る。

≺-wf : WellFounded _≺_
≺-wf x = go x ((w .snd) .snd x)
  where
  go : (y : ⟪ a ⟫) → Acc (λ u v → Holds R u v) y → Acc _≺_ y
  go y (acc h) = acc (λ z k → go z (h z (lower k)))

持ち上げた関係は、Mostowski の構成に必要な二つの仮定、すなわち推移性と整礎性を満たした。そこで、その崩壊 col を使える。付随する法則は各崩壊値の所属を記述し、すべての崩壊値が順序数であることを示す。

open Mostowski ⟪ a ⟫ _≺_ ≺-wf ≺-trans public
  using ( col; col-eq; col-in; col-out; col-ord )

すべての崩壊値を像 ot として集める。この名前は順序型を思わせるが、WFR の任意の要素が整列順序であるとは限らず、ここでは一意性や同型に関する定理も主張しない。必要なのは、この像が順序数であることだけである。

ot : SV.S
ot = sett ⟪ a ⟫ col

各 col p はこの像に属する。ここで与える証人は添字 p と反射律であり、像への所属は逆像が存在することだけを残すため、命題的切り詰めで包まれている。

ot-in : (p : ⟪ a ⟫) → ⟨ col p ∈ˢ ot ⟩
ot-in p = ∣ p , refl ∣₁

この像は順序数である。まず、像の要素はある崩壊値と単に等しく、その崩壊値が順序数なので、その要素は推移的である。次に、像そのものも推移的である。y ∈ x で、x が col p によって表されるなら、col-out は y をある前者 r の col r として命題的切り詰めのもとで提示する。そこで r に対する正準な像の証人から y ∈ ot が得られる。二つの切り詰められた存在はいずれも、命題値の所属または推移性の目標にだけ除去される。

ot-ord : IsOrd ot
ot-ord = tr , mem
  where
  mem : (x : SV.S) → ⟨ x ∈ˢ ot ⟩ → isTransV x
  mem x x∈ = rec₁ (isPropIsTransV x)

要素の推移性は、崩壊の順序数性から、提示の等式に沿って運ばれ、外側の消去が、像の中のその要素の切り詰められた分解を消費する。

    (λ z → subst isTransV (z .snd) (col-ord (z .fst) .fst)) x∈
  tr : isTransV ot
  tr {x} {y} y∈x x∈ot = rec₁ ((y ∈ˢ ot) .snd) outer x∈ot
    where
    outer : Σ[ p ∶ ⟪ a ⟫ ] (col p ≡ x) → ⟨ y ∈ˢ ot ⟩

切り詰められた分解から、崩壊が y であり、かつ p に先行する添字 r が得られる。崩壊の法則は col r を col p に入れ、正準な像の証人 ot-in r は col r を ot に入れる。したがって、等式 col r ≡ y に沿って運べば y ∈ ot が得られる。

    outer (p , e) =
      rec₁ ((y ∈ˢ ot) .snd)
        (λ z → subst (λ v → ⟨ v ∈ˢ ot ⟩) ((z .snd) .snd) (ot-in (z .fst)))
        (col-out p y (subst (λ v → ⟨ y ∈ˢ v ⟩) (sym e) y∈x))

module NoInj (f : ⟪ μ ⟫ ↪ ⟪ a ⟫) where

埋め込みの基礎となる関数が、以降の構成のために一度だけ名づけられる。

F : ⟪ μ ⟫ → ⟪ a ⟫
F = f .fst

源も目標も h-集合なので、単射な関数は埋め込みである。それぞれのファイバーは命題である。

F-emb : isEmbedding F
F-emb = injEmbedding (isSet⟪⟫ a) (λ {x} {y} e → f .snd x y e)

ある点上のファイバーは、μ の要素の添字と、F がその添字をその点へ写すことを示す等式からなる。したがって、Fib x の要素は、x が F の像に属することの提示にほかならない。

Fib : ⟪ a ⟫ → Type ℓ
Fib x = Σ[ m ∶ ⟪ μ ⟫ ] (F m ≡ x)

F の各ファイバーは命題である。したがって、二つの引き戻し関係の証明が同じ像の点を異なるかもしれない添字で提示しても、それらのファイバー要素は等しくなる。この一意性は代表を揃えるために使われ、像の外の点に代表を選ぶものではない。

isPropFib : (x : ⟪ a ⟫) → isProp (Fib x)
isPropFib = isEmbedding→hasPropFibers F-emb

関係 PreT x y はまず、x と y がともに F の像にあることを示す実際のファイバーを要求する。そのうえで、対応する μ の提示要素が小所属関係にあるとき、ちょうどそのときに x が y に先行すると定める。したがって、像の外の点にはこの関係での前者がない。

PreT : ⟪ a ⟫ → ⟪ a ⟫ → Type ℓ
PreT x y = Σ[ p ∶ Fib x ] Σ[ q ∶ Fib y ]
             ⟨ ⟪ μ ⟫↪ (p .fst) ∈ₛ ⟪ μ ⟫↪ (q .fst) ⟩

引き戻された前者の関係は命題である。二つの命題であるファイバーと一つの所属の命題からできている。

isPropPreT : (x y : ⟪ a ⟫) → isProp (PreT x y)
isPropPreT x y = isPropΣ (isPropFib x) λ p →
                 isPropΣ (isPropFib y) λ q →
                   (⟪ μ ⟫↪ (p .fst) ∈ₛ ⟪ μ ⟫↪ (q .fst)) .snd

ブールの関係は、引き戻された前者の関係の、判定可能な符号化である。命題値の関係に排中律を適用することで得られる。

R : Rel
R x y = decB (lemℓ (PreT x y , isPropPreT x y))

ブール関係が成り立つなら、その値は true である。排中律による判定を調べると PreT x y を復元できる。肯定側には求める証明があり、否定側ではブール値が false になるため矛盾する。

R→Pre : (x y : ⟪ a ⟫) → Holds R x y → PreT x y
R→Pre x y e = go (lemℓ (PreT x y , isPropPreT x y)) e
  where
  go : (d : Dec (PreT x y)) → decB d ≡ true → PreT x y
  go (yes h) _ = h

反駁の分岐は不可能である。前の事実が成立しなければ、判定器は false を返し、true の所属と矛盾する。

  go (no _) e' = ⊥₀-rec (false≢true e')

後ろ向きの読み出しは、同じ古典的な判定によって、引き戻された前者の事実からブールの所属を作る。

Pre→R : (x y : ⟪ a ⟫) → PreT x y → Holds R x y
Pre→R x y h = go (lemℓ (PreT x y , isPropPreT x y))
  where
  go : (d : Dec (PreT x y)) → decB d ≡ true
  go (yes _) = refl

空の分岐は不可能である。前の事実は仮定によって成立するからである。

  go (no n) = ⊥₀-rec (n h)

推移性を示すため、x R y と y R z を二つの PreT の証人として読み取る。そこには四つのファイバーの証人がある。x 上に一つ、共通の中間点 y 上に二つ、z 上に一つである。y 上のファイバーは命題なので二つの証人は等しく、対応する μ の要素を揃えられる。そこで最後の提示要素の推移性を使って二段階の所属を合成すると、x R z に対する PreT の証人が得られる。

R-trans : {x y z : ⟪ a ⟫} → Holds R x y → Holds R y z → Holds R x z
R-trans {x} {y} {z} e1 e2 = Pre→R x z (p , r , goal)
  where
  d1 : PreT x y
  d1 = R→Pre x y e1

第一の関係を読み取ると、x と y 上の添字 p、q が得られ、第二の関係からは y と z 上の添字 q'、r が得られる。y 上のファイバーが命題であることから q と q' が同一視され、第一の関係が表す所属を、第二の関係と同じ中間の添字を使う形に書き換えられる。

  d2 : PreT y z
  d2 = R→Pre y z e2
  p  = d1 .fst
  q  = (d1 .snd) .fst
  q' = d2 .fst

最後の要素 r が名づけられ、その推移性は μ の順序数性から読まれる。

  r  = (d2 .snd) .fst
  h1' : ⟨ ⟪ μ ⟫↪ (p .fst) ∈ₛ ⟪ μ ⟫↪ (q' .fst) ⟩
  h1' = subst (λ t → ⟨ ⟪ μ ⟫↪ (p .fst) ∈ₛ ⟪ μ ⟫↪ (t .fst) ⟩)
          (isPropFib y q q') ((d1 .snd) .snd)
  rTr : isTransV (⟪ μ ⟫↪ (r .fst))

二つの所属の関係を、r の推移性を通して合成すると、目標が作られる。第一の要素が第三の要素の中にあること、これが引き戻された関係の要求である。

  rTr = μ-ord .snd (⟪ μ ⟫↪ (r .fst)) (member μ (r .fst))
  goal : ⟨ ⟪ μ ⟫↪ (p .fst) ∈ₛ ⟪ μ ⟫↪ (r .fst) ⟩
  goal = ∈∈ₛ {a = ⟪ μ ⟫↪ (p .fst)} {b = ⟪ μ ⟫↪ (r .fst)} .fst
    (rTr (∈∈ₛ {a = ⟪ μ ⟫↪ (p .fst)} {b = ⟪ μ ⟫↪ (q' .fst)} .snd h1')
         (∈∈ₛ {a = ⟪ μ ⟫↪ (q' .fst)} {b = ⟪ μ ⟫↪ (r .fst)} .snd ((d2 .snd) .snd)))

整礎性は、周囲の階層の正則性から、埋め込みに沿って運ばれる。補助の補題は、目標が特定の階層の要素と等しい場合を扱う。

補助の証明は、与えられた要素のそれぞれの前者に対して、アクセス可能性を構成する。

wfAux : (v : SV.S) → Acc SV._∈ᵗ_ v → (m : ⟪ μ ⟫) → ⟪ μ ⟫↪ m ≡ v
      → Acc (λ x y → Holds R x y) (F m)
wfAux v (acc rec) m e = acc go
  where
  go : (r : ⟪ a ⟫) → Holds R r (F m) → Acc (λ x y → Holds R x y) r

要素のそれぞれの前者 r は、引き戻された関係で結ばれた二つの μ の要素に分解され、アクセス可能性は第一の成分へ運ばれる。

  go r rr = subst (Acc (λ x y → Holds R x y)) (p .snd)
              (wfAux (⟪ μ ⟫↪ (p .fst)) (rec (⟪ μ ⟫↪ (p .fst)) below)
                 (p .fst) refl)
    where
    d : PreT r (F m)

前の事実から、p と q が得られる。p は r の μ の中の代表であり、q は F m の μ の中の代表である。

    d = R→Pre r (F m) rr
    p = d .fst
    q = (d .snd) .fst
    h : ⟨ ⟪ μ ⟫↪ (p .fst) ∈ₛ ⟪ μ ⟫↪ m ⟩
    h = subst (λ t → ⟨ ⟪ μ ⟫↪ (p .fst) ∈ₛ ⟪ μ ⟫↪ (t .fst) ⟩)

F m 上の二つのファイバーの証人は、そのファイバーが命題なので等しくなる。この等式に沿って運ぶと、読み取った関係は、p が表す先行要素が m の表す要素に属するという形に書き換えられる。後者を v と同定する等式によって先行要素は v より真に下に置かれ、そこで到達可能性の再帰を適用できる。

          (isPropFib (F m) q (m , refl)) ((d .snd) .snd)
    below : ⟪ μ ⟫↪ (p .fst) SV.∈ᵗ v
    below = subst (λ t → ⟨ ⟪ μ ⟫↪ (p .fst) ∈ˢ t ⟩) e
              (∈∈ₛ {a = ⟪ μ ⟫↪ (p .fst)} {b = ⟪ μ ⟫↪ m} .snd h)

引き戻された関係の整礎性は、周囲の階層の正則性から従う。ある要素のそれぞれの前者は、ある階層の要素より厳密に下にあり、補助の補題がそこでアクセス可能性を作る。

R-wf : WellFounded (λ x y → Holds R x y)
R-wf x = acc go
  where
  go : (r : ⟪ a ⟫) → Holds R r x → Acc (λ u v → Holds R u v) r
  go r rr = subst (Acc (λ u v → Holds R u v)) (p .snd)

x の任意の先行要素 r に対して、関係を読み取ると r 上のファイバーの証人 p が得られる。正則性は、その添字が表す階層の要素の到達可能性を与え、wfAux がその到達可能性を点 F (p .fst) へ移す。ファイバーの等式がこの点を r と同定し、必要な到達可能性の証明が完成する。

              (wfAux (⟪ μ ⟫↪ (p .fst)) (regularityV (⟪ μ ⟫↪ (p .fst)))
                 (p .fst) refl)
    where
    p = (R→Pre r x rr) .fst

整礎で推移的な関係が、その二つの証明とともにまとめられ、上界の順序数がわたる整礎な関係の族が完成する。

w : WFR
w = R , R-trans , R-wf

仮定した単射から得た特定の関係 w に崩壊の構成を適用する。以下では、その崩壊値と像を μ の提示要素と直接比較する。w が整列順序であるという主張は必要ない。

open Col w using ( col; col-in; col-out; ot; ot-in; _≺_ )

重要な補題はこう言う。引き戻された関係の崩壊は、上界の順序数の要素を再現する。階層の要素として提示された μ の各要素について、その像の崩壊はその要素に等しい、と。証明は、階層の要素の上の整礎帰納である。

証明は、二方向で外延性によって要素を比較する。

key : (v : SV.S) → Acc SV._∈ᵗ_ v → (m : ⟪ μ ⟫) → ⟪ μ ⟫↪ m ≡ v
    → col (F m) ≡ ⟪ μ ⟫↪ m
key v (acc rec) m e =
  extensionality (col (F m)) (⟪ μ ⟫↪ m) (fwd , bwd)
  where

まず順方向の包含を示す。b が col (F m) に属するとする。除去則 col-out は、b が F m のある前者 r の崩壊値であることを命題的切り詰めのもとで述べる。その前者を PreT で読み取ると m より下の添字が得られ、帰納の仮定が、その添字の表す要素を col r、したがって b と同一視する。

  fwd : (b : SV.S) → ⟨ b ∈ₛ col (F m) ⟩ → ⟨ b ∈ₛ ⟪ μ ⟫↪ m ⟩
  fwd b b∈ = rec₁ ((b ∈ₛ ⟪ μ ⟫↪ m) .snd) go
               (col-out (F m) b (∈∈ₛ {a = b} {b = col (F m)} .snd b∈))
    where
    go : Σ[ r ∶ ⟪ a ⟫ ] ((r ≺ F m) × (col r ≡ b))

前者の証人は r ≺ F m と等式 col r ≡ b からなる。関係の証明を R→Pre で読み戻すと、r と F m のファイバーが得られる。その添字は対応する μ の提示要素を示し、最後の成分はそれらの間の所属を記録する。

       → ⟨ b ∈ₛ ⟪ μ ⟫↪ m ⟩
    go (r , rr , cr) = subst (λ t → ⟨ t ∈ₛ ⟪ μ ⟫↪ m ⟩) (cpr ∙ cr) hh
      where
      d = R→Pre r (F m) (lower rr)
      p = d .fst

F m 上のファイバーは命題なので、関係の証明から得た代表 q は明らかな代表 (m , refl) と等しくなる。この等式に沿って輸送すると、読み取った所属は、前者の添字が m の表す集合に属すという主張になる。

      q = (d .snd) .fst
      hh : ⟨ ⟪ μ ⟫↪ (p .fst) ∈ₛ ⟪ μ ⟫↪ m ⟩
      hh = subst (λ t → ⟨ ⟪ μ ⟫↪ (p .fst) ∈ₛ ⟪ μ ⟫↪ (t .fst) ⟩)
             (isPropFib (F m) q (m , refl)) ((d .snd) .snd)
      below : ⟪ μ ⟫↪ (p .fst) SV.∈ᵗ v

等式 ⟪ μ ⟫↪ m ≡ v を使うと、この所属は前者の表す集合を周囲の所属における v の下に置く。したがって、その前者で再帰の仮定を使い、その崩壊値を提示された集合と同一視できる。

      below = subst (λ t → ⟨ ⟪ μ ⟫↪ (p .fst) ∈ˢ t ⟩) e
                (∈∈ₛ {a = ⟪ μ ⟫↪ (p .fst)} {b = ⟪ μ ⟫↪ m} .snd hh)
      ih : col (F (p .fst)) ≡ ⟪ μ ⟫↪ (p .fst)
      ih = key (⟪ μ ⟫↪ (p .fst)) (rec (⟪ μ ⟫↪ (p .fst)) below) (p .fst) refl
      cpr : ⟪ μ ⟫↪ (p .fst) ≡ col r

帰納の仮定は、復号された添字の崩壊値を、その添字が表す要素と同一視する。ファイバーの等式はさらに、その添字の像を r と同一視する。そこで col の合同性を使うと、提示要素と col r の間の必要な等式が得られ、これを col r ≡ b と合成すれば順方向の包含が完了する。

      cpr = sym ih ∙ cong col (p .snd)

次に逆方向の包含を示す。b が添字 m の表す集合に属すると仮定し、b ∈ col (F m) を目指す。まず順序数 μ の推移性により b は μ の要素でもあるので、μ の正準な提示から b を表す添字 k が得られる。

  bwd : (b : SV.S) → ⟨ b ∈ₛ ⟪ μ ⟫↪ m ⟩ → ⟨ b ∈ₛ col (F m) ⟩
  bwd b b∈ = ∈∈ₛ {a = b} {b = col (F m)} .fst
               (subst (λ t → ⟨ t ∈ˢ col (F m) ⟩) (ihk ∙ ek) inCol)
    where
    b∈ˢ : ⟨ b ∈ˢ ⟪ μ ⟫↪ m ⟩

ここで fiber μ b∈μ は、実際の添字 k と等式 ⟪ μ ⟫↪ k ≡ b を返す。小所属 _∈ₛ_ が正準な提示の命題値ファイバーに基づくためである。これはその提示に対する局所的な逆操作であり、任意の切り詰められた存在からの選択ではない。

    b∈ˢ = ∈∈ₛ {a = b} {b = ⟪ μ ⟫↪ m} .snd b∈
    b∈μ : ⟨ b ∈ˢ μ ⟩
    b∈μ = μ-ord .fst b∈ˢ (member μ m)
    fb = fiber μ b∈μ
    k = fb .fst

fiber が返す等式により、もとの所属 b ∈ ⟪ μ ⟫↪ m を、提示要素 ⟪ μ ⟫↪ k の所属として書き換えられる。そこで、明らかな二つのファイバー (k , refl)、(m , refl) とこの所属から PreT (F k) (F m) が得られる。

    ek : ⟪ μ ⟫↪ k ≡ b
    ek = fb .snd
    k∈m : ⟨ ⟪ μ ⟫↪ k ∈ₛ ⟪ μ ⟫↪ m ⟩
    k∈m = subst (λ t → ⟨ t ∈ₛ ⟪ μ ⟫↪ m ⟩) (sym ek) b∈
    pre : PreT (F k) (F m)

この PreT の事実を Bool 関係に符号化すると F k ≺ F m が得られる。したがって、崩壊の導入則により col (F k) は col (F m) に属する。同時に、提示要素が m の表す集合に属すことから、それは帰納の引数 v より下にあるので、再帰の仮定を k に適用できる。

    pre = (k , refl) , ((m , refl) , k∈m)
    inCol : ⟨ col (F k) ∈ˢ col (F m) ⟩
    inCol = col-in (F m) (F k) (lift (Pre→R (F k) (F m) pre))
    below : ⟪ μ ⟫↪ k SV.∈ᵗ v
    below = subst (λ t → ⟨ ⟪ μ ⟫↪ k ∈ˢ t ⟩) e

再帰の仮定から col (F k) ≡ ⟪ μ ⟫↪ k が得られる。これをファイバーの等式 ⟪ μ ⟫↪ k ≡ b と合成し、先ほど作った所属を b ∈ col (F m) へ輸送すれば、逆方向の包含が完了する。

              (∈∈ₛ {a = ⟪ μ ⟫↪ k} {b = ⟪ μ ⟫↪ m} .snd k∈m)
    ihk : col (F k) ≡ ⟪ μ ⟫↪ k
    ihk = key (⟪ μ ⟫↪ k) (rec (⟪ μ ⟫↪ k) below) k refl

正則性は、μ の各添字 m で帰納を特殊化するための到達可能性の証明を与える。したがって key' は col (F m) を m が表す要素と同一視する。証明の次の部分で、これらの各点の等式から包含 μ ⊆ Col.ot w を導く。この時点ではまだその包含を主張していない。

key' : (m : ⟪ μ ⟫) → col (F m) ≡ ⟪ μ ⟫↪ m
key' m = key (⟪ μ ⟫↪ m) (regularityV (⟪ μ ⟫↪ m)) m refl

μ の各要素 b は崩壊像 ot にも属する。b における μ の正準なファイバーから、⟪ μ ⟫↪ m ≡ b を満たす添字 m が得られる。補題 key' はこの代表を col (F m) と同定し、ot-in はその崩壊値を ot に入れる。二つの等式に沿って輸送すれば b ∈ ot が得られる。

したがって、ここで示されるのは包含 μ ⊆ ot だけである。これと ot ∈ μ を合わせれば矛盾には十分であり、μ と ot の等しさや順序同型を示す必要はない。

μ⊆ot : (b : SV.S) → ⟨ b ∈ˢ μ ⟩ → ⟨ b ∈ˢ ot ⟩
μ⊆ot b b∈μ =
  subst (λ t → ⟨ t ∈ˢ ot ⟩) (key' (fb .fst) ∙ fb .snd)
    (ot-in (F (fb .fst)))
  where

正準な提示のファイバーは命題なので、b に対して復元される代表は一意に定まる。その代表と等式をまとめて fb として保持することで、直前の包含証明における key' と ot-in の両方に必要な添字が得られる。

  fb = fiber μ b∈μ

上界の構成により、ot は μ の要素である。この要素に包含 μ ⊆ ot を適用すると ot ∈ ot が得られ、所属関係の非反射性に反する。これで、仮定した単射 μ ↪ a から生じる矛盾が完成する。

absurd : ⊥₀
absurd = ∈-irrefl ot (μ⊆ot ot (ot∈μ w))