整形式な構成子キーの認識

この章を読むか、読書案内と依存マップで別のルートを選べます。

読書案内 · 依存マップ

符号が整形式であるとは、項または論理式のいずれかの構成子の形を持ち、そのペイロードが所定の枠に収まることです。十通りの形の述語を定義し、その平坦な証人による特徴付けを双方向で示し、項の符号と直下の部分符号を復元または構成します。

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

open import Base.Prelude

module L.Coding.CodeShape {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Term; Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊤̇; ⊥̇
        ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; #mono; module VCode )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; sucV )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Expressions {ℓ} using ( tagAtL; tagAtL-adequate; arityTagAtL; arityTagAtL-adequate; arityTagPairAtL; arityTagPairAtL-adequate; numL )
open import L.Coding.Closure {ℓ} using ( closedAt; binShapeAt; unShapeAt; bothSameAt; oneSameAt; oneSuccAt; succSndAt; binSameClosed-out; unSameClosed-out; unSuccClosed-out; binSuccClosed-out )
open import L.Coding.CodeConstructibility {ℓ} using ( closure-inv; key; codeL; codeTmL )
open import L.Coding.SubformulaClosure {ℓ} using ( clo )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Ordinal {ℓ} using ( ∈#-elim )

open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( fromℕ'; toFromId'; toℕ<n )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
import Cubical.Data.Sum as Sum
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )

open hPropStructure 𝒮ʟ

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

二つのペイロード枠

単項構成子と二項構成子では、キーに格納する部分符号の数が異なります。二つの枠はタグ、アリティ、項または論理式の部分符号を所定の位置に配置します。

module _ {n : ℕ} where
  binForm : ℕ → Formula S (4 + n) → Formula S (suc n)
  binForm k rel = ∃̇ (∃̇ (∃̇ (arityTagPairAtL
    (suc (suc (suc zero))) (suc (suc zero)) k (suc zero) zero ∧̇ rel)))

  unForm : ℕ → Formula S (3 + n) → Formula S (suc n)
  unForm k rel = ∃̇ (∃̇ (arityTagAtL (suc (suc zero)) (suc zero) k zero ∧̇ rel))

項の符号

定数項と変数項のキーを、それぞれタグとペイロードの形で認識します。isTmAt は二つの場合を一つの対象言語の述語にまとめます。

英語原文

A variable's index must lie below the arity, which is what makes the formula the code of a term at that arity rather than at some larger one. A constant must be a member of the carrier, which is what makes it the code of a term over that alphabet rather than over the whole model. This second conjunct is the one the code set was caught between two statements without: with no bound on a constant, a payload read back as one is an arbitrary element of L, and the class the decode lands in is wider than the class the introduction starts from.

英語原文

Both bounds are memberships at a slot, and both slots are named by the caller. The carrier is a slot rather than a constant on purpose. A constant would pin every predicate below this line to one carrier, and everything indexed by them would be re-indexed at the pair; a slot is threaded, and threading is free.

isTmAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
isTmAt t N A = ∃̇ (tagAtL (suc t) 0 zero ∧̇ (var zero ∈̇ var (suc A)))
            ∨̇ ∃̇ (tagAtL (suc t) 1 zero ∧̇ (var zero ∈̇ var (suc N)))

十個の形を一つの述語にする

原子、二項結合子、偽、量化子、有界量化子の十個の論理式構成子を一つの選言的な形の述語にまとめます。各枝は対応するタグとペイロード枠を検査します。

英語原文

Being shaped is therefore relative to two slots and not one: the set, and the carrier its terms name their constants from. Only the four relations that mention a term look at the second, and they are the only four that could.

module _ {n : ℕ} where
  bothTm fstTm : Fin n → Formula S (4 + n)
  bothTm A = isTmAt (suc zero) (suc (suc zero)) (suc (suc (suc (suc A))))
          ∧̇ isTmAt zero (suc (suc zero)) (suc (suc (suc (suc A))))
  fstTm  A = isTmAt (suc zero) (suc (suc zero)) (suc (suc (suc (suc A))))

  noneB : Formula S (4 + n)
  noneB = ⊤̇ {n = 4 + n}

  zeroPay noneU : Formula S (3 + n)
  zeroPay = var zero ≐ con (numeralL 0)
  noneU   = ⊤̇ {n = 3 + n}

  shapes : Fin n → Formula S (suc n)
  shapes A = binForm 0 (bothTm A) ∨̇ (binForm 1 (bothTm A)
           ∨̇ (binForm 2 noneB ∨̇ (binForm 3 noneB ∨̇ (binForm 4 noneB
           ∨̇ (unForm 5 zeroPay ∨̇ (unForm 6 noneU ∨̇ (unForm 7 noneU
           ∨̇ (binForm 8 (fstTm A) ∨̇ binForm 9 (fstTm A)))))))))

  shapedAt : Fin n → Fin n → Formula S n
  shapedAt C A = ∀̇∈ (var C) (shapes A)

要素を平坦に読み出す

形の述語を満たすキーから、どの構成子であるか、そのタグ、アリティ、直下の部分符号を平坦な証人として取り出します。この除去形式は後の閉性証明で使いやすい形です。

BinWit : ∀ {n} → ℕ → Formula S (4 + n) → S ^ n → S → Type (ℓ-suc ℓ)
BinWit k rel γ c = Σ[ N ∈ S ] (Σ[ a ∈ S ] (Σ[ b ∈ S ]
  ((fst c ≡ pr (fst N) (pr (# k) (pr (fst a) (fst b))))
   × ⟨ (b ∷ a ∷ N ∷ c ∷ γ) ⊨ rel ⟩)))

UnWit : ∀ {n} → ℕ → Formula S (3 + n) → S ^ n → S → Type (ℓ-suc ℓ)
UnWit k rel γ c = Σ[ N ∈ S ] (Σ[ a ∈ S ]
  ((fst c ≡ pr (fst N) (pr (# k) (fst a))) × ⟨ (a ∷ N ∷ c ∷ γ) ⊨ rel ⟩))

binForm-out : ∀ {n} (k : ℕ) (rel : Formula S (4 + n)) (γ : S ^ n) (c : S)
            → ⟨ (c ∷ γ) ⊨ binForm k rel ⟩ → ∥ BinWit k rel γ c ∥₁
binForm-out k rel γ c = PT.rec squash₁ (λ { (N , hN) →
  PT.rec squash₁ (λ { (a , ha) → PT.map
    (λ { (b , (hb , hr)) → N , (a , (b , (subst ⟨_⟩
       (arityTagPairAtL-adequate (suc (suc (suc zero))) (suc (suc zero)) k
          (suc zero) zero (b ∷ a ∷ N ∷ c ∷ γ)) hb , hr))) })
    ha }) hN })

unForm-out : ∀ {n} (k : ℕ) (rel : Formula S (3 + n)) (γ : S ^ n) (c : S)
           → ⟨ (c ∷ γ) ⊨ unForm k rel ⟩ → ∥ UnWit k rel γ c ∥₁
unForm-out k rel γ c = PT.rec squash₁ (λ { (N , hN) → PT.map
  (λ { (a , (ha , hr)) → N , (a , (subst ⟨_⟩
     (arityTagAtL-adequate (suc (suc zero)) (suc zero) k zero
        (a ∷ N ∷ c ∷ γ)) ha , hr)) })
  hN })

ShapeWit : ∀ {n} → Fin n → S ^ n → S → Type (ℓ-suc ℓ)
ShapeWit A γ c =
    BinWit 0 (bothTm A) γ c ⊎ (BinWit 1 (bothTm A) γ c
  ⊎ (BinWit 2 noneB γ c ⊎ (BinWit 3 noneB γ c ⊎ (BinWit 4 noneB γ c
  ⊎ (UnWit 5 zeroPay γ c ⊎ (UnWit 6 noneU γ c ⊎ (UnWit 7 noneU γ c
  ⊎ (BinWit 8 (fstTm A) γ c ⊎ BinWit 9 (fstTm A) γ c))))))))

private
  sum-out : {A B C D : Type (ℓ-suc ℓ)}
          → (A → ∥ C ∥₁) → (B → ∥ D ∥₁) → ∥ A ⊎ B ∥₁ → ∥ C ⊎ D ∥₁
  sum-out f g = PT.rec squash₁
    (Sum.rec (λ x → PT.map inl (f x)) (λ y → PT.map inr (g y)))

  sum-in : {A B C D : Type (ℓ-suc ℓ)}
         → (A → C) → (B → D) → A ⊎ B → ∥ C ⊎ D ∥₁
  sum-in f g x = ∣ Sum.map f g x ∣₁

shaped-out : ∀ {n} (C A : Fin n) (γ : S ^ n) → ⟨ γ ⊨ shapedAt C A ⟩
           → (c : S) → ⟨ c ∈ˢ lookup C γ ⟩ → ∥ ShapeWit A γ c ∥₁
shaped-out C A γ h c c∈ = read (h c c∈)
  where
  read : ⟨ (c ∷ γ) ⊨ shapes A ⟩ → ∥ ShapeWit A γ c ∥₁
  read =
    sum-out (binForm-out 0 (bothTm A) γ c)
    (sum-out (binForm-out 1 (bothTm A) γ c)
    (sum-out (binForm-out 2 noneB γ c)
    (sum-out (binForm-out 3 noneB γ c)
    (sum-out (binForm-out 4 noneB γ c)
    (sum-out (unForm-out 5 zeroPay γ c)
    (sum-out (unForm-out 6 noneU γ c)
    (sum-out (unForm-out 7 noneU γ c)
    (sum-out (binForm-out 8 (fstTm A) γ c)
    (binForm-out 9 (fstTm A) γ c)))))))))

同じ十個の形を書き込む

各構成子に必要なタグとペイロードの等式が与えられれば、対応する形の述語を満たすことを示せます。これは平坦な証人から対象言語の充足関係への逆向きです。

英語原文

The two frames are introduced once each, generically in the relation, for the reason that decided the elimination and for one more. The adequacy equation each frame carries is discharged here, with the tag, the relation and the environment all still variables. Discharged at a named tag instead, it would be ten unfoldings of a formula three quantifiers deep, and that is the difference between a second and an afternoon.

binForm-in : ∀ {n} (k : ℕ) (rel : Formula S (4 + n)) (γ : S ^ n) (c : S)
           → BinWit k rel γ c → ⟨ (c ∷ γ) ⊨ binForm k rel ⟩
binForm-in k rel γ c (N , (a , (b , (e , hr)))) =
  ∣ N , ∣ a , ∣ b , (subst ⟨_⟩ (sym (arityTagPairAtL-adequate
     (suc (suc (suc zero))) (suc (suc zero)) k (suc zero) zero
     (b ∷ a ∷ N ∷ c ∷ γ))) e , hr) ∣₁ ∣₁ ∣₁

unForm-in : ∀ {n} (k : ℕ) (rel : Formula S (3 + n)) (γ : S ^ n) (c : S)
          → UnWit k rel γ c → ⟨ (c ∷ γ) ⊨ unForm k rel ⟩
unForm-in k rel γ c (N , (a , (e , hr))) =
  ∣ N , ∣ a , (subst ⟨_⟩ (sym (arityTagAtL-adequate
     (suc (suc zero)) (suc zero) k zero (a ∷ N ∷ c ∷ γ))) e , hr) ∣₁ ∣₁
英語原文

The walk over the disjunction mirrors its reading: each level injects one summand and carries its own truncation. The shared maps operate on semantic types, with each constructor's reader supplied explicitly. They never recover a formula from its meaning. The caller supplies exactly one thing per member: which of the ten shapes that member has.

shaped-in : ∀ {n} (C A : Fin n) (γ : S ^ n)
          → ((c : S) → ⟨ c ∈ˢ lookup C γ ⟩ → ∥ ShapeWit A γ c ∥₁)
          → ⟨ γ ⊨ shapedAt C A ⟩
shaped-in C A γ g c c∈ = PT.rec (snd ((c ∷ γ) ⊨ shapes A)) fill (g c c∈)
  where
  fill : ShapeWit A γ c → ⟨ (c ∷ γ) ⊨ shapes A ⟩
  fill =
    sum-in (binForm-in 0 (bothTm A) γ c)
    (sum-in (binForm-in 1 (bothTm A) γ c)
    (sum-in (binForm-in 2 noneB γ c)
    (sum-in (binForm-in 3 noneB γ c)
    (sum-in (binForm-in 4 noneB γ c)
    (sum-in (unForm-in 5 zeroPay γ c)
    (sum-in (unForm-in 6 noneU γ c)
    (sum-in (unForm-in 7 noneU γ c)
    (sum-in (binForm-in 8 (fstTm A) γ c)
    (binForm-in 9 (fstTm A) γ c)))))))))

項の復元

項の形を持つキーから、対応する実際の項と、その符号が元のキーに等しいという証明を復元します。定数と変数の二つの場合をタグの単射性で区別します。

英語原文

What the term is produced over is a parameter, and it is what the chapter is for. The alphabet is any type with an embedding into the hierarchy, and the constant case needs one thing the shape predicate cannot supply: that the carrier's members are the alphabet's image. That is a hypothesis, because it is a fact about the pair (alphabet, carrier) and not about the code. At the one instantiation that matters, the alphabet is the carrier's own member type and the hypothesis is the presentation of a set by its members, so it costs a discharge rather than a construction.

英語原文

The two disjuncts are read by two named lemmas and the reader is their case split, which is not a matter of taste. Written as two clauses of one function, each carrying its own truncation under a disjunction that also carries one, the chapter did not finish in ten minutes; with each disjunct's reading given a written type of its own it checks in under two seconds. The rule is the elaborator's, not the mathematics': a branch whose type is written is solved against that type, and a branch whose type is inferred is solved against the whole disjunction.

module _ {K : Type ℓ} (f : K → V ℓ) where

  TmWit : ℕ → V ℓ → Type (ℓ-suc ℓ)
  TmWit n x = Σ[ t ∈ Term K n ] (VCode.⌜ mapTm f t ⌝ᵗ ≡ x)

  Onto : ∀ {m} → Fin m → S ^ m → Type (ℓ-suc ℓ)
  Onto A γ = (y : V ℓ) → ⟨ y ∈ fst (lookup A γ) ⟩ → ∥ Σ[ c ∈ K ] (f c ≡ y) ∥₁

  tmCon : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ) → Onto A γ
        → ⟨ γ ⊨ ∃̇ (tagAtL (suc t) 0 zero ∧̇ (var zero ∈̇ var (suc A))) ⟩
        → ∥ TmWit n (fst (lookup t γ)) ∥₁
  tmCon t N A γ n onto = PT.rec squash₁
    (λ { (y , (hy , y∈)) → PT.map
         (λ { (c , qc) → con c
            , ( cong (VCode.mkTag 0) qc ∙ sym
                (subst ⟨_⟩ (tagAtL-adequate (suc t) 0 zero (y ∷ γ)) hy) ) })
         (onto (fst y) y∈) })

  tmVar : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ)
        → fst (lookup N γ) ≡ # n
        → ⟨ γ ⊨ ∃̇ (tagAtL (suc t) 1 zero ∧̇ (var zero ∈̇ var (suc N))) ⟩
        → ∥ TmWit n (fst (lookup t γ)) ∥₁
  tmVar t N A γ n qN = PT.rec squash₁
    (λ { (z , (hz , z∈)) → PT.map
         (λ { (j , (j<n , ez)) →
           var (fromℕ' n j j<n)
           , ( cong (VCode.mkTag 1) (cong #_ (toFromId' n j j<n) ∙ sym ez)
             ∙ sym (subst ⟨_⟩ (tagAtL-adequate (suc t) 1 zero (z ∷ γ)) hz) ) })
         (∈#-elim n (fst z) (subst (λ w → ⟨ fst z ∈ w ⟩) qN z∈)) })

  isTmAt-decode : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ)
                → fst (lookup N γ) ≡ # n → Onto A γ
                → ⟨ γ ⊨ isTmAt t N A ⟩ → ∥ TmWit n (fst (lookup t γ)) ∥₁
  isTmAt-decode t N A γ n qN onto = PT.rec squash₁
    (λ { (inl h) → tmCon t N A γ n onto h
       ; (inr h) → tmVar t N A γ n qN h })

項の符号化

逆に、任意の項の符号は項の形の述語を満たします。項の二つの構成子を調べ、対応するタグとペイロードの証人を直接与えます。

module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where

  isTmAt-in : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ)
            → fst (lookup N γ) ≡ # n
            → ((c : K) → ⟨ f c ∈ fst (lookup A γ) ⟩)
            → TmWit f n (fst (lookup t γ)) → ⟨ γ ⊨ isTmAt t N A ⟩
  isTmAt-in t N A γ n qN into (con c , e) = ∣ inl ∣ y
    , ( subst ⟨_⟩ (sym (tagAtL-adequate (suc t) 0 zero (y ∷ γ))) (sym e)
      , into c ) ∣₁ ∣₁
    where
    y : S
    y = f c , h c
  isTmAt-in t N A γ n qN into (var i , e) = ∣ inr ∣ z
    , ( subst ⟨_⟩ (sym (tagAtL-adequate (suc t) 1 zero (z ∷ γ)))
          (sym e ∙ cong (VCode.mkTag 1) (sym (numeralL-fst (toℕ i))))
      , subst (λ w → ⟨ fst z ∈ w ⟩) (sym qN)
          (subst (λ w → ⟨ w ∈ (# n) ⟩) (sym (numeralL-fst (toℕ i)))
            (#mono (toℕ i) n (toℕ<n i))) ) ∣₁ ∣₁
    where
    z : S
    z = numeralL (toℕ i)

一層分の部分符号

論理式の符号から、その最外構成子が指す直下の項と論理式の符号を取り出します。これは構文木を一層だけ進む操作で、閉性述語が要求する部分符号を与えます。

英語原文

The equation shapedness produces is, letter for letter, the one closedness consumes, so the two compose with nothing in between. That is not luck: both were written against the same reading of an arity-tagged pair.

module Peel {m : ℕ} (C A : Fin m) (γ : S ^ m)
            (hcl : ⟨ γ ⊨ closedAt C ⟩) (hsh : ⟨ γ ⊨ shapedAt C A ⟩) where
  private
    D : V ℓ
    D = fst (lookup C γ)

  BinSame BinSucc : ℕ → S → Type (ℓ-suc ℓ)
  BinSame k c = Σ[ N ∈ S ] (Σ[ a ∈ S ] (Σ[ b ∈ S ]
    ((fst c ≡ pr (fst N) (pr (# k) (pr (fst a) (fst b))))
     × (⟨ pr (fst N) (fst a) ∈ D ⟩ × ⟨ pr (fst N) (fst b) ∈ D ⟩))))
  BinSucc k c = Σ[ N ∈ S ] (Σ[ a ∈ S ] (Σ[ b ∈ S ]
    ((fst c ≡ pr (fst N) (pr (# k) (pr (fst a) (fst b))))
     × (⟨ (a ∷ N ∷ c ∷ γ) ⊨ isTmAt zero (suc zero) (suc (suc (suc A))) ⟩
        × ⟨ pr (sucV (fst N)) (fst b) ∈ D ⟩))))

  UnSame UnSucc : ℕ → S → Type (ℓ-suc ℓ)
  UnSame k c = Σ[ N ∈ S ] (Σ[ a ∈ S ]
    ((fst c ≡ pr (fst N) (pr (# k) (fst a))) × ⟨ pr (fst N) (fst a) ∈ D ⟩))
  UnSucc k c = Σ[ N ∈ S ] (Σ[ a ∈ S ]
    ((fst c ≡ pr (fst N) (pr (# k) (fst a))) × ⟨ pr (sucV (fst N)) (fst a) ∈ D ⟩))

  PeelWit : S → Type (ℓ-suc ℓ)
  PeelWit c =
      BinWit 0 (bothTm A) γ c ⊎ (BinWit 1 (bothTm A) γ c
    ⊎ (BinSame 2 c ⊎ (BinSame 3 c ⊎ (BinSame 4 c
    ⊎ (UnWit 5 zeroPay γ c ⊎ (UnSucc 6 c ⊎ (UnSucc 7 c
    ⊎ (BinSucc 8 c ⊎ BinSucc 9 c))))))))

  peel : (c : S) → ⟨ c ∈ˢ lookup C γ ⟩ → ∥ PeelWit c ∥₁
  peel c c∈ = PT.map fill (shaped-out C A γ hsh c c∈)
    where
    bs : (k : ℕ) → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩ → BinWit k noneB γ c
       → BinSame k c
    bs k h (N , (a , (b , (e , _)))) =
      N , (a , (b , (e , binSameClosed-out C k γ h c N a b c∈ e)))

    us : (k : ℕ) → ⟨ γ ⊨ unShapeAt C k (oneSameAt C) ⟩ → UnWit k noneU γ c
       → UnSame k c
    us k h (N , (a , (e , _))) =
      N , (a , (e , unSameClosed-out C k γ h c N a c∈ e))

    uz : (k : ℕ) → ⟨ γ ⊨ unShapeAt C k (oneSuccAt C) ⟩ → UnWit k noneU γ c
       → UnSucc k c
    uz k h (N , (a , (e , _))) =
      N , (a , (e , unSuccClosed-out C k γ h c N a c∈ e))

    bz : (k : ℕ) → ⟨ γ ⊨ binShapeAt C k (succSndAt C) ⟩ → BinWit k (fstTm A) γ c
       → BinSucc k c
    bz k h (N , (a , (b , (e , hr)))) =
      N , (a , (b , (e , (hr , binSuccClosed-out C k γ h c N a b c∈ e))))

    fill : ShapeWit A γ c → PeelWit c
    fill =
      Sum.map id
      (Sum.map id
      (Sum.map (bs 2 (hcl .fst))
      (Sum.map (bs 3 (hcl .snd .fst))
      (Sum.map (bs 4 (hcl .snd .snd .fst))
      (Sum.map id
      (Sum.map (uz 6 (hcl .snd .snd .snd .fst))
      (Sum.map (uz 7 (hcl .snd .snd .snd .snd .fst))
      (Sum.map (bz 8 (hcl .snd .snd .snd .snd .snd .fst))
      (bz 9 (hcl .snd .snd .snd .snd .snd .snd))))))))))

閉じた領域の符号は整形式である

閉じた符号領域の各要素には、十個の構成子のいずれかに対応する形の証人があります。この定理が領域の所属から実際の論理式の復号へ進む入口になります。

英語原文

The analysis is on the constructor alone. The tag is not a second index to be matched against: it is computed from the constructor, exactly as byTag computes the closedness demand from it, so the table is ten lines and not ten times ten. Nothing here recurses either, because the key of a named constructor already computes to the arity-tagged pair the witness type asks for, and no transport is needed anywhere in the ten tuples.

英語原文

The one thing a tuple cannot compute is the term witness: a payload slot holding a term code must be certified as one, and the certificate is the encoder above applied to the term the constructor carries. That certificate now has a second half, supplied by the caller: every constant of the alphabet is a member of the carrier. It is one hypothesis, discharged once per call rather than once per constructor, because the alphabet is fixed before the formula is.

英語原文

The first half, on the other hand, becomes easier. The witness a term owes is that its code is the code of some term, and over the alphabet the code of a term already is that: the encoder is the identity with refl beside it. On the model's own coding it must first establish a correspondence between the two codings.

module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where
  private
    cd : ∀ {n} → Formula K n → S
    cd φ = VCode.⌜ mapFo f φ ⌝ , codeL f h φ

    ct : ∀ {n} → Term K n → S
    ct t = VCode.⌜ mapTm f t ⌝ᵗ , codeTmL f h t

    nn : ℕ → S
    nn n = # n , numL n

    tw : ∀ {n} (t : Term K n) → TmWit f n (fst (ct t))
    tw t = t , refl

  closureShaped : ∀ {n m} (φ : Formula K n) (A : Fin m) (γ : S ^ m)
                → ((k : K) → ⟨ f k ∈ fst (lookup A γ) ⟩)
                → ⟨ (clo f h φ ∷ γ) ⊨ shapedAt zero (suc A) ⟩
  closureShaped φ A γ into = shaped-in zero (suc A) (clo f h φ ∷ γ)
    (λ c c∈ → PT.map (λ { (_ , ψ , q , _) → go ψ c q })
      (closure-inv f h φ (fst c) c∈))
    where
    tm1 : ∀ {k} (t : Term K k) (b c : S)
        → ⟨ (b ∷ ct t ∷ nn k ∷ c ∷ clo f h φ ∷ γ)
            ⊨ isTmAt (suc zero) (suc (suc zero))
                (suc (suc (suc (suc (suc A))))) ⟩
    tm1 {k} t b c = isTmAt-in f h (suc zero) (suc (suc zero))
      (suc (suc (suc (suc (suc A)))))
      (b ∷ ct t ∷ nn k ∷ c ∷ clo f h φ ∷ γ) k refl into (tw t)

    tm0 : ∀ {k} (u : Term K k) (a c : S)
        → ⟨ (ct u ∷ a ∷ nn k ∷ c ∷ clo f h φ ∷ γ)
            ⊨ isTmAt zero (suc (suc zero))
                (suc (suc (suc (suc (suc A))))) ⟩
    tm0 {k} u a c = isTmAt-in f h zero (suc (suc zero))
      (suc (suc (suc (suc (suc A)))))
      (ct u ∷ a ∷ nn k ∷ c ∷ clo f h φ ∷ γ) k refl into (tw u)

    go : ∀ {k} (ψ : Formula K k) (c : S) → fst c ≡ key f h ψ
       → ShapeWit (suc A) (clo f h φ ∷ γ) c
    go {k} (t ∈̇ u) c q =
      inl (nn k , (ct t , (ct u , (q , (tm1 t (ct u) c , tm0 u (ct t) c)))))
    go {k} (t ≐ u) c q =
      inr (inl
        (nn k , (ct t , (ct u , (q , (tm1 t (ct u) c , tm0 u (ct t) c))))))
    go {k} (a ∧̇ b) c q = inr (inr (inl (nn k , (cd a , (cd b , (q , (λ z → z)))))))
    go {k} (a ∨̇ b) c q =
      inr (inr (inr (inl (nn k , (cd a , (cd b , (q , (λ z → z))))))))
    go {k} (a ⇒̇ b) c q =
      inr (inr (inr (inr (inl (nn k , (cd a , (cd b , (q , (λ z → z)))))))))
    go {k} ⊥̇ c q =
      inr (inr (inr (inr (inr (inl (nn k , (nn 0 , (q , sym (numeralL-fst 0)))))))))
    go {k} (∃̇ a) c q =
      inr (inr (inr (inr (inr (inr (inl (nn k , (cd a , (q , (λ z → z))))))))))
    go {k} (∀̇ a) c q =
      inr (inr (inr (inr (inr (inr (inr (inl (nn k , (cd a , (q , (λ z → z)))))))))))
    go {k} (∀̇∈ t a) c q =
      inr (inr (inr (inr (inr (inr (inr (inr (inl
        (nn k , (ct t , (cd a , (q , tm1 t (cd a) c))))))))))))
    go {k} (∃̇∈ t a) c q =
      inr (inr (inr (inr (inr (inr (inr (inr (inr
        (nn k , (ct t , (cd a , (q , tm1 t (cd a) c))))))))))))