---
title: "構成可能階層を表す列"
module: L.Coding.HierarchySequence
lang: ja
site: "Bedrock"
description: "構成可能階層を表す列"
stage: "内部の符号化：表と一様な充足関係"
reading_order: 70
canonical: https://bedrock.institute/ja/L.Coding.HierarchySequence.html
html: L.Coding.HierarchySequence.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/HierarchySequence.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Model, L.Coding.Expressions, L.Coding.DefinablePowerSet]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.HierarchySequence.md, https://bedrock.institute/zh/L.Coding.HierarchySequence.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 構成可能階層を表す列

本章では、定義可能な冪集合を逐次取って得られる段階を関数グラフで記述します。その関数の部分的な近似を特徴づけ、後で構成可能階層の始切片を認識するために使うグラフを包装します。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The tower is the one construction on this route that cannot be internalized the
way the satisfaction recursion was. A graph may not name the object it defines,
and the tower at a stage is built out of the tower below that stage, so a graph
written directly for the tower would have to name its own values at
sub-arguments. It has none to name.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

What can be said instead is what an **approximation** is. A function `f` is an
approximation to the hierarchy on `a` when it is defined exactly on the members
of `a` and every value it records is the step at that argument computed from `f`
itself. The step consults `f` only below the argument, so the condition never
looks at a value the function does not already record, and the tower's own value
at `a` is then whatever the step from such an `f` yields. That is a sequence
characterization, and it is a first-order sentence about `f` alone.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Every slot in this chapter is represented by a variable. The approximation is
bound by the graph's one existential, the argument and the value are the graph's
two free variables, and nothing anywhere is a named constant, which is what lets
the whole description be stated where the hierarchy needs it: under the binder
that holds the stage. Every reading below is stated at a **variable**
environment, for the reason the last two chapters were: an adequacy discharged at a
concrete environment puts the construction of that environment inside a satisfaction, and
the same statement then costs minutes instead of seconds.

</details>

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

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

module L.Coding.HierarchySequence {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; _⇒̇_; ∃̇_; ∀̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; 𝒟ₒ )
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; domAt; domAt-in; domAt-out; prAtL; prAtL-adequate )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-out; extAt-in; extAt-in-both )
open import L.Coding.DefinablePowerSet {ℓ} lem using ( DefAt; DefAt-in; DefAt-out )

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )

open hPropStructure 𝒮ʟ

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
```

## 後者段階の関係

`StepAt v b f` は、`v` が `f` の定義域にある後者の引数であり、そこでの `f` の値が直前の `b` での値の定義可能な冪集合であることを表します。`Records`、`StepOf`、`PowOK` がこの主張の三部分を示します。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

`v` is the stage at `b`, given the approximation `f` below `b`, when the members
of `v` are exactly the sets lying in the definable powerset of some value `f`
records at some argument in `b`. Three adjacent existentials carry it: the
argument `c`, the value `w` the approximation records there, and the definable
powerset `d` of that value. The powerset has to be **bound**, because the
previous chapter delivers a description of it and not a term for it; `DefAt`
says that `d` is the definable powerset of `w`, so the only way to use it is to
quantify over the thing it describes.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The whole step is **one** `extAt`, and that is a decision rather than a
convenience. A stage is a set, and every clause of a set-valued recursion says
the same thing: this value is the set of exactly those things meeting a
condition. Written as a hand-made pair of inclusions the condition would appear
twice, once under each inclusion, so the three existentials would be duplicated,
every later change to them would have to be made in two places, and each reading
would have to be reassembled from two halves that are not each other's inverse.
`extAt` writes the condition once and hands the two readings back as
projections, which is exactly what it exists for.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

One side condition travels with the step, and one hypothesis discharges it in
both directions. To satisfy the description one must produce the definable
powerset **as an element of the model**, since an object-language existential
ranges over `L`; to read the description back one needs the elimination of
`DefAt`, whose side condition is that the definable subsets of the carrier are
constructible. The first implies the second: if `𝒟ₒ w` is an element of `L` then
its members are constructible by transitivity of the class. So both directions
ask for the same thing, `PowOK`, and a consumer at a stage discharges it
with the successor identity.

</details>

```agda
private
  sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n))))
  sh4 i = suc (suc (suc (suc i)))

StepBody : ∀ {n} → Fin n → Fin n → Formula S (suc (suc (suc (suc n))))
StepBody b f = (var (suc (suc zero)) ∈̇ var (sh4 b))
             ∧̇ ( appAt (sh4 f) (suc (suc zero)) (suc zero)
               ∧̇ ( DefAt zero (suc zero)
                 ∧̇ (var (suc (suc (suc zero))) ∈̇ var zero) ) )

StepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
StepAt v b f = extAt v (∃̇ (∃̇ (∃̇ (StepBody b f))))

Records : ∀ {n} → Fin n → Fin n → S ^ n → S → S → Type (ℓ-suc ℓ)
Records b f γ c w = ⟨ fst c ∈ fst (lookup b γ) ⟩
                  × ⟨ pr (fst c) (fst w) ∈ fst (lookup f γ) ⟩

StepOf : ∀ {n} → Fin n → Fin n → S ^ n → S → Type (ℓ-suc ℓ)
StepOf b f γ z = Σ[ c ∈ S ] Σ[ w ∈ S ]
                   (Records b f γ c w × ⟨ fst z ∈ 𝒟ₒ (fst w) ⟩)

PowOK : ∀ {n} → Fin n → Fin n → S ^ n → Type (ℓ-suc ℓ)
PowOK b f γ = (c w : S) → Records b f γ c w → ⟨ isL (𝒟ₒ (fst w)) ⟩
```

## 階層の一段を読み取り構成する

`StepAt-out` は満たされた段階から定義可能な冪集合の条件を取り出し、`StepAt-in` はその条件と必要な定義域データから充足を構成します。`StepAt-back` は取り出した条件を後の証明が使う形で保持します。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Reading the body is where the three existentials are spent, and each `PT.rec`
below names the type of its payload. That is the law the Powerset chapter was
written under and it is not a stylistic one: left to inference the payload is a
metavariable standing for the satisfaction of a formula the elaborator has not
committed to, and the same two lines then run past two minutes instead of two
seconds.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Assembling the body is the same three existentials filled in. The definable
powerset is supplied as the element of the model that `PowOK` provides,
its own coding equation is `refl` at that element, and the introduction
of `DefAt` needs nothing else. The readings of the step are then
`extAt`'s directions with those halves plugged in, and there are three of
them rather than two: `StepAt-out` reads a member of the step as a
payload, `StepAt-back` puts a payload back, and `StepAt-in` builds
the step from both directions at once, since a set built by extension has to be
re-entered member by member from both sides. The reading and the assembly of the
body are shared between all three, so each projection is one line.

</details>

```agda
module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) where
  private
    Φ : Formula S (suc n)
    Φ = ∃̇ (∃̇ (∃̇ (StepBody b f)))

    readBody : PowOK b f γ → (z c w d : S)
             → ⟨ (d ∷ w ∷ c ∷ z ∷ γ) ⊨ StepBody b f ⟩ → StepOf b f γ z
    readBody ok z c w d (hb , (ha , (hd , hz))) =
      c , w , rec , subst (λ X → ⟨ fst z ∈ X ⟩) qd hz
      where
```

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Perf: `env` spelled out at both ends; via an abbreviation, 15 s per conversion.

</details>

```agda
      rec : Records b f γ c w
      rec = hb , subst ⟨_⟩ (appAt-adequate
        (sh4 f) (suc (suc zero)) (suc zero) (d ∷ w ∷ c ∷ z ∷ γ)) ha

      qd : fst d ≡ 𝒟ₒ (fst w)
      qd = DefAt-out w zero (suc zero) (d ∷ w ∷ c ∷ z ∷ γ)
        (λ x x∈ → isL-trans {x = 𝒟ₒ (fst w)} {y = x} x∈ (ok c w rec)) refl hd

    unfold : PowOK b f γ → (z : S)
           → ⟨ (z ∷ γ) ⊨ Φ ⟩ → ∥ StepOf b f γ z ∥₁
    unfold ok z = PT.rec squash₁ viaArg
      where
      viaPow : (c w : S)
             → Σ[ d ∈ S ] ⟨ (d ∷ w ∷ c ∷ z ∷ γ) ⊨ StepBody b f ⟩
             → ∥ StepOf b f γ z ∥₁
      viaPow c w (d , hd) = ∣ readBody ok z c w d hd ∣₁

      viaVal : (c : S)
             → Σ[ w ∈ S ] ⟨ (w ∷ c ∷ z ∷ γ) ⊨ ∃̇ (StepBody b f) ⟩
             → ∥ StepOf b f γ z ∥₁
      viaVal c (w , hw) = PT.rec squash₁ (viaPow c w) hw

      viaArg : Σ[ c ∈ S ] ⟨ (c ∷ z ∷ γ) ⊨ ∃̇ (∃̇ (StepBody b f)) ⟩
             → ∥ StepOf b f γ z ∥₁
      viaArg (c , hc) = PT.rec squash₁ (viaVal c) hc

    fill : PowOK b f γ → (z : S) → StepOf b f γ z → ⟨ (z ∷ γ) ⊨ Φ ⟩
    fill ok z (c , (w , (rec , hz))) =
      ∣ c , ∣ w , ∣ D , (rec .fst , (ha , (hdef , hz))) ∣₁ ∣₁ ∣₁
      where
```

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Perf: `env` spelled out at both ends; via an abbreviation, 15 s per conversion.

</details>

```agda
      D : S
      D = 𝒟ₒ (fst w) , ok c w rec

      ha : ⟨ (D ∷ w ∷ c ∷ z ∷ γ) ⊨ appAt (sh4 f) (suc (suc zero)) (suc zero) ⟩
      ha = subst ⟨_⟩ (sym (appAt-adequate
        (sh4 f) (suc (suc zero)) (suc zero) (D ∷ w ∷ c ∷ z ∷ γ))) (rec .snd)

      hdef : ⟨ (D ∷ w ∷ c ∷ z ∷ γ) ⊨ DefAt zero (suc zero) ⟩
      hdef = DefAt-in w zero (suc zero) (D ∷ w ∷ c ∷ z ∷ γ) refl refl

  StepAt-out : ⟨ γ ⊨ StepAt v b f ⟩ → PowOK b f γ
             → (z : S) → ⟨ fst z ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ z ∥₁
  StepAt-out h ok z z∈ = unfold ok z (extAt-out v Φ γ h z z∈)

  StepAt-back : ⟨ γ ⊨ StepAt v b f ⟩ → PowOK b f γ
              → (z : S) → StepOf b f γ z → ⟨ fst z ∈ fst (lookup v γ) ⟩
  StepAt-back h ok z s = extAt-in v Φ γ h z (fill ok z s)

  StepAt-in : PowOK b f γ
            → ((z : S) → ⟨ fst z ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ z ∥₁)
            → ((z : S) → StepOf b f γ z → ⟨ fst z ∈ fst (lookup v γ) ⟩)
            → ⟨ γ ⊨ StepAt v b f ⟩
  StepAt-in ok into back = extAt-in-both v Φ γ
    (λ z z∈ → PT.rec (snd ((z ∷ γ) ⊨ Φ)) (fill ok z) (into z z∈))
    (λ z h → PT.rec (snd (fst z ∈ fst (lookup v γ))) (back z) (unfold ok z h))
```

## 階層列の近似

`ApproxAt f a` は、順序数 `a` を定義域とし、指定された初期値をもち、各後者での値が `StepAt` によって結ばれる関数を記述します。`GraphAt` はそのような関数を存在量化で包装し、読取り補題は定義域、値、段階方程式を示します。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Two conjuncts, and there is no third. `f` is defined on `a`, and every value `f`
records is the step at that argument from `f` itself. The second conjunct needs
no guard saying the argument lies in `a`: the first conjunct already pins the
domain to `a` in both directions, so an argument at which anything is recorded
is a member of `a` and saying so again would only lengthen the sentence.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The pair is a membership **equivalence**, and that matters more than it looks.
Stated the other way, as "for each argument in `a` there merely is a value which
is the step there", the sentence permits `f` to hold junk pairs beside the right
ones, so it does not determine `f`, the existence claim is not a proposition,
and an induction against it needs an internal function-extensionality lemma to
get from two approximations to one. As an equivalence the motive is a
proposition and that lemma never has to be written.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

There is deliberately **no single-valuedness conjunct**. It would assert nothing
the second conjunct does not already give: if two values are recorded at one
argument then both are the step at that argument, the step is a set identity,
and two sets with the same members are equal. Carrying it would put three
universal quantifiers under a satisfaction in exchange for a corollary.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The three projections are the three questions a consumer asks: an argument with
an entry is in the domain, an argument in the domain has an entry, and a
recorded value is a step. The introduction is here rather than at the call site
for the reason every reading is: it discharges an adequacy, and it must do so
at a variable environment.

</details>

```agda
private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)

module RecShape (Step : ∀ {n} → Fin n → Fin n → Fin n → Formula S n) where

  Domain₀ : S → V ℓ → Type (ℓ-suc ℓ)
  Domain₀ h B = (c z : S) → ⟨ pr (fst c) (fst z) ∈ fst h ⟩ → ⟨ fst c ∈ B ⟩

  ApproxAt : ∀ {n} → Fin n → Fin n → Formula S n
  ApproxAt f a = domAt f a
               ∧̇ ∀̇ (∀̇ ( appAt (sh2 f) (suc zero) zero
                       ⇒̇ Step zero (suc zero) (sh2 f) ))

  GraphAt : ∀ {n} → Fin n → Fin n → Formula S n
  GraphAt w b = ∃̇ (ApproxAt zero (suc b) ∧̇ Step (suc w) (suc b) zero)

  module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) where
    ApproxAt-dom : ⟨ γ ⊨ ApproxAt f a ⟩ → Domain₀ (lookup f γ) (fst (lookup a γ))
    ApproxAt-dom h = domAt-out f a γ (h .fst)

    ApproxAt-value : ⟨ γ ⊨ ApproxAt f a ⟩ → (c : S)
                   → ⟨ fst c ∈ fst (lookup a γ) ⟩
                   → ∥ (Σ[ z ∈ S ] ⟨ pr (fst c) (fst z) ∈ fst (lookup f γ) ⟩) ∥₁
    ApproxAt-value h = domAt-in f a γ (h .fst)

    ApproxAt-step : ⟨ γ ⊨ ApproxAt f a ⟩ → (c z : S)
                  → ⟨ pr (fst c) (fst z) ∈ fst (lookup f γ) ⟩
                  → ⟨ (z ∷ c ∷ γ) ⊨ Step zero (suc zero) (sh2 f) ⟩
    ApproxAt-step h c z p = h .snd c z
      (subst ⟨_⟩ (sym (appAt-adequate (sh2 f) (suc zero) zero (z ∷ c ∷ γ))) p)

    ApproxAt-in : ⟨ γ ⊨ domAt f a ⟩
                → ((c z : S) → ⟨ pr (fst c) (fst z) ∈ fst (lookup f γ) ⟩
                   → ⟨ (z ∷ c ∷ γ) ⊨ Step zero (suc zero) (sh2 f) ⟩)
                → ⟨ γ ⊨ ApproxAt f a ⟩
    ApproxAt-in hd hs = hd , λ c z p → hs c z
      (subst ⟨_⟩ (appAt-adequate (sh2 f) (suc zero) zero (z ∷ c ∷ γ)) p)

  module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where
    GraphOf : Type (ℓ-suc ℓ)
    GraphOf = Σ[ f ∈ S ] ( ⟨ (f ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
                         × ⟨ (f ∷ γ) ⊨ Step (suc w) (suc b) zero ⟩ )

    Graph-in : (f : S) → ⟨ (f ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
             → ⟨ (f ∷ γ) ⊨ Step (suc w) (suc b) zero ⟩ → ⟨ γ ⊨ GraphAt w b ⟩
    Graph-in f ha hs = ∣ f , (ha , hs) ∣₁

    Graph-out : ⟨ γ ⊨ GraphAt w b ⟩ → ∥ GraphOf ∥₁
    Graph-out h = h

  PairGraphAt : ∀ {n} → Fin n → Fin n → Formula S n
  PairGraphAt e c = ∃̇ (prAtL (suc e) (suc c) zero ∧̇ GraphAt zero (suc c))

  module _ {n : ℕ} (e c : Fin n) (γ : S ^ n)
           (φ : Formula S n) (qφ : φ ≡ PairGraphAt e c) where
    PairOf : Type (ℓ-suc ℓ)
    PairOf = Σ[ z ∈ S ] ( (fst (lookup e γ) ≡ pr (fst (lookup c γ)) (fst z))
                        × ⟨ (z ∷ γ) ⊨ GraphAt zero (suc c) ⟩ )

    PairGraph-in : (z : S) → fst (lookup e γ) ≡ pr (fst (lookup c γ)) (fst z)
                 → ⟨ (z ∷ γ) ⊨ GraphAt zero (suc c) ⟩ → ⟨ γ ⊨ φ ⟩
    PairGraph-in z q hg = subst (λ ψ → ⟨ γ ⊨ ψ ⟩) (sym qφ)
      ∣ z , (subst ⟨_⟩
        (sym (prAtL-adequate (suc e) (suc c) zero (z ∷ γ))) q , hg) ∣₁

    PairGraph-out : ⟨ γ ⊨ φ ⟩ → ∥ PairOf ∥₁
    PairGraph-out h = PT.map
      (λ { (z , (hq , hg)) →
        z , (subst ⟨_⟩ (prAtL-adequate (suc e) (suc c) zero (z ∷ γ)) hq , hg) })
      (subst (λ ψ → ⟨ γ ⊨ ψ ⟩) qφ h)

open RecShape StepAt public renaming ( GraphAt to LsetGraphAt
                                     ; Graph-in to LsetGraph-in
                                     ; Graph-out to LsetGraph-out )
```

## 階層近似のグラフ

`PairGraphAt` は、順序数の引数と近似がそこで割り当てる値との対を認識します。最後のグラフ論理式はこれらの対だけを集め、各点での近似を階層列を表す集合にします。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

One existential over the approximation, and under it the two conjuncts the
chapter was written for: `f` is an approximation on the argument, and the value
is the step at that argument from `f`. The value stands at the first slot and
the argument at the second, which is the order the model's replacement field
reads a graph in, and `LsetGraph` is the sentence with those two slots
filled in.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The approximation is bound, and it has to be. A graph may not name the object it
defines, and it may assert the existence of something only when that something
is already known to be an element of `L`, since satisfaction is read at the
model. An approximation is such a thing: it is a set of pairs collected by
replacement from arguments below, not the tower it is used to describe. The
consumer supplies one; the graph merely says there merely is one.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Both readings are one line each, because a satisfied existential **is** a
truncated sigma and a satisfied conjunction **is** a pair. What they buy is not
proof, it is the name and the slot. `GraphOf` writes the payload type out
rather than leaving it to inference, and both readings stand at **variable**
slots in a variable environment, so a consumer instantiates them rather than
converting against them.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The naming is the whole cost of this section, and the figure is worth keeping
because the first diagnosis of it was wrong. Stated with the graph named by its
closed-sentence alias, the same two lines took 98 seconds of the chapter's 130.
The slots were blamed and they are innocent: an isolating measurement in the next
chapter puts a reading at fully concrete slots at fifteen milliseconds and the
same reading against an alias at fifty-one seconds. What costs is deciding a
satisfaction of the alias against a satisfaction of its expansion, which Agda
settles by normalizing a satisfaction that carries the entire
definable-powerset description inside it. Generic in the slots the readings never
meet that question, and the closed sentence is one unfolding away,
and the concrete sentence is one unfolding away.

</details>

## まとめ

得られた集合符号化グラフは、ある順序数の限界までの構成可能段階を順に記録し、その段階関係は後の内部記述に必要な定義可能な冪集合の論理式ですでに表されています。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

`LsetGraph` is the object-language sentence "the value is the stage at
the argument", written without naming a stage, a tower, or an ordinal.
`StepAt` is one `extAt` over three adjacent existentials, the
argument, the value recorded there and its definable powerset;
`ApproxAt` is two conjuncts, the domain and the step condition, and no
more.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Nothing here is proved twice. The definable powerset arrives from the previous
chapter as a description at a slot and is used exactly as it was delivered, the
function machinery is read off `appAt` and `domAt`, and the step's
two readings are `extAt`'s own two. What the chapter contributes is the
shape: a graph that consults an approximation rather than the tower, which is
the only shape a graph is allowed to have.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Two rulings are recorded where a reader meets them. The step is a membership
equivalence rather than a one-directional collection, which keeps the motive of
the induction to come a proposition and removes an internal
function-extensionality lemma from the route entirely. And there is no
single-valuedness conjunct, because the step condition already pins every value
recorded at an argument, so single-valuedness is a corollary and not a
hypothesis.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

One measurement, and the chapter after this one corrected its diagnosis. Every
second this chapter ever cost was a conversion between two spellings of the same
thing, and every time Agda answered it by normalizing a satisfaction with the
whole definable-powerset description inside: 98 seconds for two readings taken
against the graph's closed-sentence alias, and 15 seconds at each place where a
hypothesis carried an environment written out while the application named it
behind an abbreviation. Concrete slots are not the mechanism and cost nothing.
Written so that the two sides are the same expression, the chapter checks in
under two seconds rather than 130, with no change to the mathematics. The law
the preceding coding chapters were written under, that an adequacy is discharged at a
variable argument, holds for a **statement** exactly as it does for a
substitution.

</details>