段階順序の記述の妥当性

private
  β : V ℓ
  β = (lookup b γ) .fst

要素 z は、その底の集合と、それが L に属するという証拠をともに持つ。メタ言語の関数 birth はその証拠を用いて順序数を作るが、証明無関係性により、得られる順序数が構成可能性の証明の選択を符号化することはない。

  z : S
  z = lookup x γ

内側の記録は、候補の段階 c の上の定義可能冪の値 d と、冪の記述の充足、そして引数が d に属することを集める。

  Inner : S → Type (ℓ-suc ℓ)
  Inner c = Σ[ d ∶ S ]
    ( ⟨ (d ∷ c ∷ γ) ⊨ DefAt zero (suc zero) ⟩ × ⟨ z .fst ∈ d .fst ⟩ )

外側の記録はさらに、上げられた添字のもとでの段階のグラフの充足、引数が候補の段階に属さないことの反証、そして内側の記録の切り詰めを加える。三つ合わせて、これこそ誕生の論理式が主張することである。

  Outer : S → Type (ℓ-suc ℓ)
  Outer c = ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩
          × ( (⟨ z .fst ∈ c .fst ⟩ → Lift {j = ℓ-suc ℓ} ⊥₀) × ∥ Inner c ∥₁ )

中心となる意味論的補題は、β が順序数であり、x が 𝒟ₒ (Lset β) に属する一方で Lset β には属さないと仮定する。まさにこの境界の事実から β ≡ birth x を示す。順序数性はこの読みへの入力であり、BirthAt の充足から取り出されるものではない。

  decideBirth : IsOrd β → ⟨ z .fst ∈ 𝒟ₒ (Lset β) ⟩
              → (⟨ z .fst ∈ Lset β ⟩ → ⊥₀)
              → β ≡ birth (z .fst) (z .snd)
  decideBirth ob hin hout = go (ord-tri (sucV β) (suc-ord ob)
                                        (stage (z .fst) (z .snd))

Lset-suc により、𝒟ₒ (Lset β) への所属は Lset (sucV β) への所属に変わる。これは x を含む最初の段階が β の後続より後ではないことを意味するが、さらに早い可能性をすべて排除する必要がある。

                                        (stage-ord (z .fst) (z .snd)))
    where
    mem : ⟨ z .fst ∈ Lset (sucV β) ⟩
    mem = subst (λ u → ⟨ z .fst ∈ u ⟩) (sym (Lset-suc β)) hin

x の最初の段階が sucV β に属すると仮定する。後続順序数への所属は、その段階が β に属する場合と β に等しい場合に分かれる。前者では単調性により、後者では直接の輸送により、どちらも x が Lset β に属することになり、仮定した非所属に反する。

    early : ⟨ stage (z .fst) (z .snd) ∈ sucV β ⟩ → ⊥₀
    early h = ⊥*-rec (∈sucV-elim {A = β} {x = stage (z .fst) (z .snd)}
      isProp⊥* h below same)
      where
      below : ⟨ stage (z .fst) (z .snd) ∈ β ⟩ → ⊥*

stage x ∈ β なら、段階の単調性により、既知の x ∈ Lset (stage x) から x ∈ Lset β が従う。stage x ≡ β なら、その等式に沿う輸送によって同じ結論が直接得られる。どちらも境界の仮定 x ∉ Lset β に反する。

      below k = ⊥₀-rec (hout
        (Lset-mono {α = β} {β = stage (z .fst) (z .snd)} k
          {x = z .fst} (stage-mem (z .fst) (z .snd))))
      same : stage (z .fst) (z .snd) ≡ β → ⊥*
      same e = ⊥₀-rec (hout (subst (λ u → ⟨ z .fst ∈ Lset u ⟩) e

等しい場合には、stage x ≡ β に沿って既知の所属 x ∈ Lset (stage x) を x ∈ Lset β へ輸送する。これが、最初の段階が β 以下にはありえないことを示すための第二の矛盾である。

        (stage-mem (z .fst) (z .snd))))

ここで順序数の三岐性により sucV β と stage x を比較する。前者が真に早ければ、x ∈ Lset (sucV β) が stage x の定義上の最小性に反する。stage x が早ければ、直前の議論が x ∉ Lset β に反する。したがって、等しい場合だけが残る。

    go : ⟨ sucV β ∈ stage (z .fst) (z .snd) ⟩
       ⊎ ((sucV β ≡ stage (z .fst) (z .snd)) ⊎ ⟨ stage (z .fst) (z .snd) ∈ sucV β ⟩)
       → β ≡ birth (z .fst) (z .snd)
    go (inl h) = ⊥₀-rec
      (stage-earliest (z .fst) (z .snd) (sucV β) (suc-ord ob) mem h)

sucV β ≡ stage x と stage x ≡ sucV (birth x) から、順序数の後続の単射性によって β ≡ birth x が得られる。結論は二つの狭義の場合を排除したことで強制されるのであり、論理式から誕生の証人を選んでいるのではない。

    go (inr (inl e)) = ord-suc-inj β (birth (z .fst) (z .snd)) ob
      (e ∙ sym (birth-suc (z .fst) (z .snd)))
    go (inr (inr h)) = ⊥₀-rec (early h)

読みの補題は、その枠の順序数性の仮定を運ぶ。論理式だけでは、その枠が順序数であることを証明しない。証明は、切り詰められた存在量化を解いて、外側の記録に到達する。

BirthAt-out : ⟨ γ ⊨ BirthAt b x ⟩ → IsOrd β → β ≡ birth (z .fst) (z .snd)
BirthAt-out h ob =
  rec₁ (setIsSet β (birth (z .fst) (z .snd))) atCarrier h
  where
  atInner : (c : S) → ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩

候補の段階ごとに、内側の記録は、引数を含む定義可能冪の値と、引数が候補の段階に属さないことの反証を供給する。判定の補題が、この三つのデータに適用される。

          → (⟨ z .fst ∈ c .fst ⟩ → ⊥₀)
          → Inner c → β ≡ birth (z .fst) (z .snd)
  atInner c hg hn (d , (hd , hm)) = decideBirth ob
    (subst (λ u → ⟨ z .fst ∈ u ⟩) qd hm)
    (λ k → hn (subst (λ u → ⟨ z .fst ∈ u ⟩) (sym qc) k))

上げられた添字のもとでの段階のグラフは、階層の記述の一意性によって、候補の順序数の段階と同一視される。そして冪の値は、記述の段階の等式によって、その段階の定義可能冪と同一視される。

    where
    qc : c .fst ≡ Lset β
    qc = Lset-only zero (suc b) (c ∷ γ) hg ob
    qd : d .fst ≡ 𝒟ₒ (Lset β)
    qd = subst ⟨_⟩ (DefAt-stage β ob zero (suc zero) (d ∷ c ∷ γ) qc) hd

外側の記録は内側の読みへ消去され、内側の読みが判定の補題に渡される。証明全体は、切り詰めを、順序数の等式という命題の中へ消去する。

  atCarrier : Σ[ c ∶ S ] Outer c → β ≡ birth (z .fst) (z .snd)
  atCarrier (c , (hg , (hn , hi))) =
    rec₁ (setIsSet β (birth (z .fst) (z .snd)))
      (atInner c hg (λ k → lower (hn k))) hi

逆向きでは、スロット b の順序数が x のメタ言語での誕生に等しいと仮定する。二つの存在証人には、包装された段階 Lset β と、その包装された定義可能冪を用いる。存在量化の充足が要求する通り、これらは命題的切り詰めの中に置かれるので、この構成は論理式の証人が一意に定まるとは主張しない。

BirthAt-in : IsOrd β → β ≡ birth (z .fst) (z .snd) → ⟨ γ ⊨ BirthAt b x ⟩
BirthAt-in ob e = ∣ towerS β ob
  , (hg , (hn , ∣ powS β ob , (hd , hm) ∣₁)) ∣₁
  where
  hg : ⟨ (towerS β ob ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩

上げられた添字のもとでの段階のグラフが成立するのは、まとめられた段階が、提示の定義の等式によって、その添字の段階だからである。

  hg = Lset-defines zero (suc b) (towerS β ob ∷ γ) ob (towerS-fst β ob)

もし x が Lset β に属するなら、β を birth x で置き換えることで、x は stage x = sucV (birth x) より真に低い段階ですでに現れることになる。これは stage-earliest に反し、BirthAt が要求する非所属を与える。

  hn : ⟨ z .fst ∈ (towerS β ob) .fst ⟩ → Lift {j = ℓ-suc ℓ} ⊥₀
  hn k = lift (stage-earliest (z .fst) (z .snd) β ob
    (subst (λ u → ⟨ z .fst ∈ u ⟩) (towerS-fst β ob) k)
    (subst (λ u → ⟨ u ∈ stage (z .fst) (z .snd) ⟩) (sym e)
      (birth-stage (z .fst) (z .snd))))

DefAt の段階における等式は、その充足命題を 𝒟ₒ (Lset β) との等しさに同一視する。powS β ob の射影の等式がまさにこの等しさを与えるので、包装された定義可能冪は必要な条項を満たす。

  hd : ⟨ (powS β ob ∷ towerS β ob ∷ γ) ⊨ DefAt zero (suc zero) ⟩
  hd = subst ⟨_⟩
    (sym (DefAt-stage β ob zero (suc zero)
            (powS β ob ∷ towerS β ob ∷ γ) (towerS-fst β ob)))
    (powS-fst β ob)

最後に、birth-mem は x を Lset (sucV (birth x)) に入れる。候補順序数を誕生順序数で置き換え、Lset-suc を使い、さらに包装された定義可能冪の射影方程式を使うことで、この所属を第二の証人へ輸送する。外向きの読みと合わせると、候補スロットが順序数であると仮定した場合に BirthAt が誕生順序数を正確に記述することが分かる。内部で順序数性を加えることも、標準的な存在証人を与えることもない。

  hm : ⟨ z .fst ∈ (powS β ob) .fst ⟩
  hm = subst (λ u → ⟨ z .fst ∈ u ⟩) (sym (powS-fst β ob))
    (subst (λ u → ⟨ z .fst ∈ u ⟩) (Lset-suc β)
      (subst (λ u → ⟨ z .fst ∈ Lset (sucV u) ⟩) (sym e)
        (birth-mem (z .fst) (z .snd))))

codeAnyAt-in : ∀ {n k} (c w : Fin n) (γ : Vec S n)
             → (lookup w γ) .fst ≡ A .fst
             → (ψ : Formula ⟪ A .fst ⟫ k) → (lookup c γ) .fst ≡ (keyS A ψ) .fst
             → ⟨ γ ⊨ isCodeAnyAt c w ⟩

二つの連言項は、それぞれの内向きの読み出しで満たされる。アリティの読み出しが自然数と符号を名指し、証人の読み出しが、論理式が揃えられたアルファベットの上にあることを確認する。

codeAnyAt-in {k = k} c w γ qw ψ qc =
  arityNumAtL-in c γ k (codeS A ψ) qc , witnessAt-in A w c γ ψ qw qc

外向きの読み出しが、切り詰められた符号の証人を復元する。あるアリティとある論理式がこのキーを作る。切り詰められたデータは、命題の切り詰めの中にとどまる。

codeAnyAt-out : ∀ {n} (c w : Fin n) (γ : Vec S n)
              → (lookup w γ) .fst ≡ A .fst
              → ⟨ γ ⊨ isCodeAnyAt c w ⟩
              → ⟨ IsKeyOverAny A (lookup c γ) ⟩
codeAnyAt-out c w γ qw (hk , hw) =

証明は、アリティの読み出しを、自然数と符号の対の中へ消去し、証人の読み出しを、符号のレベルの切り詰められた存在の中へ写像する。

  rec₁ squash₁ step (arityNumAtL-out c γ hk)
  where
  step : Σ[ m ∶ ℕ ] Σ[ z ∶ S ] ((lookup c γ) .fst ≡ pr (# m) (z .fst))
       → ⟨ IsKeyOverAny A (lookup c γ) ⟩
  step (m , (z , qz)) = map₁ (λ { (ψ , q) → m , (ψ , q) })

証人の読み出しの消去が、正しいアリティで論理式と符号の等式を復元し、切り詰められた存在を完成させる。

    (witnessAt-out A w c γ qw hw m z qz)

CodesAt-out : ⟨ γ ⊨ CodesAt c w ⟩ → lookup c γ ≡ AllCodes A
CodesAt-out h = extensionalL step
  where

第一の包含では、codeAnyAt-out が、記述されたスロットへの所属を「その要素はある論理式のキーである」という命題的切り詰めへ読み替える。AllCodes-in はまさにこの主張を、固定されたメタ言語の集合 AllCodes A への所属へ変える。特定の復号が選ばれることはない。

  step : (x : S) → (x ∈ˢ lookup c γ) ≡ (x ∈ˢ AllCodes A)
  step x = ⇔toPath
    (λ hx → AllCodes-in A x
      (codeAnyAt-out A zero (suc w) (x ∷ γ) qw
        (extAt-out c (isCodeAnyAt zero (suc w)) γ h x hx)))

逆向きの包含では、AllCodes A への所属から得られるのは、与えられた要素をキーにもつアリティと論理式の命題的切り詰めだけである。符号ごとの論理式の充足は命題なので、そこで切り詰めを除去して codeAnyAt-in を適用できる。ただし、特定の復号が取り出されるわけではない。

    (λ hx → extAt-in c (isCodeAnyAt zero (suc w)) γ h x
      (rec₁ (((x ∷ γ) ⊨ isCodeAnyAt zero (suc w)) .snd)
        (λ { (k , (ψ , q)) →
               codeAnyAt-in A {k = k} zero (suc w) (x ∷ γ) qw ψ q })
        (AllCodes-out A x hx)))

逆に、スロット c の値が AllCodes A に等しいとする。CodesAt を示すには、外延を述べる論理式が要求する二つの所属の含意を示せば十分である。すなわち、スロットの要素は符号ごとの述語を満たし、その述語を満たすものはスロットに属する。

CodesAt-in : lookup c γ ≡ AllCodes A → ⟨ γ ⊨ CodesAt c w ⟩
CodesAt-in q = extAt-in-both c (isCodeAnyAt zero (suc w)) γ into back
  where
  into : (x : S) → ⟨ x .fst ∈ (lookup c γ) .fst ⟩
       → ⟨ (x ∷ γ) ⊨ isCodeAnyAt zero (suc w) ⟩

第一の含意では、集合の等式によってスロットへの所属を AllCodes A への所属へ移す。そこから論理式の証人が得られるのは命題的切り詰めのもとだけであるが、目標は isCodeAnyAt の充足という命題なので、その目標へ切り詰めを除去できる。

  into x hx = rec₁ (((x ∷ γ) ⊨ isCodeAnyAt zero (suc w)) .snd)
    (λ { (k , (ψ , qk)) →
           codeAnyAt-in A {k = k} zero (suc w) (x ∷ γ) qw ψ qk })
    (AllCodes-out A x (subst (λ u → ⟨ x .fst ∈ u .fst ⟩) q hx))

逆向きの含意では、codeAnyAt-out が充足を「候補はある論理式のキーである」という命題的切り詰めへ読み替える。AllCodes-in はまさにこの切り詰められた主張から AllCodes A への所属を示し、集合の等式がその結論をスロット c へ戻す。

  back : (x : S) → ⟨ (x ∷ γ) ⊨ isCodeAnyAt zero (suc w) ⟩
       → ⟨ x .fst ∈ (lookup c γ) .fst ⟩
  back x hx = subst (λ u → ⟨ x .fst ∈ u .fst ⟩) (sym q)
    (AllCodes-in A x (codeAnyAt-out A zero (suc w) (x ∷ γ) qw hx))

private module Fam = Family α (λ δ _ → orderAt δ) oα

層のすべての要素は構成可能である。層の構成可能性と、所属に沿う推移性によるものである。

memberL : (a : Mem (Lset α)) → ⟨ isL (a .fst) ⟩
memberL a = Lset→isL α oα (a .fst) (a .snd)

Lset α の各要素 a は構成可能なので、誕生順序数をもつ。この順序数を bornOf a と書く。これは α での順序を展開するときの第一の比較キーになる。

bornOf : (a : Mem (Lset α)) → V ℓ
bornOf a = birth (a .fst) (memberL a)

bornOf a ∈ α という事実には二つの役割がある。まず、orderAt α の展開で誕生順序数を前段階の添字として使えることを保証する。さらに後では、対象言語による誕生の記述から、bornIn によって a の周囲の段階への所属を回復できる。

bornMem : (a : Mem (Lset α)) → ⟨ bornOf a ∈ α ⟩
bornMem a = Fam.bornAt a .snd

展開の等式が、本章の接続点である。α での順序が a と b の間で成立するのは、a の誕生の順序数が b のそれより厳密に下にあるか、あるいは、同じ誕生の順序数を共有していて、その誕生の順序数での局所のステップの順序が a を b の下に置くときで、そのときに限る。

order-unfold : (a b : Mem (Lset α))
             → relOf (orderAt α oα) a b
             ≡ ( ⟨ bornOf a ∈ bornOf b ⟩
               ⊎ ( (bornOf b ≡ bornOf a)
                 × Under (bornOf a) (stepOrder (bornOf a)

証明は orderAt-step で所属再帰を一段だけ開き、その基礎にある関係へ合同性を適用する。したがって、この二場合の等式は前章で構成済みの順序から導かれる。ここでその狭義整列順序を構成し直したり、証明し直したりはしない。

                     (mem-ord {A = α} oα (bornOf a) (bornMem a)))
                     (a .fst) (b .fst) ) )
order-unfold a b = cong (λ z → relOf (z oα) a b) (orderAt-step α)

新たに束縛される四つの対象は、比較される集合 u,v と、その誕生順序数の候補 du,dv である。最初の二つの条項は BirthAt du u と BirthAt dv v を主張する。これらが候補を実際の誕生段階と同一視するのは、後の読みが du と dv の順序数性を与えたときである。

OrdBody : ∀ {n} → Term S n → Fin n → Formula S (suc (suc (suc (suc n))))
OrdBody tb f =
    BirthAt (suc zero) (sh3 zero)
  ∧̇ ( BirthAt zero (sh2 zero)
    ∧̇ ( (var (suc zero) ∈̇ tm4 tb)

次の二つの条項は、誕生段階の二つの候補がともに項 tb の表す段階に属することを要求する。最後の選言は誕生段階優先の規則を再現する。すなわち、du ∈ dv であるか、または dv ≡ du であり、与えられたステップ論理式がその共通の台で u と v を比較する。ここでは u と v の間の集合所属を主張していない。

      ∧̇ ( (var zero ∈̇ tm4 tb)
        ∧̇ ( (var (suc zero) ∈̇ var zero)
          ∨̇ ( (var zero ≐ var (suc zero))
            ∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ) ) )

CondCore はまず、比較される二つの対象 u と v を存在量化する。対を表す論理式は、スロット z の引数がそれらの順序対であることを要求する。さらに二つの存在量化が誕生段階の候補を束縛し、その後で OrdBody が誕生段階優先の比較を調べる。四つの証人はいずれも存在論理式の充足意味論のもとにあるため、命題的に切り詰められている。

opaque
  CondCore : ∀ {n} → Fin n → Term S n → Fin n → Formula S n
  CondCore z tb f =
    ∃̇ ( ∃̇ ( prAtL (sh2 z) (suc zero) zero ∧̇ ∃̇ (∃̇ (OrdBody tb f)) ) )

記述の意味を双方向に読む

CondCore を読むため、tb が表す順序数段階と、その段階上の表を固定する。Values は記録された各値が対応する局所関係を実現することを保証し、Entries は段階より下の各台で何らかの値が記録されていることだけを述べる。これらが、後の二方向で使う仮定である。

module _ {n : ℕ} (z : Fin n) (tb : Term S n) (f : Fin n) (γ : Vec S n)
         (oα : IsOrd ((⟦ tb ⟧ γ) .fst))
         (vals : Values (lookup f γ) ((⟦ tb ⟧ γ) .fst))
         (ents : Entries (lookup f γ) ((⟦ tb ⟧ γ) .fst)) where

private

  α : V ℓ
  α = (⟦ tb ⟧ γ) .fst

  shift : (u v du dv : S) → ⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ) ≡ ⟦ tb ⟧ γ
  shift u v du dv = tm4-val tb u v du dv γ

  value : (d : S) → ⟨ d .fst ∈ α ⟩ → (P : hProp (ℓ-suc ℓ))
        → ((r : S) → ⟨ pr (d .fst) (r .fst) ∈ (lookup f γ) .fst ⟩
           → IsRel (d .fst) r → ⟨ P ⟩)
        → ⟨ P ⟩
  value d hd P k = rec₁ ⟨ P ⟩isProp

    (λ { (r , hr) → k r hr (vals d r hd hr) }) (ents d hd)

  Deep : (u v du : S) → S → Type (ℓ-suc ℓ)
  Deep u v du dv = ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ OrdBody tb f ⟩

opaque
 unfolding CondCore

 CondCore-out : ⟨ γ ⊨ CondCore z tb f ⟩ → ⟨ Related α ((lookup z γ) .fst) ⟩
 CondCore-out = rec₁ ((Related α ((lookup z γ) .fst)) .snd)
   (λ { (u , hv) → rec₁ ((Related α ((lookup z γ) .fst)) .snd)
     (λ { (v , (hp , hdu)) → rec₁ ((Related α ((lookup z γ) .fst)) .snd)
       (λ { (du , hdv) → rec₁ ((Related α ((lookup z γ) .fst)) .snd)

         (λ { (dv , hd) → atDeep u v du dv hp hd }) hdv }) hdu }) hv })
   where
   Goal : Type (ℓ-suc ℓ)
   Goal = ⟨ Related α ((lookup z γ) .fst) ⟩

   atDeep : (u v du dv : S)
          → ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩
          → Deep u v du dv → Goal
   atDeep u v du dv hp (hbu , (hbv , (hmu₀ , (hmv₀ , hcmp)))) =
     subst (λ w → ⟨ Related α w ⟩) (sym qz)

       (rec₁ ((Related α (pr (u .fst) (v .fst))) .snd) atCase hcmp)
     where
     qz : (lookup z γ) .fst ≡ pr (u .fst) (v .fst)
     qz = subst ⟨_⟩ (prAtL-adequate (sh2 z) (suc zero) zero (v ∷ u ∷ γ)) hp

     hmu : ⟨ du .fst ∈ α ⟩
     hmu = subst (λ w → ⟨ du .fst ∈ w .fst ⟩) (shift u v du dv) hmu₀

     hmv : ⟨ dv .fst ∈ α ⟩
     hmv = subst (λ w → ⟨ dv .fst ∈ w .fst ⟩) (shift u v du dv) hmv₀

     odu : IsOrd (du .fst)
     odu = mem-ord {A = α} oα (du .fst) hmu

     odv : IsOrd (dv .fst)
     odv = mem-ord {A = α} oα (dv .fst) hmv

     qu : du .fst ≡ birth (u .fst) (u .snd)
     qu = BirthAt-out (suc zero) (sh3 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) hbu odu

     qv : dv .fst ≡ birth (v .fst) (v .snd)
     qv = BirthAt-out zero (sh2 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) hbv odv

     a : Mem (Lset α)
     a = u .fst , bornIn α oα (u .fst) (u .snd)
           (subst (λ w → ⟨ w ∈ α ⟩) qu hmu)

     c : Mem (Lset α)
     c = v .fst , bornIn α oα (v .fst) (v .snd)
           (subst (λ w → ⟨ w ∈ α ⟩) qv hmv)

     qa : bornOf α oα a ≡ du .fst
     qa = birth-proof (u .fst) (memberL α oα a) (u .snd) ∙ sym qu

     qc : bornOf α oα c ≡ dv .fst
     qc = birth-proof (v .fst) (memberL α oα c) (v .snd) ∙ sym qv

     fill : relOf (orderAt α oα) a c → ⟨ Related α (pr (u .fst) (v .fst)) ⟩
     fill = related-in α oα a c

     atCase : ⟨ du .fst ∈ dv .fst ⟩
            ⊎ ( (dv .fst ≡ du .fst)
              × ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ⟩ )
            → ⟨ Related α (pr (u .fst) (v .fst)) ⟩
     atCase (inl h) = fill (transport (sym (order-unfold α oα a c))