符号化された単射

private
  Holds₀ : S → S → Type (ℓ-suc ℓ)
  Holds₀ x y = ⟨ pr (x .fst) (y .fst) ∈ (lookup f γ) .fst ⟩

  at₁ : (y x x' : S)

パス at₁ は、拡張された割り当て x' ∷ x ∷ y ∷ γ での最初の適用条項の妥当性を記録する。そこでの充足は、対 (x, y) のグラフへの所属という射影された事実と同一視される。この同一視は命題どうしの等しさであり、所定の変数の添字での appAt-adequate によって与えられるので、どちらの方向へも輸送できる。

      → ((x' ∷ x ∷ y ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc zero) (suc (suc zero)))
      ≡ (pr (x .fst) (y .fst) ∈ (lookup f γ) .fst)
  at₁ y x x' = appAt-adequate (suc (suc (suc f))) (suc zero) (suc (suc zero))
                 (x' ∷ x ∷ y ∷ γ)

  at₂ : (y x x' : S)

パス at₂ はもう一つの条項についての同じ主張である。変数 0 と 2 での適用の充足は、対 (x', y) のグラフへの所属という射影された事実と等しくなる。二つのパスの違いは、対の符号にどちらの第一成分を入れるかだけで、これこそ単射性が利用する非対称である。

      → ((x' ∷ x ∷ y ∷ γ) ⊨ appAt (suc (suc (suc f))) zero (suc (suc zero)))
      ≡ (pr (x' .fst) (y .fst) ∈ (lookup f γ) .fst)
  at₂ y x x' = appAt-adequate (suc (suc (suc f))) zero (suc (suc zero))
                 (x' ∷ x ∷ y ∷ γ)

injAt-out : ⟨ γ ⊨ injAt f ⟩

外向きの injAt-out は、論理式が γ で成り立つ証明と二つの所属の事実 Holds₀ x y、Holds₀ x' y から出発する。三つの量化子を具体化すると、拡張された割り当てでの含意の本体の充足証明が得られ、所属の事実を at₁ と at₂ の逆向きに輸送して、二つの前件の条項の充足証明に変える。最後の x .fst ≡ x' .fst はモデルの等しさの中で読み取る。

          → (y x x' : S) → Holds₀ x y → Holds₀ x' y → x .fst ≡ x' .fst
injAt-out h y x x' p q = h y x x'
  (subst ⟨_⟩ (sym (at₁ y x x')) p) (subst ⟨_⟩ (sym (at₂ y x x')) q)

injAt-in : ((y x x' : S) → Holds₀ x y → Holds₀ x' y → x .fst ≡ x' .fst)
         → ⟨ γ ⊨ injAt f ⟩

内向きの injAt-in は同じ輸送を順方向に行う。Holds₀ についての射影された単射性を仮定として与えると、二つの所属の事実を at₁ と at₂ そのものに沿って輸送して二つの前件の充足を得、仮定が論理式の結論の求める等しさを出す。二つの方向を合わせて、この論理式が単射性に対して過不足なく妥当であることが分かる。

injAt-in h y x x' p q = h y x x'
  (subst ⟨_⟩ (at₁ y x x') p) (subst ⟨_⟩ (at₂ y x x') q)

γ : Vec S 
γ = F ∷ D ∷ []

Holds x y は、底の対が底のグラフに属すという射影された所属である。ファイバー Fib x は出力 y にこの証明を添えた組で、その要素はグラフが x で取る候補の値であり、それぞれが本当に値であることの証明書を伴う。

Holds : S → S → Type (ℓ-suc ℓ)
Holds x y = ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩

Fib : S → Type (ℓ-suc ℓ)
Fib x = Σ[ y ∶ S ] Holds x y

isPropFib : (x : S) → isProp (Fib x)

Fib x が命題であることを示すには、(y,p) と (y′,q) を比較する。一価性からまずパス y .fst ≡ y′ .fst が得られる。内側の Σ≡Prop は、S の要素の第二成分である isL の証明が命題であることを使い、このパスを y ≡ y′ へ持ち上げる。外側の Σ≡Prop は、グラフ所属の証明が命題であることを使い、その等しさを Fib x の二要素の等しさへ持ち上げる。これは別々の二つの証明無関係性の段階であり、周囲の集合の等しさが構成可能性だけから従うという意味ではない。

isPropFib x (y , p) (y' , q) =
  Σ≡Prop (λ w → (pr (x .fst) (w .fst) ∈ F .fst) .snd)
    (Σ≡Prop (λ z → (isL z) .snd) (svAt-out zero γ sv x y y' p q))

toVal : (x : S) → ∥ Fib x ∥₁ → Fib x
toVal x = rec₁ (isPropFib x) (λ z → z)

Fib x が命題なので、toVal は値の切り詰められた存在 ∥ Fib x ∥₁ を実際のファイバーへ消去できる。選択がここに隠れていそうで、そうではない。命題の切り詰めは命題値の任意の対象へ消去できるので、排中律も代表的な元の選出も要らない。定義域 Dom は入力に D への所属の射影された証明を添えてまとめ、fib は domAt-in から得た各入力の切り詰められた像を toVal に通す。

Dom : Type (ℓ-suc ℓ)
Dom = Σ[ x ∶ S ] ⟨ x .fst ∈ D .fst ⟩

fib : (u : Dom) → Fib (u .fst)
fib (x , m) = toVal x (domAt-in zero (suc zero) γ dm x m)

toFun : Dom → S

関数 toFun は定義域の要素を、その一意なファイバーに含まれる出力 y : S へ送る。捨てるのは付随するグラフ所属の証明だけで、出力はモデルの要素のままなので構成可能性の証明書を保持する。定理 toFun-graph は、捨てた所属の証拠をファイバーの第二成分として取り出す。

toFun u = (fib u) .fst

toFun-graph : (u : Dom) → Holds (u .fst) (toFun u)
toFun-graph u = (fib u) .snd

module _ (ij : ⟨ γ ⊨ injAt zero ⟩) where

toFun-inj : (u v : Dom) → (toFun u) .fst ≡ (toFun v) .fst

          → (u .fst) .fst ≡ (v .fst) .fst
toFun-inj u v e = injAt-out zero γ ij (toFun v) (u .fst) (v .fst)
  (subst (λ w → ⟨ pr ((u .fst) .fst) w ∈ F .fst ⟩) e (toFun-graph u))
  (toFun-graph v)

内側のモジュールは、F と D と先の二つの充足の証明で Extract を改めて開くので、前節の構成はすべて接頭辞付きの名前で使える。そして toS は D の標準的な提示のインデックス m を模型の要素に変える。第一成分は提示された集合そのものであり、第二成分はその構成可能性の証明書で、isL-trans により、明示的な所属 member (D .fst) m と D 自身が構成可能である証明書から得られる。推移性はまさに必要な原理である。構成可能集合の要素は構成可能である。

module E = Extract F D sv dm

toS : ⟪ D .fst ⟫ → S
toS m = ⟪ D .fst ⟫↪ m
      , isL-trans {x = D .fst} {y = ⟪ D .fst ⟫↪ m} (member (D .fst) m) (D .snd)

各小さなインデックスは、Extract の意味でも定義域の要素と見なされねばならず、at がその組を与える。模型の要素 toS m と明示的な所属の証明 member (D .fst) m である。at m を E.toFun でグラフに通すと値が得られ、値域の仮定がこの値が C に属すことを証明する。標準的な提示での所属 ⟪ C .fst ⟫↪ k ≡ (E.toFun (at m)) .fst は、命題値のファイバーを持つ埋め込みのファイバーなので、fiber は切り詰められた存在ではなく、実際のインデックス k とパスの組を返す。

at : ⟪ D .fst ⟫ → E.Dom
at m = toS m , member (D .fst) m

fib : (m : ⟪ D .fst ⟫)
    → Σ[ k ∶ ⟪ C .fst ⟫ ] (⟪ C .fst ⟫↪ k ≡ (E.toFun (at m)) .fst)
fib m = fiber (C .fst)

パスを捨てると small が得られる。D のインデックス型から C のインデックス型への関数で、各定義域のインデックスは、グラフの下での像に対応するインデックスへ送られる。ここで二つの表現が合流する。small は固定された宇宙レベルの型の間の写しであり、数え上げの議論が求める形そのものであり、保持されたパスを通してグラフと結び付いている。

  (ran (toS m) (E.toFun (at m)) (E.toFun-graph (at m)))

small : ⟪ D .fst ⟫ → ⟪ C .fst ⟫
small m = (fib m) .fst

small-inj : (m n : ⟪ D .fst ⟫) → small m ≡ small n → m ≡ n
small-inj m n e = ↪-inj {a = D .fst} {m = m} {n = n}

small の単射性は、インデックスの等しさを提示の中を通して辿ることで証明される。small m ≡ small n から、(fib m) .snd を逆向きにたどって m での提示された値を得、埋め込みの下での合同が等しさを運び、(fib n) .snd が n での提示された値に着く。三つのパスを正にこの方向でつなぐことで、二つの値の底の集合が等しくなる。続いて Extract の単射性が二つの入力の底の集合の等しさを与え、↪-inj、すなわち定義域の提示の埋め込みのインデックス上の単射性が m ≡ n を結論する。ここでは二つの異なる単射性の事実が働いており、一つはグラフについて、もう一つは標準的な埋め込みについてで、どちらも他方で代用できない。

  (E.toFun-inj ij (at m) (at n)
    (sym ((fib m) .snd) ∙ cong ⟪ C .fst ⟫↪ e ∙ (fib n) .snd))