Read this chapter directly, or use the interactive contents and dependency graph to choose another route.

Interactive contents · Dependency graph

Everything in this chapter takes place at a single type-theoretic universe level ℓ, fixed once and used throughout. The hierarchy V ℓ of sets at this level is the target of the eventual coding, and the first-order language is the setting in which parameters live. The plan is uniform: given a constructible set W, read its members as constant symbols, name them by abstract indices, and transport each name to the set it denotes in V ℓ. Nothing in that plan depends on which W is chosen, so it is carried out for an arbitrary W.

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

A statement about a constructible set W typically mentions members of W: to say, for instance, that some x in W satisfies a property, the formula carries x as a parameter. Internally, such parameters appear as constant symbols of a first-order language. The ambient coding of syntax, however, expects constants that are sets of the hierarchy V ℓ, not abstract references to members of an arbitrary set. So a bridge is needed: a language whose alphabet indexes the members of W, together with an embedding that gives each index its denotation as a set.

This chapter builds that bridge for a fixed W. The alphabet is the type of member indices of the underlying set of W; the embedding sends each index to the set it designates, and supplies a certificate that this set is a member of W. Relabeling constants along the embedding turns every term and formula over the alphabet into syntax over sets, to which the existing V-valued coding applies, yielding the term code ct and the formula code cd. Because the coding ignores arities, transporting a formula across an equality of arities leaves its code unchanged, as cd-subst records.

open import Cubical.Foundations.Prelude using ( J; substRefl )

The object-language syntax is generic in its alphabet. A type Formula K n of formulas over constants K and arity n never inspects what the constants are; it only arranges them into logical structure. Consequently, any function on the alphabet extends to a relabeling of syntax: mapping each constant through the function rewrites every occurrence while leaving connectives, quantifiers and variables untouched. Here the function will be the embedding of member indices into V ℓ, and the relabeled formulas will have sets as constants, which is precisely the input format of the set-valued syntax coding over the hierarchy. What remains is to choose the alphabet and the embedding so that the constants are genuinely the members of W.

Two distinctions organize the construction. First, a member of a set of the hierarchy is presented by an abstract index q in ⟪ a ⟫, and the embedding ⟪ a ⟫↪ sends that index to the set it designates; the index is a name, the value ⟪ a ⟫↪ q is the denotation in V ℓ, and the two roles are kept apart. Second, W is not an arbitrary set but an element of the carrier S of the constructible structure, so it comes with an underlying set W .fst of the hierarchy and a constructibility certificate; this is what licenses reading its members as parameters of a language about constructible sets. The alphabet will be ⟪ W .fst ⟫ itself, and the next section assembles these pieces into the codes ct and cd.

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties using
  ( ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )

open hPropView 𝒮ʟ using ( S )

Embedding constants and coding syntax

The section fixes a constructible set W as an element of the carrier S and asks how to code syntax over W as sets. Three steps compose: extract the type Ab of available constant symbols, embed each symbol into the hierarchy V ℓ with a certificate that it lies in W, and then apply the set-valued coding to the relabeled terms and formulas. The final lemma disposes of a bookkeeping issue arising because formulas are indexed by their arity.

An element W : S packages a set of the hierarchy with structure data; W .fst is its underlying set. The type Ab is then ⟪ W .fst ⟫, the type of indices for members of that set, and ι is the embedding ⟪ W .fst ⟫↪ that sends each index to the member it designates inside V ℓ. So an inhabitant of Ab is exactly an available constant symbol, and ι computes its denotation as a set.

module Alphabet (W : S) where

Ab : Type ℓ
Ab = ⟪ W .fst ⟫

ι : Ab → V ℓ
ι = ⟪ W .fst ⟫↪

The membership certificate ι∈ says that for every constant symbol q, the set ι q genuinely is a member of W .fst; it is read off from the library's equivalence between membership and the classified membership relation ∈ₛ. With the alphabet in place, cd and ct are now almost forced: mapFo ι and mapTm ι rewrite a formula or term by replacing each constant con q with con (ι q), and the brackets ⌜_⌝ and ⌜_⌝ᵗ from the hierarchy coding then package the result as a set. The logical skeleton of the formula survives the relabeling untouched, which is exactly why the coding can be reused.

ι∈ : (q : Ab) → ⟨ ι q ∈ W .fst ⟩
ι∈ q = ∈∈ₛ {a = ι q} {b = W .fst} .snd (∈ₛ⟪ W .fst ⟫↪ q)

cd : ∀ {n} → Formula Ab n → V ℓ
cd ψ = VCode.⌜ mapFo ι ψ ⌝

ct : ∀ {n} → Term Ab n → V ℓ

A formula of type Formula Ab n carries an arity n, and in dependent type theory that index is part of the type. If a proof later needs n and n' to be equal, it transports the formula along a path e : n ≡ n', and the transported formula is a different inhabitant syntactically even when the underlying formula is the same. The lemma cd-subst shows that this makes no difference for coding: cd applied to the transported formula equals cd applied to the original. The proof is by J on e, where the reflexive case holds because transporting along refl is the identity and substRefl makes that reduction explicit, leaving cong cd to equate the two applications.

ct t = VCode.⌜ mapTm ι t ⌝ᵗ

cd-subst : ∀ {n n'} (e : n ≡ n') (ψ : Formula Ab n) → cd (subst (Formula Ab) e ψ) ≡ cd ψ
cd-subst {n} e ψ = J (λ n' e' → cd (subst (Formula Ab) e' ψ) ≡ cd ψ)
  (cong cd (substRefl {B = Formula Ab} ψ)) e

Recap

Alphabet W regards the members of a constructible set W as the constant symbols of a first-order language, embeds each of them into the ambient hierarchy with the certificate ι∈, and returns the resulting set codes of terms and formulas through ct and cd. Because the coding never inspects the arity, cd-subst guarantees that transporting a formula across an equality of arities does not change its code.