---
title: "固定長環境の集合"
module: L.Coding.EnvironmentSet
lang: ja
site: "Bedrock"
description: "固定長環境の集合"
stage: "内部の符号化：表と一様な充足関係"
reading_order: 48
canonical: https://bedrock.institute/ja/L.Coding.EnvironmentSet.html
html: L.Coding.EnvironmentSet.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/EnvironmentSet.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, FOL.ZFModel, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Stage, L.Axioms.Basic, L.Axioms.Full, L.Axioms.Numerals, L.Coding.Environment, L.Coding.CodeConstructibility, L.Coding.Model, L.Coding.Expressions]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.EnvironmentSet.md, https://bedrock.institute/zh/L.Coding.EnvironmentSet.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 固定長環境の集合

構成可能集合 `B` と自然数 `n` に対し、本章は `L` の要素 `envSet n` を構成し、その要素がちょうど `B` に値を取る長さ `n` の環境であることを示します。

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

The chapter that wrote the ten clauses said what it means for one thing to be
an environment over a set, and set aside the question of whether all of them
together form a set. This chapter answers it: the satisfaction predicates will
be separated from this common set of environments.

</details>

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

The route is the one the axioms already provide. Environments over a set of `L` at a
fixed length are indexed by a small type; each is an element of `L`, so they all
lie below one stage, and separating that stage by the description gives exactly them.
Nothing here needs replacement, and nothing here needs recursion.

</details>

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _≐_; _∧̇_; ∃̇_ )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
open import V.Coding {ℓ} using ( pr; #-inj′ )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono )
open import L.Ordinal {ℓ} using ( boundingOrd; ∈#-elim )
open import V.Coding {ℓ} using ( #mono; pr-inj )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Coding.Environment {ℓ} using ( env )
open import L.Coding.CodeConstructibility {ℓ} using ( envL )
open import L.Coding.Model {ℓ} using ( envOverAt; svAt; domAt; valuesInAt; pairsInAt; inDomAt; prʟ; prʟ-fst; svAt-in; svAt-out; inDomAt-adequate; appAt-adequate; domAt-in; valuesInAt-out; envOver-sv; envOver-dom; envOver-values; envOver-pairs; pairsIn-in; pairsIn-out )
open import L.Coding.Expressions {ℓ} using ( numL )

open import Cubical.Data.FinData using ( toℕ; inj-toℕ )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈∈ₛ; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( #_ )

open hPropStructure 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ

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

## 小さい族を覆う段階

`stageFor` は構成可能集合からなる任意の小さい族の全要素を含む一つの順序数段階を見つけ、分出に必要な共通の周囲の段階を与えます。

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

The move `smallDom` makes, with the ordinal kept rather than hidden,
because what is needed here is a lemma stated about stages rather than about a set
of the model.

</details>

```agda
stageFor : (X : Type ℓ) (f : X → S)
         → Σ[ β ∈ V ℓ ] (IsOrd β × ((x : X) → ⟨ fst (f x) ∈ Lset β ⟩))
stageFor X f = β , (oβ , mem)
  where
  b = boundingOrd X (λ x → stage (fst (f x)) (f x .snd))
        (λ x → stage-ord (fst (f x)) (f x .snd))
  β = b .fst
  oβ : IsOrd β
  oβ = b .snd .fst
  mem : (x : X) → ⟨ fst (f x) ∈ Lset β ⟩
  mem x = Lset-mono {α = β} {β = stage (fst (f x)) (f x .snd)} (b .snd .snd x)
            (stage-mem (fst (f x)) (f x .snd))
```

## 一つの環境をモデルの要素にする

各 `g : Fin n → ⟪ B ⟫` について `envSL` はその有限グラフが構成可能であることを示すので、包装された `envS g` を `stageFor` で抑えられます。

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

An environment over a set of `L` is a finite set of pairs of a numeral with a
member, and a member of an element of `L` is an element of `L`, so the pairs are
too and the stage lemma above closes it.

</details>

```agda
module _ (B : S) where
  private
    ix : ⟪ fst B ⟫ → S
    ix m = ⟪ fst B ⟫↪ m
         , isL-trans (∈∈ₛ {a = ⟪ fst B ⟫↪ m} {b = fst B} .snd (∈ₛ⟪ fst B ⟫↪ m))
             (snd B)

  Ix : ℕ → Type ℓ
  Ix n = Fin n → ⟪ fst B ⟫

  opaque
    envSL : {n : ℕ} (g : Ix n) → ⟨ isL (env (λ i → fst (ix (g i)))) ⟩
    envSL {n} g = envL β oβ (λ i → fst (ix (g i))) mem
      where
      pairs : Lift {ℓ-zero} {ℓ} (Fin n) → S
      pairs i = prʟ (numeralL (toℕ (lower i))) (ix (g (lower i)))

      sf : Σ[ b ∈ V ℓ ] (IsOrd b
         × ((i : Lift {ℓ-zero} {ℓ} (Fin n)) → ⟨ fst (pairs i) ∈ Lset b ⟩))
      sf = stageFor (Lift {ℓ-zero} {ℓ} (Fin n)) pairs

      β : V ℓ
      β = sf .fst

      oβ : IsOrd β
      oβ = sf .snd .fst

      mem : (i : Fin n) → ⟨ pr (# (toℕ i)) (fst (ix (g i))) ∈ Lset β ⟩
      mem i = subst (λ w → ⟨ w ∈ Lset β ⟩)
        (prʟ-fst (numeralL (toℕ i)) (ix (g i))
          ∙ cong₂ pr (numeralL-fst (toℕ i)) refl)
        (sf .snd .snd (lift i))

  envS : {n : ℕ} → Ix n → S
  envS g = env (λ i → fst (ix (g i))) , envSL g
```

## 環境の集合を分出する

`envFo n` は `envOverAt` を固定された長さ `n` と基礎集合 `B` に特殊化し、共通の段階での分出が `envSet n` とその要素条件を定義します。

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

The description takes three arguments and separation offers one variable, so the
other two are bound and pinned to constants. That is three lines and it keeps the
description as the chapter wrote it, which is worth more than saving them.

</details>

```agda
  private
    nn : ℕ → S
    nn k = # k , numL k

  envFo : (n : ℕ) → Formula S 1
  envFo n = ∃̇ (∃̇ ( (var (suc zero) ≐ con (nn n))
                 ∧̇ ((var zero ≐ con B)
                 ∧̇ envOverAt (suc (suc zero)) (suc zero) zero) ))

  private
    sf : (n : ℕ) → Σ[ β ∈ V ℓ ] (IsOrd β × ((g : Ix n) → ⟨ fst (envS g) ∈ Lset β ⟩))
    sf n = stageFor (Ix n) envS

    amb : (n : ℕ) → S
    amb n = LsetS (sf n .fst) (sf n .snd .fst)

  opaque
    envSet : (n : ℕ) → S
    envSet n = hasSeparationL (amb n) (envFo n) .fst .fst

    envSet-mem : (n : ℕ) (x : S)
               → (x ∈ˢ envSet n) ≡ ((x ∈ˢ amb n) ⊓ ((x ∷ []) ⊨ envFo n))
    envSet-mem n = hasSeparationL (amb n) (envFo n) .fst .snd
```

## すべての環境がその集合に入る

`g : Fin n → ⟪ B ⟫` について、そのグラフが単値で定義域が `n` であり、必要な値と対をちょうど含むことを確認し、`envSet n` に属することを示します。

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

Four conjuncts, and each is the description read against what an environment
actually is. Single-valuedness and the two containments come straight off the
membership specification, which is `refl`; the domain is the only one that
does arithmetic, because saying the domain is the numeral `n` means saying that
the indices below `n` are exactly the numerals below `n`.

</details>

```agda
  module _ {n : ℕ} (g : Ix n) where
    private
      out : (s : V ℓ) → ⟨ s ∈ fst (envS g) ⟩
          → ∥ (Σ[ i ∈ Fin n ] (pr (# (toℕ i)) (fst (ix (g i))) ≡ s)) ∥₁
      out s = PT.map (λ { (li , e) → lower li , e })

      into : (i : Fin n) → ⟨ pr (# (toℕ i)) (fst (ix (g i))) ∈ fst (envS g) ⟩
      into i = ∣ lift i , refl ∣₁

      val∈ : (i : Fin n) → ⟨ fst (ix (g i)) ∈ fst B ⟩
      val∈ i = ∈∈ₛ {a = ⟪ fst B ⟫↪ (g i)} {b = fst B} .snd (∈ₛ⟪ fst B ⟫↪ (g i))

      δ : S ^ 3
      δ = B ∷ nn n ∷ envS g ∷ []

      E : Fin 3
      E = suc (suc zero)

    envOver : ⟨ δ ⊨ envOverAt E (suc zero) zero ⟩
    envOver = sv , (dom , (vals , pairs))
      where
      sv : ⟨ δ ⊨ svAt E ⟩
      sv = svAt-in E δ (λ x y y' p q →
        PT.rec (setIsSet (fst y) (fst y'))
          (λ { (i , ei) → PT.rec (setIsSet (fst y) (fst y'))
            (λ { (j , ej) → sym (pr-inj ei .snd)
               ∙ cong (λ k → fst (ix (g k)))
                   (inj-toℕ (#-inj′ (pr-inj ei .fst ∙ sym (pr-inj ej .fst))))
               ∙ pr-inj ej .snd })
            (out (pr (fst x) (fst y')) q) })
          (out (pr (fst x) (fst y)) p))

      dom : ⟨ δ ⊨ domAt E (suc zero) ⟩
      dom x = fwd , bwd
        where
        fwd : ⟨ (x ∷ δ) ⊨ inDomAt (suc E) zero ⟩ → ⟨ fst x ∈ (# n) ⟩
        fwd hd = PT.rec (snd (fst x ∈ (# n)))
          (λ { (y , p) → PT.rec (snd (fst x ∈ (# n)))
            (λ { (i , ei) → subst (λ w → ⟨ w ∈ (# n) ⟩) (pr-inj ei .fst)
                   (#mono (toℕ i) n (toℕ<n i)) })
            (out (pr (fst x) (fst y)) p) })
          (subst ⟨_⟩ (inDomAt-adequate (suc E) zero (x ∷ δ)) hd)

        bwd : ⟨ fst x ∈ (# n) ⟩ → ⟨ (x ∷ δ) ⊨ inDomAt (suc E) zero ⟩
        bwd hx = subst ⟨_⟩ (sym (inDomAt-adequate (suc E) zero (x ∷ δ)))
          (PT.map
            (λ { (m , m<n , e) →
              ix (g (fromℕ' n m m<n))
              , subst (λ w → ⟨ pr w (fst (ix (g (fromℕ' n m m<n))))
                                 ∈ fst (envS g) ⟩)
                  (cong #_ (toFromId' n m m<n) ∙ sym e) (into (fromℕ' n m m<n)) })
            (∈#-elim n (fst x) hx))

      vals : ⟨ δ ⊨ valuesInAt E zero ⟩
      vals x y hp = PT.rec (snd (fst y ∈ fst B))
        (λ { (i , ei) → subst (λ w → ⟨ w ∈ fst B ⟩) (pr-inj ei .snd) (val∈ i) })
        (out (pr (fst x) (fst y))
          (subst ⟨_⟩ (appAt-adequate (suc (suc E)) (suc zero) zero (y ∷ x ∷ δ))
            hp))

      pairs : ⟨ δ ⊨ pairsInAt E (suc zero) zero ⟩
      pairs = pairsIn-in E (suc zero) zero δ
        (λ s s∈ → PT.map
          (λ { (i , ei) → nn (toℕ i)
             , ( ix (g i)
               , ( #mono (toℕ i) n (toℕ<n i) , (val∈ i , sym ei) ) ) })
          (out (fst s) s∈))

    envSetIn : ⟨ (envS g ∷ []) ⊨ envFo n ⟩
    envSetIn = ∣ nn n , ∣ B , (refl , (refl , envOver)) ∣₁ ∣₁
```

## 要素から環境を復元する

逆に、要素 `x` が満たす `envOverAt` の四条件から関数 `g : Fin n → ⟪ B ⟫` が定まり、外延性によって `x` と `envS g` が同一視されます。

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

The other direction is what four clauses need when they read a bound variable
off an environment, and seven further clauses use it in a weaker form: a clause
binds its own ambient set and says only that its members are the environments,
so a proof that consumes the clause has to recognize that description as
**this** set. Both uses come from the same recovery, which is why it takes the
environment and the three slots as parameters rather than fixing them: a clause
places them where its own frame places them, not where this chapter would. A set satisfying the description is the graph of a function,
and recovering that function is the only place the four conjuncts must work
together: the domain conjunct says every index below the length has an entry,
and single-valuedness says there is at most one, so the existence of that entry
is a **proposition** and the truncation given by the domain conjunct can be
eliminated. Membership then names the index, which is untruncated because the
fibers of a set's own indexing are.

</details>

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

Extensionality completes the proof: one direction comes from the entries and
the other from the pairs conjunct, which is the conjunct without which
unwanted elements could enter.

</details>

```agda
  module Recover (n : ℕ) {k : ℕ} (γ : S ^ k) (Ei di bi : Fin k)
    (qd : fst (lookup di γ) ≡ # n) (qb : fst (lookup bi γ) ≡ fst B)
    (h : ⟨ γ ⊨ envOverAt Ei di bi ⟩)
    where
    private
      e : S
      e = lookup Ei γ

      Entry : Fin n → Type (ℓ-suc ℓ)
      Entry i = Σ[ y ∈ S ] ⟨ pr (# (toℕ i)) (fst y) ∈ fst e ⟩

      isPropEntry : (i : Fin n) → isProp (Entry i)
      isPropEntry i (y , p) (y' , p') =
        Σ≡Prop (λ w → snd (pr (# (toℕ i)) (fst w) ∈ fst e))
          (Σ≡Prop (λ v → snd (isL v))
            (svAt-out Ei γ (envOver-sv Ei di bi γ h)
              (nn (toℕ i)) y y' p p'))

      entry : (i : Fin n) → Entry i
      entry i = PT.rec (isPropEntry i) (λ z → z)
        (domAt-in Ei di γ (envOver-dom Ei di bi γ h)
          (nn (toℕ i)) (subst (λ z → ⟨ (# (toℕ i)) ∈ z ⟩) (sym qd)
            (#mono (toℕ i) n (toℕ<n i))))

      fib : (i : Fin n) → Σ[ m ∈ ⟪ fst B ⟫ ] (⟪ fst B ⟫↪ m ≡ fst (entry i .fst))
      fib i = ∈-asFiber {a = fst (entry i .fst)} {b = fst B}
        (subst (λ z → ⟨ fst (entry i .fst) ∈ z ⟩) qb
          (valuesInAt-out Ei bi γ (envOver-values Ei di bi γ h)
            (nn (toℕ i)) (entry i .fst) (entry i .snd)))

    g : Ix n
    g i = fib i .fst

    private
      val≡ : (i : Fin n) → fst (ix (g i)) ≡ fst (entry i .fst)
      val≡ i = fib i .snd

      fwd : (w : V ℓ) → ⟨ w ∈ fst (envS g) ⟩ → ⟨ w ∈ fst e ⟩
      fwd w = PT.rec (snd (w ∈ fst e))
        (λ { (li , q) → subst (λ z → ⟨ z ∈ fst e ⟩)
               (cong (pr (# (toℕ (lower li)))) (sym (val≡ (lower li))) ∙ q)
               (entry (lower li) .snd) })

      bwd : (w : V ℓ) → ⟨ w ∈ fst e ⟩ → ⟨ w ∈ fst (envS g) ⟩
      bwd w hw = PT.rec squash₁
        (λ { (u , (v , (u∈ , (v∈ , eq)))) → PT.rec squash₁
          (λ { (m , (m<n , um)) →
            let i = fromℕ' n m m<n
                iu : # (toℕ i) ≡ fst u
                iu = cong #_ (toFromId' n m m<n) ∙ sym um
                hv : ⟨ pr (# (toℕ i)) (fst v) ∈ fst e ⟩
                hv = subst (λ z → ⟨ z ∈ fst e ⟩)
                       (eq ∙ cong (λ z → pr z (fst v)) (sym iu)) hw
                same : fst v ≡ fst (entry i .fst)
                same = svAt-out Ei γ (envOver-sv Ei di bi γ h)
                         (nn (toℕ i)) v (entry i .fst) hv (entry i .snd)
            in ∣ lift i , cong (pr (# (toℕ i))) (val≡ i ∙ sym same)
                        ∙ cong (λ z → pr z (fst v)) iu ∙ sym eq ∣₁ })
          (∈#-elim n (fst u) (subst (λ z → ⟨ fst u ∈ z ⟩) qd u∈)) })
        (pairsIn-out Ei di bi γ
          (envOver-pairs Ei di bi γ h)
          (w , isL-trans {x = fst e} {y = w} hw (snd e)) hw)

    recovers : fst e ≡ fst (envS g)
    recovers = extensionalV (λ w → ⇔toPath (bwd w) (fwd w))

  envSet-in : {n : ℕ} (g : Ix n) → ⟨ envS g ∈ˢ envSet n ⟩
  envSet-in {n} g = subst ⟨_⟩ (sym (envSet-mem n (envS g)))
    (sf n .snd .snd g , envSetIn g)

  envSet-out : (n : ℕ) (x : S) → ⟨ x ∈ˢ envSet n ⟩
             → ∥ (Σ[ g ∈ Ix n ] (fst x ≡ fst (envS g))) ∥₁
  envSet-out n x hx = PT.rec squash₁
    (λ { (d , hd) → PT.map
      (λ { (b , (qd , (qb , hov))) →
        Recover.g n (b ∷ d ∷ x ∷ []) (suc (suc zero)) (suc zero) zero qd qb hov
        , Recover.recovers n (b ∷ d ∷ x ∷ []) (suc (suc zero)) (suc zero) zero
            qd qb hov })
      hd })
    (subst ⟨_⟩ (envSet-mem n x) hx .snd)
```

## まとめ

二方向は `envSet n` を特徴づけます。その要素であることは `B` に値を取る長さ `n` の割当てのグラフであることと同値なので、後の構成は `L` 内で環境を量化できます。

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

`envSet` is the ambient set the negative clauses take their complements
in, and it reads both ways: `envSet-in` puts every environment over the
carrier into it, `envSet-out` recovers from any member the function whose
graph it is. The second is what four clauses want when they read a bound variable
off an environment, and it is the one that needed all four conjuncts of the
description at once.

</details>

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

Two measurements, and the second is a sharper form of a rule the development
already had. Proving the fourth conjunct with the environment written out **did
not finish in ten minutes**; proving the same statement as a lemma whose
environment is a *variable*, then applying it, takes no measurable time. A
satisfaction substitution along an adequacy equation must be discharged where the
arguments are variables: at concrete elements it drags the whole absoluteness
bridge through normalization, and the elements' constructibility certificates
with it. Sealing the certificate at the construction site was necessary and not
sufficient. The recovery is written the same way, with the description's two
constant slots left as parameters constrained by equations rather than written in,
so that nothing substitutes underneath a satisfaction at a concrete environment.

</details>