BedrockLocating the hull and its collapse inside L
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapThe condensation argument needs more than an external hull: the hull itself and every value of its collapse must belong to L. This chapter proves these membership facts by coding the collapse and expressing the hull as an ω-iteration.
{-# OPTIONS --cubical --safe --guardedness #-}
The chapter runs under classical logic: an excluded-middle instance at the successor of the model's own level. This is the same hypothesis the choice construction carries, and it is the only classical assumption made here.
open import Base.Prelude open import Base.Classical using ( LEM )
The module is parameterized by that hypothesis, so every statement below is relative to it rather than to an ambient principle of excluded middle.
module L.GCH.ConstructibleHull {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
The chapter speaks the first-order language of set theory: formulas are built over the carrier of the constructible structure, their constants name elements of L, and constants can be relabeled along any map, with satisfaction invariant under such relabeling. This is the vocabulary in which the collapse and the hull will be described.
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ∃̇_; ∀̇_; ∀̇∈; ⊥̇ ) open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp ) open import FOL.Manipulation.Relabelling using ( ⊨-map )
Formula readings move between environments by renaming, and renaming is harmless for satisfaction. The ambient hierarchy contributes the background facts: induction along membership, extensionality of sets, and the presentation of an element as an index together with its membership proof.
open import FOL.Manipulation.Renaming using ( renameFo; module Sat ) import FOL.Absoluteness import FOL.Semantics open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV ) open import V.Presentation {ℓ} using ( member; fiber )
The argument begins where every set of L lives: in the tower of stages indexed by ordinals. The collapse of a set is computed from its members alone, and constructibility travels along membership; what must be shown is that this local computation never leaves L. Since a hull is not transitive, the argument cannot invoke global facts about the collapse; it re-derives, stage by stage, that the values stay inside.
open import V.Coding {ℓ} using ( pr; module VCode ) open import V.Collapse {ℓ} using ( module Collapse ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-out; Lset→isL; 𝒟ₒ; 𝒟ₒ∋⊆ ; Lset-layer; layer-trans )
The constructible set ωʟ represents the ambient ω, and its specification identifies its members with the internal numerals. Separation will carve the bounded slices and one-step closures used later. In both operations the result is an element of L again, which is what keeps the whole construction inside the universe it describes.
open import L.Ordinal {ℓ} using ( mem-ord; #∈ω ) open import L.Axioms.Basic {ℓ} using ( LsetS; ∅ʟ; extensionalL ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL ) open import L.Axioms.Infinity {ℓ} lem using ( ωʟ; ω-specL ) open import L.Axioms.Numerals {ℓ} using ( numeralL-fst )
Replacement assembles values into tables: a recursion whose graph is definable becomes an element of L, and it suffices that a unique value merely exists at each argument. Definability interprets the constants of formulas, and the model-side coding of pairs and numerals provides the entries and their names.
open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct ) open import L.Recursion.Graph {ℓ} lem using () renaming ( module Graph to RecursionGraph ) open import L.Definability {ℓ} using ( module DefOf ) open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; envOverAt; envOverAt-transport ) open import L.Coding.Expressions {ℓ} using ( numL; sucAtL; sucAtL-adequate; consAtL; consAtL-adequate )
Environments code parameter vectors as single sets, from which the vectors are recovered; the satisfaction bridge reads internal satisfaction externally; the code set gathers all codes into one element of L; and constructible unions combine the pieces that the construction collects along the way.
open import L.Coding.Environment {ℓ} using ( env; cons ) open import L.Coding.EnvironmentSet {ℓ} lem using ( envS; Ix; envOver; module Recover ) open import L.Coding.SatisfactionBridge {ℓ} lem using ( graph; envFor; envFor-graph ) open import L.Coding.CodeSet {ℓ} lem using ( AllCodes; keyS; key∈AllCodes ) open import L.Coding.CodeConstructibility {ℓ} using ( cupʟ; cupʟ-inl; cupʟ-inr )
The uniform satisfaction table assigns to every code its satisfaction set, read externally; the canonical-names construction places numerals and the codes of parameter-free formulas, which may still have free-variable slots, in Lset ω; the internal well-order of a stage compares its members, first by birth stage and then by name.
open import L.Coding.UniformSatisfaction {ℓ} lem using ( val-sat ) open import L.Choice.CanonicalNames {ℓ} lem using ( limitCode; numeral∈limit; pr∈limit ) open import L.Choice.NameComparison {ℓ} lem using ( freeCode-in; freeCode-out ) open import L.Choice.InternalWellOrder {ℓ} lem using ( relL; relL-fill; relL-rep ) open import L.Choice.StageOrders {ℓ} lem using ( orderAt; relOf )
Least-element search over a strict well-order returns, from an inhabited family, the least element; relations themselves become sets of pairs with two readings, and the order-type chapter states the three predicates describing a collapse table.
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; IsLeast; leastOf; isPropLeastOf ) renaming ( Tri to Tri∙; lt to tri-lt; eq to tri-eq; gt to tri-gt ) open import L.GCH.CardinalSquareLaw {ℓ} lem using ( module Relation; isL-ord ) open import L.GCH.OrderType {ℓ} lem
Correctness, completeness at an argument, and the value clause are each a formula with its two satisfaction readings; internal ω-recursion iterates a definable two-place step along the model's own ω. The hull's members are named by codes of arbitrary nesting depth, so no single separation can produce the hull; it is reached by iterating a definable one-step closure along ω, and this is why the closure must be built ω times.
using ( Holds; Complete; Src; ValueIs; Correct ; completeAt; complete-in; complete-out ; valueAt; value-in; value-out ; correctAt; correct-in; correct-out ) open import L.GCH.OmegaRecursion {ℓ} lem using ( module Iterate )
The proof has two connected parts. First, a local collapse table shows that each collapse value of a constructible carrier is constructible. Second, the Skolem hull is realized as the union of its finite closure stages, making the carrier itself constructible and allowing the first argument to apply to it.
open import L.GCH.SkolemHull {ℓ} lem using ( module HullStage; module Frame ) open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate ) open import L.GCH.AdequateStages {ℓ} lem using ( Superadequate ) open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph ) open import L.GCH.CondensationTransfer {ℓ} lem using ( module Condense )
A nested hull code has a finite depth, computed by taking maxima over the depths of its parameter codes. This depth bounds the closure stage at which its value appears.
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop ) open import Cubical.Data.Nat.Properties using ( max ) open import Cubical.Data.Nat.Order using ( _≤_; left-≤-max; right-≤-max ) open import Cubical.Data.Sum using ( _⊎_; inl; inr ) import Cubical.Data.Sum as Sum
Finite parameter vectors let one witness code depend on finitely many earlier values. Empty sets, singletons and unordered pairs provide the set codes needed to represent those parameters and their ordered pairs inside the hierarchy.
import Cubical.Data.Empty as Empty open import Cubical.Foundations.Prelude using ( subst2; J ) open import Cubical.Data.Vec using ( Vec; _∷_; []; lookup ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; ⁅_,_⁆; ⁅_⁆s; module InfinitySet )
The von Neumann successor and numerals organize the finite closure stages inside ω. Unordered pairs also supply the ingredients from which the ordered pairs used in graphs and environments are encoded.
open import V.Model {ℓ} using ( pair-spec ) open InfinitySet {ℓ} using ( ω; sucV; #_ ) open import Cubical.Foundations.HLevels using ( isPropΣ; isPropΠ; isPropΠ2 ) open import Cubical.Functions.Logic using ( ⇔toPath )
Existence statements are kept propositionally truncated until their witnesses are needed only to prove another proposition. Equalities in the cumulative hierarchy are propositions, so the collapse argument can eliminate such truncated data when proving its set equalities.
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 ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ )
Two levels of membership must be distinguished. Ambient membership belongs to the cumulative hierarchy, whereas an element of the constructible carrier packages an ambient set together with a proof of constructibility; carrier membership is read through those underlying sets.
open hPropStructure 𝒮ᵥ module CS = hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )
For formulas whose constants are elements of L, ⊨ denotes satisfaction in the class model of L. Relabeling constants by the identity map leaves both the environment and satisfaction unchanged.
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ ) open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ ) module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename )
Seven names, i0 through i6, abbreviate the first seven de Bruijn indices, one per slot of a long environment.
private i0 : ∀ {k} → Fin (suc k) i0 = zero i1 : ∀ {k} → Fin (suc (suc k)) i1 = suc i0
Each successor shifts the preceding index into a larger finite type; the names continue slot by slot.
i2 : ∀ {k} → Fin (suc (suc (suc k))) i2 = suc i1 i3 : ∀ {k} → Fin (suc (suc (suc (suc k)))) i3 = suc i2 i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))
These are free-variable positions, whose interpretation changes as later binders extend the environment.
i4 = suc i3 i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k)))))) i5 = suc i4 i6 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc k))))))) i6 = suc i5
An element of the carrier is determined by its underlying set, because constructibility is a proposition: two carrier elements with equal underlying sets are equal, and the helper S≡ makes that identification wherever a carrier element is rebuilt from the same underlying set.
S≡ : {x y : CS.S} → fst x ≡ fst y → x ≡ y S≡ = Σ≡Prop (λ v → snd (isL v))
The renaming ρs swaps the two slots: a formula about a pair in the swapped order is read in the original order. It is used when the step formula is proved in one slot order and consumed in the other.
ρs : Fin 2 → Fin 2 ρs zero = suc zero ρs (suc zero) = zero
The renaming ρf keeps w in slot zero and sends Z from slot one to slot two, skipping the middle slot occupied by the candidate next stage Z'.
ρf : Fin 2 → Fin 3 ρf zero = zero ρf (suc zero) = suc (suc zero)
An agreement for ρs says that the swapped environment carries the same elements as the original at the moved slots. Both cases are proved by reflexivity, since each slot is sent to the position of the very same element.
ags : (Z'' w : CS.S) → Ren.Agrees ρs (Z'' ∷ w ∷ []) (w ∷ Z'' ∷ []) ags Z'' w zero = refl ags Z'' w (suc zero) = refl
Fix an arbitrary constructible carrier M.
agf : (w Z' Z : CS.S) → Ren.Agrees ρf (w ∷ Z' ∷ Z ∷ []) (w ∷ Z ∷ []) agf w Z' Z zero = refl agf w Z' Z (suc zero) = refl
The collapse of a constructible carrier stays in L
The collapse argument uses only the constructibility of M and the predecessors that remain inside it; no transitivity assumption is imposed.
module PiIn (Mʟ : CS.S) where
Let M be the underlying set of the chosen constructible carrier. Its accompanying certificate ensures that every member later lifted from M is constructible.
M : S M = fst Mʟ
The collapse π x is formed from the collapse values of those members of x that also lie in M; πX collects the values π x for x ∈ M. This restricted predecessor relation makes the definition meaningful without assuming that M is transitive.
module C = Collapse M using ( Fiber; π; π-compute; πX; πX-member; π∈-fwd )
Since constructibility is inherited by members, every y ∈ M is constructible. Hence such a y can be paired with that proof and treated as an element of the constructible carrier.
memL : (y : S) → ⟨ y ∈ˢ M ⟩ → ⟨ isL y ⟩ memL y y∈M = isL-trans {x = M} {y = y} y∈M (snd Mʟ)
The lifting up packages a member as a carrier element. The first lemma reads the collapse value outward: every member of π x is the collapse of a member of x that lies in M, which follows from the computation clause of the collapse, the identity π x equals the image of the collapse over the members of x inside M.
up : (y : S) → ⟨ y ∈ˢ M ⟩ → CS.S up y y∈M = y , memL y y∈M π-mem-out : (x w : S) → ⟨ w ∈ˢ C.π x ⟩ → ∥ Σ[ y ∈ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) ∥₁ π-mem-out x w w∈ = PT.map mk (subst (λ u → ⟨ w ∈ˢ u ⟩) (C.π-compute x) w∈)
The conversion turns the collapse's own fibre witness into the member statement: the fibre pairs a presented index with the proof that the collapse of the presented element equals w, and the presented element is a member of x whose collapse is taken.
where mk : Σ[ p ∈ C.Fiber x ] (C.π (⟪ x ⟫↪ (p .fst)) ≡ w) → Σ[ y ∈ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) mk (p , q) = ⟪ x ⟫↪ (p .fst) , ( member x (p .fst)
The membership relation of M is expressed using three free-variable slots, read by Relation at the environment y ∷ x ∷ e ∷ []; the third slot carries the coded pair, while the formula asserts y ∈ M, x ∈ M, and y ∈ x.
, ∈∈ₛ {a = ⟪ x ⟫↪ (p .fst)} {b = M} .snd (p .snd) , q ) private module Membership = Relation Mʟ Mʟ ((var i1 ∈̇ con Mʟ) ∧̇ ((var i0 ∈̇ con Mʟ) ∧̇ (var i1 ∈̇ var i0)))
The host-side reading of the relation is exactly the three memberships, conjoined; this is the adequacy that lets the object-language formula and the external statement stand for each other.
(λ y x → (fst y ∈ˢ M) ⊓ ((fst x ∈ˢ M) ⊓ (fst y ∈ˢ fst x))) (λ y x z h → h) (λ y x z h → h)
The relation becomes an element of the model: a set of pairs of carrier elements, introduced and eliminated by the two readings. Because the relation is bounded by the carrier, the pair set is small enough to be carved out by separation.
R : CS.S R = Membership.rel
The introduction reading exhibits both endpoint memberships and the membership between them, which is the content of the relation at the pair.
R-in : (y x : CS.S) → ⟨ fst y ∈ˢ M ⟩ → ⟨ fst x ∈ˢ M ⟩ → ⟨ fst y ∈ˢ fst x ⟩ → Holds R y x R-in y x my mx yx = Membership.into y x my mx (my , mx , yx)
The elimination reading returns the same three memberships; the two directions together say the relation is adequate, neither stronger nor weaker than the host-side statement.
R-out : (y x : CS.S) → Holds R y x → ⟨ fst y ∈ˢ M ⟩ × ⟨ fst x ∈ˢ M ⟩ × ⟨ fst y ∈ˢ fst x ⟩ R-out = Membership.pair-out
The collapse formula is local, not global. At slots for a value and an argument it says: there merely exists a table F correct for the relation R, complete at the argument, whose value at the argument is the given value. No single global function graph is claimed; at each argument only the existence of such a table is asserted, which is what lets the formula hold over a non-transitive carrier.
opaque piFo : Formula CS.S 2 piFo = ∃̇ ( correctAt i0 R ∧̇ ( completeAt i0 R i2 ∧̇ valueAt i0 R i2 i1 ) )
The outward reading of the formula unpacks the satisfaction into the three components: the correct table, its completeness at the argument, and the value clause, each transported out of its binder by the order-type chapter's own projections.
piFo-out : (v p : CS.S) → ⟨ (v ∷ p ∷ []) ⊨ piFo ⟩ → ∥ Σ[ F ∈ CS.S ] (Correct F R × (Complete F R p × ValueIs F R p v)) ∥₁ piFo-out v p = PT.map (λ { (F , (hc , (hm , hv))) → F , ( correct-out i0 R (F ∷ v ∷ p ∷ []) hc , ( complete-out i0 R i2 (F ∷ v ∷ p ∷ []) hm
The innermost projection finishes the unpacking: the value clause arrives as an ordinary statement about the table's entry at the argument.
, value-out i0 R i2 i1 (F ∷ v ∷ p ∷ []) hv ) ) })
The inward reading chooses the table F for the existential quantifier and supplies proofs of its correctness, completeness at the argument, and value clause. Together with the outward reading, this identifies the formula exactly with its intended content.
piFo-in : (v p F : CS.S) → Correct F R → Complete F R p → ValueIs F R p v → ⟨ (v ∷ p ∷ []) ⊨ piFo ⟩ piFo-in v p F hc hm hv = ∣ F , ( correct-in i0 R (F ∷ v ∷ p ∷ []) hc , ( complete-in i0 R i2 (F ∷ v ∷ p ∷ []) hm
Uniqueness is proved by one membership induction. The motive says: at every constructible member x of the carrier, any table correct for the relation and complete at x assigns the collapse of x as its value. Both the constructibility and the membership travel with the motive, because the table's entries are pairs of carrier elements.
, value-in i0 R i2 i1 (F ∷ v ∷ p ∷ []) hv ) ) ∣₁ private Pv : CS.S → S → Type (ℓ-suc ℓ) Pv F x = (xL : ⟨ isL x ⟩) → ⟨ x ∈ˢ M ⟩ → (v : CS.S) → Complete F R (x , xL) → ValueIs F R (x , xL) v → fst v ≡ C.π x
The induction runs along membership in the ambient hierarchy, exactly as the collapse itself is defined along it: to prove the motive at x, prove it at every member of x.
value-val′ : (F : CS.S) → Correct F R → (x : S) → Pv F x value-val′ F hc = ∈-induction {P = Pv F} go where go : (x : S) → ((y : S) → ⟨ y ∈ˢ x ⟩ → Pv F y) → Pv F x go x IH xL x∈M v cmp val =
The step compares members: the recorded value and the collapse have the same members, and extensionality of the ambient hierarchy turns that into equality. The argument is presented as a carrier element, so its entries may be typed over the carrier.
extensionalV {a = fst v} {b = C.π x} (λ w → ⇔toPath (fwd w) (bwd w)) where xS : CS.S xS = x , xL
Forward: a member w of the recorded value is carried, and the value clause produces a relation entry together with a table entry at it. The carrying packages w with the constructibility inherited from the recorded value.
fwd : (w : S) → ⟨ w ∈ˢ fst v ⟩ → ⟨ w ∈ˢ C.π x ⟩ fwd w w∈ = PT.rec (snd (w ∈ˢ C.π x)) read (val wS .fst w∈) where wS : CS.S wS = w , isL-trans {x = fst v} {y = w} w∈ (snd v)
The source witness separates into a relation fact ry and a table entry fy. Reading ry yields y ∈ M and y ∈ x; the induction hypothesis applied to fy identifies w with π y, and π∈-fwd then places w in π x.
read : Σ[ y ∈ CS.S ] (Holds R y xS × Holds F y wS) → ⟨ w ∈ˢ C.π x ⟩ read (y , (ry , fy)) = subst (λ t → ⟨ t ∈ˢ C.π x ⟩) e (C.π∈-fwd x (fst y) y∈x y∈M) where y∈M : ⟨ fst y ∈ˢ M ⟩
The relation entry also says the component lies in the argument, which unlocks the induction hypothesis: the table's value at that component equals the collapse of the component. This equation, composed with the collapse reading, is the identification of w.
y∈M = R-out y xS ry .fst y∈x : ⟨ fst y ∈ˢ x ⟩ y∈x = R-out y xS ry .snd .snd e : C.π (fst y) ≡ w e = sym (IH (fst y) y∈x (snd y) y∈M wS (hc y wS fy .fst) (hc y wS fy .snd))
Backward: a member w of the collapse decomposes, by the outward reading already proved, into a component of the argument inside the carrier whose collapse is w. Completeness at the original argument x, applied to the predecessor y, supplies an entry (y,u).
bwd : (w : S) → ⟨ w ∈ˢ C.π x ⟩ → ⟨ w ∈ˢ fst v ⟩
bwd w w∈ = PT.rec (snd (w ∈ˢ fst v)) read (π-mem-out x w w∈)
where
read : Σ[ y ∈ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) → ⟨ w ∈ˢ fst v ⟩
read (y , (y∈x , y∈M , e)) = PT.rec (snd (w ∈ˢ fst v)) inner (cmp yS ry)
The component is carried as a carrier element, and the relation entry at the pair is reintroduced from the two memberships and the membership between them.
where yS : CS.S yS = up y y∈M ry : Holds R yS xS ry = R-in yS xS y∈M x∈M y∈x
The induction hypothesis identifies u with π y, and π y = w transports membership in the recorded value to w. This is what the backward direction claims.
inner : Σ[ u ∈ CS.S ] Holds F yS u → ⟨ w ∈ˢ fst v ⟩ inner (u , fu) = subst (λ t → ⟨ t ∈ˢ fst v ⟩) (eu ∙ e) (val u .snd ∣ yS , (ry , fu) ∣₁) where eu : fst u ≡ C.π y
The equation eu is the induction hypothesis at the component: the table's value at y equals the collapse of y. Composed with the equation carried by the decomposition, it identifies the entry's value with w, which is exactly what the backward direction had to place.
eu = IH y y∈x (snd yS) y∈M u (hc yS u fu .fst) (hc yS u fu .snd)
Applying the induction to the underlying set of a carrier element gives the same uniqueness statement in the restricted structure. The resulting determination lemma says that whenever the collapse formula is satisfied at a member of M, its value must equal that member's collapse.
value-val : (F : CS.S) → Correct F R → (x : CS.S) → ⟨ fst x ∈ˢ M ⟩ → (v : CS.S) → Complete F R x → ValueIs F R x v → fst v ≡ C.π (fst x) value-val F hc x = value-val′ F hc (fst x) (snd x) piFo-val : (q : CS.S) → ⟨ fst q ∈ˢ M ⟩ → (v : CS.S) → ⟨ (v ∷ q ∷ []) ⊨ piFo ⟩ → fst v ≡ C.π (fst q)
The proof eliminates the truncated existence into the equality of two h-sets, which is a proposition, and applies the uniqueness just proved to the correct table handed over by the outward reading. The next construction cuts from the carrier the elements lying inside a given element of L.
piFo-val q mq v h = PT.rec (setIsSet (fst v) (C.π (fst q))) (λ { (F , (hc , (hm , hv))) → value-val F hc q mq v hm hv }) (piFo-out v q h) module Cut (K : CS.S) where
The cutting formula is the single atomic formula: the free slot is a member of the constant K. Everything the slice contains is what satisfies it.
cutFo : Formula CS.S 1 cutFo = var i0 ∈̇ con K
Separation applied at Mʟ yields the slice as an element of L, so the slice is more than a mere class of members. This is what lets the slice serve as the domain of an internal recursion.
opaque cut : CS.S cut = hasSeparationL Mʟ cutFo .fst .fst
The membership specification identifies membership in the slice with membership in the carrier together with satisfaction of the cutting formula, which unpacks to lying in the underlying set of K.
cut-mem : (y : CS.S) → (y CS.∈ˢ cut) ≡ ((y CS.∈ˢ Mʟ) ⊓ ((y ∷ []) ⊨ cutFo)) cut-mem = hasSeparationL Mʟ cutFo .fst .snd
The inward direction combines membership in M with membership in the underlying set of K to place the carried element in the slice.
cut-in : (y : CS.S) → ⟨ fst y ∈ˢ M ⟩ → ⟨ fst y ∈ˢ fst K ⟩ → ⟨ y CS.∈ˢ cut ⟩ cut-in y my yK = subst ⟨_⟩ (sym (cut-mem y)) (my , yK)
The outward direction reads the same specification back into its two components. A member q of the carrier is good at a stage δ when membership in that stage yields both a constructible presentation of its collapse and the collapse formula at q.
cut-out : (y : CS.S) → ⟨ y CS.∈ˢ cut ⟩ → ⟨ fst y ∈ˢ M ⟩ × ⟨ fst y ∈ˢ fst K ⟩ cut-out y h = subst ⟨_⟩ (cut-mem y) h Good : S → S → Type (ℓ-suc ℓ) Good δ q = ⟨ q ∈ˢ M ⟩ → ⟨ q ∈ˢ Lset δ ⟩ → Σ[ qL ∈ ⟨ isL (C.π q) ⟩ ] ((mq : ⟨ q ∈ˢ M ⟩)
The second component of goodness packages the collapse as an element of 𝒮ʟ using its constructibility proof, and states that the collapse formula holds of this value and the chosen presentation of the member of M.
→ ⟨ ((C.π q , qL) ∷ up q mq ∷ []) ⊨ piFo ⟩)
Goodness is a proposition: membership in the carrier, in the stage, constructibility, and satisfaction are each one. This matters because the stage decomposition returns a merely-existing witness, and a merely-existing goodness can be consumed without choosing among witnesses.
isPropGood : (δ q : S) → isProp (Good δ q) isPropGood δ q = isPropΠ2 λ _ _ → isPropΣ (snd (isL (C.π q))) λ qL → isPropΠ λ mq → snd (((C.π q , qL) ∷ up q mq ∷ []) ⊨ piFo)
Fix an ordinal stage δ' and assume goodness for every q that lies both in M and in Lset δ'. These earlier collapse values will be assembled into the value at the next argument.
module Step (δ' : S) (oδ' : IsOrd δ') (IH : (q : S) → Good δ' q) where
The slice is cut at the stage Lset δ': the members of the carrier that the stage already contains. Because the stage is a set of L, the slice is an element of L by separation, and it is exactly the domain the induction hypothesis speaks about.
module Sl = Cut (LsetS δ' oδ') using ( cut; cut-in; cut-out )
Stages are transitive, so a member of a member of the stage is still inside the stage; this is the fact that later restricts the table's conditions to smaller arguments. By the induction hypothesis, the collapse of a slice member is available as an element of 𝒮ʟ; its constructibility proof is the first component of goodness.
Lδ'-trans : {x y : S} → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ Lset δ' ⟩ → ⟨ y ∈ˢ Lset δ' ⟩ Lδ'-trans {x} {y} = layer-trans (Lset-layer δ') {x = x} {y = y} πʟ : (y : CS.S) → ⟨ y CS.∈ˢ Sl.cut ⟩ → CS.S πʟ y hy = C.π (fst y) , IH (fst y) (Sl.cut-out y hy .fst) (Sl.cut-out y hy .snd) .fst
The collapse formula holds at the pair of that collapse and the member, by the same induction hypothesis: the second component of goodness is exactly a satisfaction of the formula at the pair, transported along the identification of the element with its underlying set.
πʟ-graph : (y : CS.S) (hy : ⟨ y CS.∈ˢ Sl.cut ⟩) → ⟨ (πʟ y hy ∷ y ∷ []) ⊨ piFo ⟩ πʟ-graph y hy = subst (λ y' → ⟨ (πʟ y hy ∷ y' ∷ []) ⊨ piFo ⟩) (S≡ refl) (IH (fst y) my (Sl.cut-out y hy .snd) .snd my)
The identification uses the membership of the member in the carrier, read out of the slice specification; the underlying set has not changed, so the transport is determined by the propositionality of constructibility.
where my : ⟨ fst y ∈ˢ M ⟩ my = Sl.cut-out y hy .fst
Over the slice, these collapse values form an internal recursion with domain the slice and graph piFo. Constructibility supplies each value as an element of 𝒮ʟ, so the graph entries are pairs of 𝒮ʟ-elements.
private Rπ : Recursion Rπ = record { dom = Sl.cut ; graph = piFo ; funct = λ y hy → (πʟ y hy , πʟ-graph y hy)
Functionality holds because the collapse formula determines its value at every member of the carrier: any other value satisfying the formula at the same pair is equal to it, which the determination lemma reads out. The equality of the corresponding 𝒮ʟ-elements then follows because their constructibility proofs are proposition-valued.
, λ { (v , h) → Σ≡Prop (λ w → snd ((w ∷ y ∷ []) ⊨ piFo)) (sym (S≡ (piFo-val y (Sl.cut-out y hy .fst) v h))) } }
The graph recursion of L collects the table: a set of pairs of carrier elements whose entries are exactly the collapse records over the slice.
module T = RecursionGraph Rπ using ( F; F-in; pair-out )
The collected set is the table at the stage: an element of L that pairs each slice member with its constructible collapse.
Tab : CS.S Tab = T.F
The inward reading of the table exhibits its entries: at every slice member, the pair of the member with its collapse is recorded.
Tab-in : (y : CS.S) (hy : ⟨ y CS.∈ˢ Sl.cut ⟩) → Holds Tab y (πʟ y hy) Tab-in = T.F-in
The outward reading decomposes an entry into a slice member and a value equal to the collapse of its underlying set. Together with the inward reading this says the table records exactly the collapses, nothing distorted.
Tab-pair : (x v : CS.S) → Holds Tab x v → ⟨ x CS.∈ˢ Sl.cut ⟩ × (fst v ≡ C.π (fst x)) Tab-pair = T.pair-out
An argument x is closed when every member of x that also belongs to M lies in the stage slice. This condition is imposed on each argument separately, because no transitivity assumption is made on M.
Closed : CS.S → Type (ℓ-suc ℓ) Closed x = (y : S) (y∈x : ⟨ y ∈ˢ fst x ⟩) (y∈M : ⟨ y ∈ˢ M ⟩) → ⟨ up y y∈M CS.∈ˢ Sl.cut ⟩
A slice member is closed by transitivity of the stage: any member of it that lies in M remains in the stage and therefore belongs to the slice.
slice-closed : (x : CS.S) → ⟨ x CS.∈ˢ Sl.cut ⟩ → Closed x slice-closed x hx y y∈x y∈M = Sl.cut-in (up y y∈M) y∈M (Lδ'-trans {x = fst x} {y = y} y∈x (Sl.cut-out x hx .snd))
For a closed argument, completeness of the table is the truncated existence of the table's own entry at each related member: closedness places that member inside the slice, where the table records its collapse. The relation entry is decomposed to name the member.
complete-of : (x : CS.S) → Closed x → Complete Tab R x complete-of x cl y ry = ∣ πʟ y' hy' , subst (λ w → ⟨ pr w (C.π (fst y)) ∈ˢ fst Tab ⟩) refl (Tab-in y' hy') ∣₁ where ro = R-out y x ry y' : CS.S
The member is carried as a carrier element, and closedness places the carried element inside the slice, which is exactly the hypothesis under which the table recorded the collapse.
y' = up (fst y) (ro .fst) hy' : ⟨ y' CS.∈ˢ Sl.cut ⟩ hy' = cl (fst y) (ro .snd .snd) (ro .fst)
For a closed argument, the value clause holds of the collapse itself. The proof has two directions: every member of the collapse value comes from a related member, and every member related to the argument is carried into the collapse value by the table.
valueIs-of : (x : CS.S) → ⟨ fst x ∈ˢ M ⟩ → Closed x → (v : CS.S) → fst v ≡ C.π (fst x) → ValueIs Tab R x v valueIs-of x mx cl v ev w = fwd , bwd where fwd : ⟨ fst w ∈ˢ fst v ⟩ → Src Tab R x w
Forward: a member w of the candidate value v is decomposed by the collapse reading into a component of the argument inside the carrier, whose collapse equals w. The decomposition is a truncated existence, and the elimination targets a proposition.
fwd w∈ = PT.map read (π-mem-out (fst x) (fst w) (subst (λ t → ⟨ fst w ∈ˢ t ⟩) ev w∈)) where read : Σ[ y ∈ S ] (⟨ y ∈ˢ fst x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ fst w)) → Σ[ y ∈ CS.S ] (Holds R y x × Holds Tab y w) read (y , (y∈x , y∈M , e)) = up y y∈M
The component is lifted to the carrier. Its membership in the argument yields the relation entry, while the table entry is transported along the equality between its collapse and w. Together these two entries form the required witness of Src Tab R x w.
, ( R-in (up y y∈M) x y∈M mx y∈x , subst (λ t → ⟨ pr y t ∈ˢ fst Tab ⟩) e (Tab-in (up y y∈M) (cl y y∈x y∈M)) )
Backward: a source entry for w names a related member whose table value is w. The pair reading splits the entry into memberships and an equality; the collapse reading places w in the collapse of the first component, and the two equations transport it back into the recorded value.
bwd : Src Tab R x w → ⟨ fst w ∈ˢ fst v ⟩ bwd = PT.rec (snd (fst w ∈ˢ fst v)) (λ { (y , (ry , ty)) → subst2 (λ s t → ⟨ s ∈ˢ t ⟩) (sym (Tab-pair y w ty .snd)) (sym ev) (C.π∈-fwd (fst x) (fst y) (R-out y x ry .snd .snd) (R-out y x ry .fst)) })
The correctness of the table at each entry is assembled from the two clauses at the slice member that the entry names. The pair reading contributes the slice membership and the carrier membership.
Tab-correct : Correct Tab R Tab-correct x v hxv = complete-of x cl , valueIs-of x mx cl v (Tab-pair x v hxv .snd) where hx : ⟨ x CS.∈ˢ Sl.cut ⟩ hx = Tab-pair x v hxv .fst
The carrier membership and closedness complete the hypotheses, and the step module is parameterized by an argument q of the carrier all of whose members lie below the earlier stage. This is the situation needed for an element of the definable powerset of Lset δ'; here closedness follows from q⊆.
mx : ⟨ fst x ∈ˢ M ⟩ mx = Sl.cut-out x hx .fst cl : Closed x cl = slice-closed x hx module At (q : S) (mq : ⟨ q ∈ˢ M ⟩) (q⊆ : (y : S) → ⟨ y ∈ˢ q ⟩ → ⟨ y ∈ˢ Lset δ' ⟩) where
The argument is carried as a carrier element, so that it can serve as an environment slot and as the second component of pairs.
qS : CS.S
qS = up q mq
Closedness of the carried argument holds by the hypothesis: each member inside the carrier lies below the earlier stage, and the slice admits it. The members of the argument inside the carrier are then cut out as their own slice, the domain on which the collapse value will be computed.
cl : Closed qS cl y y∈q y∈M = Sl.cut-in (up y y∈M) y∈M (q⊆ y y∈q) module Mq = Cut qS using ( cut; cut-in; cut-out )
The collapse value of q is built as an internal recursion: domain the slice of members of q in the carrier, graph the collapse formula. This functional graph therefore meets the hypotheses of replacement in L.
private valR : Recursion valR = record { dom = Mq.cut ; graph = piFo
Functionality is assembled through mereFunct, from a merely-existing unique value at each argument. The witness wit produces such a value together with its satisfaction and uniqueness, all inside the truncation, because uniqueness of the collapse formula at a member of the carrier is a proposition.
; funct = λ y hy → mereFunct piFo y (wit y hy) } where wit : (y : CS.S) (hy : ⟨ y CS.∈ˢ Mq.cut ⟩) → ∥ Σ[ v ∈ CS.S ] (⟨ (v ∷ y ∷ []) ⊨ piFo ⟩ × ((v' : CS.S) → ⟨ (v' ∷ y ∷ []) ⊨ piFo ⟩ → v' ≡ v)) ∥₁
The witness is the global collapse value C.π (fst y), presented as constructible by the induction hypothesis. The stage-slice table supplies its piFo proof, and piFo-val supplies uniqueness.
wit y hy = ∣ πʟ y hy' , ( πʟ-graph y hy' , λ v' hv' → S≡ (piFo-val y my v' hv') ) ∣₁ where my : ⟨ fst y ∈ˢ M ⟩
The membership of y in the carrier comes from the slice of q. The hypothesis puts every member of q in Lset δ', so every such carrier element is admitted by the stage slice.
my = Mq.cut-out y hy .fst hy' : ⟨ y CS.∈ˢ Sl.cut ⟩ hy' = Sl.cut-in y my (q⊆ (fst y) (Mq.cut-out y hy .snd))
Replacement now collects the values of this recursion into an element of L: its members are exactly the constructible collapse values of members of q that lie in M.
module Vq = Of valR using ( table; table-in; table-out )
The underlying set of the table agrees with the collapse of q, proved by extensionality through a member-by-member equivalence. Forward: a member of the table is a value at some member y of q inside the carrier, and the elimination targets the proposition that w lies in the collapse of q.
val≡π : fst Vq.table ≡ C.π q val≡π = extensionalV {a = fst Vq.table} {b = C.π q} (λ w → ⇔toPath (fwd w) (bwd w)) where fwd : (w : S) → ⟨ w ∈ˢ fst Vq.table ⟩ → ⟨ w ∈ˢ C.π q ⟩ fwd w hw = PT.rec (snd (w ∈ˢ C.π q))
The outward reading names the member y and its value; the determination lemma identifies the value with the collapse of y, and the collapse reading places the collapse of y inside the collapse of q, which the transport composes.
(λ { (y , (hy , h)) → subst (λ t → ⟨ t ∈ˢ C.π q ⟩) (sym (piFo-val y (Mq.cut-out y hy .fst) wS h)) (C.π∈-fwd q (fst y) (Mq.cut-out y hy .snd) (Mq.cut-out y hy .fst)) }) (Vq.table-out wS hw)
Since w belongs to the constructible value set Vq.table, transitivity of L supplies its constructibility and hence its presentation as an element of 𝒮ʟ.
where wS : CS.S wS = w , isL-trans {x = fst Vq.table} {y = w} hw (snd Vq.table)
Backward: a member of the collapse of q decomposes into a component of q inside the carrier whose collapse equals it, which is precisely the form in which the table records entries.
bwd : (w : S) → ⟨ w ∈ˢ C.π q ⟩ → ⟨ w ∈ˢ fst Vq.table ⟩ bwd w hw = PT.rec (snd (w ∈ˢ fst Vq.table)) read (π-mem-out q w hw) where read : Σ[ y ∈ S ] (⟨ y ∈ˢ q ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) → ⟨ w ∈ˢ fst Vq.table ⟩ read (y , (y∈q , y∈M , e)) =
The equation transports w to the collapse of the component, and the table's inward reading produces the entry at the carried component, which records exactly that collapse.
subst (λ t → ⟨ t ∈ˢ fst Vq.table ⟩) e (Vq.table-in yS (πʟ yS hy') hy (πʟ-graph yS hy')) where yS : CS.S yS = up y y∈M
The carried component lies in the slice of q by its carrier membership, and in the stage slice by the hypothesis that members of q lie below the earlier stage.
hy : ⟨ yS CS.∈ˢ Mq.cut ⟩ hy = Mq.cut-in yS y∈M y∈q hy' : ⟨ yS CS.∈ˢ Sl.cut ⟩ hy' = Sl.cut-in yS y∈M (q⊆ y y∈q)
The collapse of q is constructible: it equals the underlying set of the table, and the table is an element of L, so constructibility is transported along the equality. This is the first clause of goodness at q.
πq-isL : ⟨ isL (C.π q) ⟩ πq-isL = subst (λ t → ⟨ isL t ⟩) val≡π (snd Vq.table)
The second clause of goodness is the collapse formula satisfied at the pair of the collapse with the member: correctness of the table, completeness at the closed argument, and the value clause identifying the value with the collapse. With both clauses, the stage induction can be stated: goodness at every ordinal.
The induction runs along membership in the hierarchy, consuming at each step the decomposition of membership in the stage.
good : (mq' : ⟨ q ∈ˢ M ⟩) → ⟨ ((C.π q , πq-isL) ∷ up q mq' ∷ []) ⊨ piFo ⟩ good mq' = subst (λ q' → ⟨ ((C.π q , πq-isL) ∷ q' ∷ []) ⊨ piFo ⟩) (S≡ refl) (piFo-in (C.π q , πq-isL) qS Tab Tab-correct (complete-of qS cl) (valueIs-of qS mq cl (C.π q , πq-isL) refl)) good-at : (δ : S) → IsOrd δ → (q : S) → Good δ q
To prove goodness at δ, the membership of q in the stage Lset δ is decomposed: q lies in the definable powerset of an earlier stage δ'. The decomposition is eliminated into goodness, because goodness is a proposition.
good-at = ∈-induction {P = λ δ → IsOrd δ → (q : S) → Good δ q} go where go : (δ : S) → ((δ' : S) → ⟨ δ' ∈ˢ δ ⟩ → IsOrd δ' → (q : S) → Good δ' q) → IsOrd δ → (q : S) → Good δ q go δ IH oδ q mq q∈Lδ = PT.rec (isPropGood δ q) read (Lset-out δ q q∈Lδ) mq q∈Lδ
The decomposition names the earlier stage δ' below δ and the membership of q in its definable powerset. Using goodness below δ', the step construction yields goodness at q. The definable powerset clause then says every member of q lies in the stage Lset δ', which is the closedness hypothesis the step consumes.
where read : Σ[ δ' ∈ S ] (⟨ δ' ∈ˢ δ ⟩ × ⟨ q ∈ˢ 𝒟ₒ (Lset δ') ⟩) → Good δ q read (δ' , (δ'∈δ , q∈𝒟)) _ _ = A.πq-isL , A.good where oδ' : IsOrd δ'
Ordinality of δ' follows from δ' ∈ δ. Applying the induction hypothesis below δ', together with the definable-powerset fact that every member of q lies in Lset δ', yields goodness at q. Thus the membership induction proves good-at. Since M itself belongs to L, its constructibility certificate supplies a stage containing M; transitivity of that stage then places every member of M inside it.
oδ' = mem-ord {A = δ} oδ δ' δ'∈δ module A = Step.At δ' oδ' (IH δ' δ'∈δ oδ') q mq (λ y y∈q → 𝒟ₒ∋⊆ (Lset δ') q q∈𝒟 y y∈q) using ( πq-isL; good ) π-isL : (y : S) → ⟨ y ∈ˢ M ⟩ → ⟨ isL (C.π y) ⟩ π-isL y y∈M = PT.rec (snd (isL (C.π y)))
A stage containing the constructible carrier M is obtained from the proof Mʟ, and goodness at that stage yields constructibility of the collapse of every member of M. The following claim begins the corresponding argument for members of the whole collapse image C.πX, again eliminating a truncated presentation into constructibility.
(λ { (α , (oα , M∈Lα)) → good-at α oα y y∈M (layer-trans (Lset-layer α) {x = M} {y = y} y∈M M∈Lα) .fst }) (snd Mʟ) πX-isL : (x : S) → ⟨ x ∈ˢ C.πX ⟩ → ⟨ isL x ⟩ πX-isL x x∈πX = PT.rec (snd (isL x))
The statement of πX-isL is about members: each member of the collapse image is the collapse of some member of the carrier, hence constructible.
(λ { (y , (y∈M , e)) → subst (λ w → ⟨ isL w ⟩) e (π-isL y y∈M) }) (C.πX-member x x∈πX)
The Skolem hull as an ω-iteration
This says exactly that the collapse image is contained in L; it is a statement about members, and no claim is made that the image itself is an element of L. With the first half finished, the second half opens under new parameters: a stage lam closed under successors of its members, and a start X whose members all lie in the stage.
module Telescope (lam : S) (ordλ : IsOrd lam) (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩) (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)
The empty set lies in the stage as well, and the hull machinery is opened on these data: the hull carrier M, the fact that the hull is contained in the stage, and that every member of the start is a member of the hull.
(∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where module HS = HullStage lam ordλ succλ X X⊆L ∅∈λ using ( M ) module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ using ( ∅∈Lsetα; hull-member; X⊆M; Hull⊆L ) open HullStage.H.T lam ordλ succλ X X⊆L ∅∈λ public
A hull code is either a base name for a member of X, or wit k ψ cs, which stores a constant-free formula and codes for its parameters. Its value is obtained by evaluating the subcodes and then, according as a witness exists, choosing the least witness or the junk value.
using ( Code; base; wit; val; vals; search; Sat; Hull; val-wit ) open HullStage.H.T lam ordλ succλ X X⊆L ∅∈λ using ( inHull; _⊨₀_ )
The small carrier SL collects the members of the stage over which everything is typed. A parameter vector is drawn from a set Z when each of its components belongs to the underlying set of Z; the searches of the step range only over such vectors.
SL : Type (ℓ-suc ℓ) SL = HullStage.ASt.SL lam ordλ succλ X X⊆L ∅∈λ From : {k : ℕ} → CS.S → Vec SL k → Type (ℓ-suc ℓ) From {k} Z vs = (i : Fin k) → ⟨ fst (lookup i vs) ∈ˢ fst Z ⟩ Searched : CS.S → S → Type (ℓ-suc ℓ)
A search uses a constant-free formula of arity k+1. The vector from Z assigns its k parameter variables, while the remaining variable is assigned the candidate witness; Sat asserts that such a witness exists.
Searched Z z = Σ[ k ∈ ℕ ] Σ[ ψ ∈ Formula (⊥* {ℓ}) (suc k) ] Σ[ vs ∈ Vec SL k ] Σ[ w ∈ Sat k ψ vs ] (From Z vs × (z ≡ fst (search k ψ vs w))) Reads : CS.S → S → Type (ℓ-suc ℓ) Reads Z z = ⟨ z ∈ˢ fst Z ⟩ ⊎ ((z ≡ ∅) ⊎ Searched Z z)
The package contains the operation Φ, a two-variable formula ΦFo, and a proof that for every Z the environment assigning Φ Z and Z to its two variables satisfies that formula.
record StepPack : Type (ℓ-suc (ℓ-suc ℓ)) where field Φ : CS.S → CS.S ΦFo : Formula CS.S 2 defines : (Z : CS.S) → ⟨ (Φ Z ∷ Z ∷ []) ⊨ ΦFo ⟩
The remaining fields pin the step down: any set satisfying the formula is the step's, members grow, the junk value is always present, and for every search at parameters from the current set the least witness is adjoined.
only : (Z Z' : CS.S) → ⟨ (Z' ∷ Z ∷ []) ⊨ ΦFo ⟩ → Z' ≡ Φ Z grows : (Z : CS.S) (z : S) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ fst (Φ Z) ⟩ junk : (Z : CS.S) → ⟨ ∅ ∈ˢ fst (Φ Z) ⟩ least : (Z : CS.S) (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec SL k) → From Z vs → (w : Sat k ψ vs) → ⟨ fst (search k ψ vs w) ∈ˢ fst (Φ Z) ⟩
The outward field reads a member of the step host-side, provided the current set lies below the stage: every member of the step is an old member, the junk value, or the value of a search. This reading is what the exhaustion proof will spend.
out : (Z : CS.S) → ((z : S) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩) → (z : S) → ⟨ z ∈ˢ fst (Φ Z) ⟩ → ∥ Reads Z z ∥₁
The iteration module takes the constructibility of the start together with the packaged step. Both are needed: the internal recursion begins at an element of L, and the step supplies the formula and its clauses.
module HullIter (X-isL : ⟨ isL X ⟩) (P : StepPack) where open StepPack P
The start is presented as a carrier element, pairing the set with its constructibility; this is the form the internal recursion consumes.
Xʟ : CS.S Xʟ = X , X-isL
The internal ω-recursion produces the iterates, and its closure machinery carries the growth field along: each iterate contains the previous one. The iterates are sets of the model, which is what will make their union an element of L.
module It = Iterate Xʟ ΦFo Φ defines only using ( it; module Closure; iterUnion; iterUnion-in; iterUnion-out; iter; iter-in; iter-out; ω-num; Num ) module Cl = It.Closure (λ Z z → grows Z (fst z)) using ( it-up )
The stages of the iteration are named hullStep n, the n-th application of the step to the start.
hullStep : ℕ → CS.S hullStep = It.it
The iteration is governed by its defining equation: applying the step n+1 times produces exactly the one-step closure Φ applied to the n-th iterate. The equation holds by refl, because internal ω-recursion computes its successor stage by calling the step operation directly, and nothing needs to be transported. This is the arithmetic of the construction in its barest form: each layer of the telescope is the closure of the previous layer under the single definable step.
hullStep-suc : (n : ℕ) → hullStep (suc n) ≡ Φ (hullStep n) hullStep-suc n = refl
The iterates grow with their index: if n does not exceed n', then everything collected by the n-th iterate is still collected by the n'-th. The growth field of the step is applied once for each step of the difference, keeping the old members every time; the numeric equation carries the count, and the constructibility of the member travels with it, since it belongs to a constructible iterate. This monotonicity is what makes collection in an earlier iterate permanent.
hullStep-≤ : (n n' : ℕ) → n ≤ n' → (z : S) → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ fst (hullStep n') ⟩ hullStep-≤ n n' (k , e) z h = subst (λ m → ⟨ z ∈ˢ fst (hullStep m) ⟩) e (Cl.it-up n k (z , zL) h) where
Monotonicity of the iterates follows from the growth field: a member of an earlier iterate remains a member of every later one, and constructibility is carried along. Depth is assigned to hull codes by recursion: a base code has depth zero.
The witness code is one deeper than its code vector, because its value is computed one step after the values of the parameters.
zL : ⟨ isL z ⟩ zL = isL-trans {x = fst (hullStep n)} {y = z} h (snd (hullStep n)) mutual depth : Code → ℕ depth (base m) = 0
The witness constructor adds one to the depth of its vector of subcodes.
depth (wit k ψ cs) = suc (depths cs)
The depth of a code vector is the maximum of the depths of its entries: a vector is available once all of its entries are.
depths : {m : ℕ} → Vec Code m → ℕ depths [] = 0 depths (c ∷ cs) = max (depth c) (depths cs)
A helper records how a case split on a decidable disjunction behaves when one disjunct is impossible: if satisfaction is empty, the computed value is the junk branch, whatever the other branch would have said.
private stuck-r : {A : Type (ℓ-suc ℓ)} (na : A → Empty.⊥) (f : A → SL) (g : (A → Empty.⊥) → SL) (s : A ⊎ (A → Empty.⊥)) → Sum.rec f g s ≡ g na stuck-r na f g (inl a) = Empty.rec (na a)
The refutation branch is proved by the function extensionality of the impossible function: no member exists to distinguish.
stuck-r na f g (inr h) = cong g (funExt (λ a → Empty.rec (na a)))
Hull into union, first half: every hull code has its value staged at the iterate indexed by its depth. A base code names a member of the start, present at the zeroth iterate.
mutual hullStep-in : (c : Code) → ⟨ fst (val c) ∈ˢ fst (hullStep (depth c)) ⟩ hullStep-in (base m) = member X m hullStep-in (wit k ψ cs) = go (lem (Sat k ψ (vals cs) , squash₁)) where
A witness code is split according to whether its search is satisfiable. Its depth is one more than the depth of its parameter-code vector, and the successor equation identifies that depth with the iterate obtained by applying Φ once more.
n : ℕ n = depths cs go : (s : Sat k ψ (vals cs) ⊎ (Sat k ψ (vals cs) → Empty.⊥)) → ⟨ fst (Sum.rec (search k ψ (vals cs)) (λ _ → (∅ , HSH.∅∈Lsetα)) s) ∈ˢ fst (hullStep (suc n)) ⟩
If the search is satisfied, the least-witness clause of the step adjoins the searched value at the next iterate, whose parameters are available by the vector depths. If the search is unsatisfiable, there is no witness to adjoin, and the step keeps the junk value instead.
go (inl w) = least (hullStep n) k ψ (vals cs) (vals-in cs) w go (inr h) = junk (hullStep n)
The parameters of a code vector are available at the maximum of the entry depths: each entry's value appeared at its own depth, and monotonicity carries it to the later iterate where the vector is consumed.
vals-in : {m : ℕ} (cs : Vec Code m) → From (hullStep (depths cs)) (vals cs) vals-in (c ∷ cs) zero = hullStep-≤ (depth c) (max (depth c) (depths cs)) left-≤-max (fst (val c)) (hullStep-in c) vals-in (c ∷ cs) (suc i) = hullStep-≤ (depths cs) (max (depth c) (depths cs)) right-≤-max
The choice proceeds recursively over the parameter vector. For the empty vector, the empty code vector has the required value vector; at a nonempty vector, hull membership supplies a code for the head and recursion supplies codes for the tail.
(fst (lookup i (vals cs))) (vals-in cs i) private choose : {k : ℕ} (vs : Vec SL k) → ((i : Fin k) → ⟨ fst (lookup i vs) ∈ˢ Hull ⟩) → ∥ Σ[ cs ∈ Vec Code k ] (vals cs ≡ vs) ∥₁
The recursive step codes the head by hull membership and the tail recursively; the value equation is assembled componentwise, with the carrier equality reduced to the underlying sets.
choose [] h = ∣ [] , refl ∣₁ choose (v ∷ vs) h = PT.rec squash₁ (λ { (c , ec) → PT.map (λ { (cs , ecs) → (c ∷ cs) , cong₂ _∷_ (Σ≡Prop (λ z → snd (z ∈ˢ Lset lam)) ec) ecs }) (choose vs (λ i → h (suc i))) })
For a code vector cs, val-wit identifies the value of wit k ψ cs with the least witness returned by the search. Since every code value belongs to the hull, the searched value belongs to the hull.
(HSH.hull-member (fst v) (h zero)) search-val : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (cs : Vec Code k) (vs : Vec SL k) → vals cs ≡ vs → (w : Sat k ψ vs) → ⟨ fst (search k ψ vs w) ∈ˢ Hull ⟩ search-val k ψ cs vs e w = J (λ vs' e' → (w' : Sat k ψ vs') → ⟨ fst (search k ψ vs' w') ∈ˢ Hull ⟩)
The path induction transports the statement along the identification of the parameter vectors, and the witness code is judged inside the hull.
(λ w' → subst (λ z → ⟨ fst z ∈ˢ Hull ⟩) (val-wit k ψ cs w') (inHull (wit k ψ cs))) e w
The code wit 0 ⊥̇ [] has no satisfying witness, so its value follows the failure branch and is ∅. As every code value lies in the hull, the junk value lies there as well.
junk∈Hull : ⟨ ∅ ∈ˢ Hull ⟩ junk∈Hull = subst (λ z → ⟨ fst z ∈ˢ Hull ⟩) (stuck-r no (search 0 ⊥̇ []) (λ _ → (∅ , HSH.∅∈Lsetα)) (lem (Sat 0 ⊥̇ [] , squash₁))) (inHull (wit 0 ⊥̇ [])) where
No environment satisfies falsity: unpacking such a satisfaction proof would produce an element of the empty type.
no : Sat 0 ⊥̇ [] → Empty.⊥ no = PT.rec Empty.isProp⊥ (λ { (a , h) → Empty.rec* h })
Union into hull, second half: every member of every iterate lies in the hull, by induction on the iterate index. The base case is the start, whose members are hull members by the hull chapter.
hullStep⊆Hull : (n : ℕ) (z : S) → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ Hull ⟩ hullStep⊆Hull zero z h = HSH.X⊆M z h hullStep⊆Hull (suc n) z h = PT.rec (snd (z ∈ˢ Hull)) read (out (hullStep n) (λ z' hz' → HSH.Hull⊆L z' (hullStep⊆Hull n z' hz')) z h) where
The step case reads a member of the successor iterate through the outward clause: it is an old member, already in the hull by the induction hypothesis; it is the junk value, already in the hull; or it is a searched value, handled next.
read : Reads (hullStep n) z → ⟨ z ∈ˢ Hull ⟩ read (inl h') = hullStep⊆Hull n z h' read (inr (inl e)) = subst (λ t → ⟨ t ∈ˢ Hull ⟩) (sym e) junk∈Hull read (inr (inr (k , ψ , vs , w , from , e))) = subst (λ t → ⟨ t ∈ˢ Hull ⟩) (sym e)
A searched value is matched with the code vector of its parameters, each parameter being a hull member by the induction hypothesis; the search then lies in the hull by search-val, and the equation transports that membership to z. The union of the iterates is named as the element of L presenting the hull.
(PT.rec (snd (fst (search k ψ vs w) ∈ˢ Hull)) (λ { (cs , ecs) → search-val k ψ cs vs ecs w }) (choose vs (λ i → hullStep⊆Hull n (fst (lookup i vs)) (from i)))) hullL : CS.S hullL = It.iterUnion
The hull as an element of L is the union of the iterates, and its membership description says its members are exactly the hull members. Forward: a member of the union lies at some iterate, hence in the hull.
hullL-spec : fst hullL ≡ Hull
hullL-spec = extensionalV {a = fst hullL} {b = Hull} (λ z → ⇔toPath (fwd z) (bwd z))
where
fwd : (z : S) → ⟨ z ∈ˢ fst hullL ⟩ → ⟨ z ∈ˢ Hull ⟩
fwd z h = PT.rec (snd (z ∈ˢ Hull))
The iterate index is consumed by the outward reading of the union, and the constructibility of the member is carried from the union, itself constructible by construction.
(λ { (n , hn) → hullStep⊆Hull n z hn }) (It.iterUnion-out (z , isL-trans {x = fst hullL} {y = z} h (snd hullL)) h)
Backward: a hull member is named by a code, whose value appears at the iterate indexed by the code's depth; the inward reading of the union admits it.
bwd : (z : S) → ⟨ z ∈ˢ Hull ⟩ → ⟨ z ∈ˢ fst hullL ⟩ bwd z h = PT.rec (snd (z ∈ˢ fst hullL)) (λ { (c , ec) → It.iterUnion-in (depth c) zS (subst (λ t → ⟨ t ∈ˢ fst (hullStep (depth c)) ⟩) ec (hullStep-in c)) }) (HSH.hull-member z h)
The named member is carried into the carrier: its constructibility follows from the hull being contained in the stage, whose element presentation supplies the certificate.
where zS : CS.S zS = z , Lset→isL lam ordλ z (HSH.Hull⊆L z h)
The equality of underlying sets transports the union's constructibility onto the hull: the hull is an element of L. The first half of the chapter is now discharged in full, and the second module builds the definable step whose iteration was just consumed.
The step is built inside the stage, and its constants name objects of the stage: ordinality of lam comes from being an ordinal.
M-isL : ⟨ isL HS.M ⟩ M-isL = subst (λ t → ⟨ isL t ⟩) hullL-spec (snd hullL) module Build where
An ordinal of the hierarchy is constructible, which anchors the stage inside L.
λ-isL : ⟨ isL lam ⟩ λ-isL = isL-ord lam ordλ
A presents Lset lam together with its constructibility proof. It is the stage parameter used by the satisfaction graph and the coding of formulas over the stage.
A : CS.S A = LsetS lam ordλ
The satisfaction graph over the stage supplies the satisfaction sets of all codes at once, with both readings; and definability over the stage interprets the constants of formulas as elements of the stage.
module SM = SatGraph A using ( pairs; pairs-in; pairs-out; valOf; valOf≡ ) module DA = DefOf (Lset lam) using ( ι; _⊨ᵐ_; 𝒮M )
The code set at the empty alphabet collects the codes of the parameter-free formulas. Such formulas may have free variables; what they lack is constants, and the free variables will be assigned by the parameter environments of the searches.
C₀ : CS.S C₀ = AllCodes ∅ʟ
The stage's internal well-order is presented as an element of the model, the relation by which least witnesses will be compared.
Rel : CS.S Rel = relL lam λ-isL ordλ
The strict well-order on the small carrier is read from that relation; its comparison is stated on carrier elements. The second component of a constructible ordered pair is again constructible, which the parameters of names will need.
wL : SWO SL wL = orderAt lam ordλ relOf-at : SL → SL → Type (ℓ-suc ℓ) relOf-at = relOf wL pr-snd-isL : (a b : V ℓ) → ⟨ isL (pr a b) ⟩ → ⟨ isL b ⟩
The proof peels the ordered pair twice through singletons: membership in a pair puts the second component inside a singleton-pair nesting, and each peeling keeps constructibility by transitivity.
pr-snd-isL a b h = isL-trans {x = ⁅ a , b ⁆} {y = b} (subst ⟨_⟩ (sym (pair-spec a b b)) ∣ inr refl ∣₁) (isL-trans {x = pr a b} {y = ⁅ a , b ⁆} (subst ⟨_⟩ (sym (pair-spec ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a , b ⁆)) ∣ inr refl ∣₁) h)
Numerals are presented as carrier elements: the finite ordinal together with its constructibility, which the key clause of the witness formula will quantify over.
nn : ℕ → CS.S nn k = # k , numL k
Because the constant alphabet is empty, there is a unique interpretation ε′ into the stage carrier. It allows a constant-free formula to be relabeled into the stage language without making any choices.
ε′ : ⊥* {ℓ} → ⟪ Lset lam ⟫ ε′ = Empty.rec* sat-bridge : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) (δ : SL ^ k) → (δ ⊨₀ χ) ≡ (δ DA.⊨ᵐ mapFo ε′ χ) sat-bridge k χ δ =
The bridge is a composition: the environments of the empty alphabet agree trivially because there is nothing to interpret, and the relabeling theorem identifies the external satisfaction of the relabeled formula with the stage's internal satisfaction.
cong (λ κ → FOL.Semantics.At._⊨_ DA.𝒮M (⊥* {ℓ}) κ δ χ) (funExt (λ b → Empty.rec* b)) ∙ sym (⊨-map DA.𝒮M ε′ DA.ι χ δ) opaque keyOf : (k : ℕ) → Formula (⊥* {ℓ}) k → CS.S
The key of a parameter-free formula at the stage is the key of its relabeled form in the stage's code set. It is named once, so that later statements can mention it without reopening its construction.
keyOf k χ = keyS A (mapFo ε′ χ)
The key belongs to the code set at the stage: a code of the relabeled formula is a code over the stage's alphabet, and the code set contains all of them.
keyOf∈ : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) → ⟨ keyOf k χ CS.∈ˢ AllCodes A ⟩ keyOf∈ k χ = key∈AllCodes A (mapFo ε′ χ)
Although keyOf is opaque, the lemma keyOf≡ exposes the exact equation with keyS A (mapFo ε′ χ). Later proofs use this equation without unfolding the sealed definition.
keyOf≡ : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) → keyOf k χ ≡ keyS A (mapFo ε′ χ) keyOf≡ k χ = refl
The underlying set of the sealed key is computed: it is the ordered pair of the numeral of the arity with the code of the relabeled formula. The proof composes the two relabelings of the formula, the empty alphabet followed by the stage's embedding, and the relabeling theorem identifies the result with the code the limit level records.
keyOf-fst : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) → fst (keyOf k χ) ≡ pr (# k) (fst (limitCode χ)) keyOf-fst k χ = cong (pr (# k)) (cong VCode.⌜_⌝ ( mapFo-comp ε′ ⟪ Lset lam ⟫↪ χ ∙ cong (λ f → mapFo f χ) (funExt (λ b → Empty.rec* b)) ))
For each parameter-free formula, Tof is the satisfaction set selected by the satisfaction graph at the formula's sealed key. This fixed set represents satisfaction of that formula throughout the stage.
Tof : (k : ℕ) → Formula (⊥* {ℓ}) k → CS.S Tof k χ = SM.valOf (keyOf k χ) (keyOf∈ k χ)
The ordered pair of the key and its satisfaction set belongs to the satisfaction graph. Moreover, any carrier element with the same underlying set as the key selects the same satisfaction set: their constructibility witnesses are propositions, so equality of the underlying sets lifts to equality in the carrier and hence to equality of the selected values.
Tof-pair : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) → ⟨ pr (fst (keyOf k χ)) (fst (Tof k χ)) ∈ˢ fst SM.pairs ⟩ Tof-pair k χ = SM.pairs-in (keyOf k χ) (keyOf∈ k χ) valOf-same : (x : CS.S) (m : ⟨ x CS.∈ˢ AllCodes A ⟩) (k : ℕ) (χ : Formula (⊥* {ℓ}) k) → fst x ≡ fst (keyOf k χ) → SM.valOf x m ≡ Tof k χ
The proof runs by path induction on the equation of underlying sets, with the propositionality of code-set membership absorbing the difference of membership proofs. Only the underlying sets matter, so the transport is silent about everything else.
valOf-same x m k χ e = J (λ x' e' → (m' : ⟨ x' CS.∈ˢ AllCodes A ⟩) → SM.valOf x m ≡ SM.valOf x' m') (λ m' → cong (SM.valOf x) (snd (x CS.∈ˢ AllCodes A) m m')) (S≡ {x = x} {y = keyOf k χ} e) (keyOf∈ k χ) sat-at : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) (δ : SL ^ k) (z : CS.S)
Membership in a satisfaction set is now computed as the stage's own satisfaction. The bridge composes three identifications: the sealed name agrees with the key it was built from; the value at the key is read externally by the uniform satisfaction theorem; and the external satisfaction of the relabeled formula is the stage's internal satisfaction by the relabeling bridge.
→ fst z ≡ graph A δ → (z CS.∈ˢ Tof k χ) ≡ (δ ⊨₀ χ) sat-at k χ δ z qz = cong (z CS.∈ˢ_) (SM.valOf≡ (keyOf k χ) (keyOf∈ k χ)) ∙ val-sat A (mapFo ε′ χ) (keyOf k χ) (keyOf∈ k χ) (cong fst (keyOf≡ k χ)) δ z qz ∙ sym (sat-bridge k χ δ)
The key recognizer is a formula. It says that the value in slot s belongs to the stage's code set and is the ordered pair of the successor of the numeral in slot a with some code. Thus, when slot a contains # k, it recognizes a key of arity k+1 for a parameter-free formula. Parameter-free here means that the constant domain is empty; the formula may still have free variables.
opaque keyIn : ∀ {n} → Fin n → Fin n → Formula CS.S n keyIn s a = (var s ∈̇ con C₀) ∧̇ ∃̇ ( sucAtL (suc a) zero ∧̇ ∃̇ (prAtL (suc (suc s)) (suc zero) zero) )
The readings are stated at a variable environment, for a fixed arity k whose numeral is named at slot a. Fixing the arity in advance is what makes the two readings equations about codes rather than searches through them.
module KeyIn {n : ℕ} (s a : Fin n) (γ : CS.S ^ n) (k : ℕ)
(qa : fst (lookup a γ) ≡ # k) where
The formula is opened for computation at its own slots, since the readings must compute through the conjunctions and existentials of the definition.
opaque unfolding keyIn
The introduction builds the satisfaction from three data: the code-set membership of s, an element c of the hierarchy, and the equation identifying s with the pair of the successor numeral and c. The numeral, the successor clause and the pair clause are filled in order.
keyIn-in : ⟨ fst (lookup s γ) ∈ˢ fst C₀ ⟩ → (c : V ℓ) → fst (lookup s γ) ≡ pr (# (suc k)) c → ⟨ γ ⊨ keyIn s a ⟩ keyIn-in h c q = h , ∣ numAt , ( hsuc , ∣ cS , hpr ∣₁ ) ∣₁ where numAt : CS.S
The numeral is presented as a carrier element, and the code c is lifted to one as well. From the equation identifying s with the ordered pair and from the constructibility of s, pr-snd-isL extracts the constructibility of the pair's second component c.
numAt = nn (suc k) cS : CS.S cS = c , pr-snd-isL (# (suc k)) c (subst (λ u → ⟨ isL u ⟩) q (isL-trans h (snd C₀))) hsuc : ⟨ (numAt ∷ γ) ⊨ sucAtL (suc a) zero ⟩
The successor clause is transported from the equation of the numeral at slot a, and the pair clause from the equation of s, each through the adequacy of its coding operator. Both transports are exactly what converts host equations into satisfaction.
hsuc = subst ⟨_⟩ (sym (sucAtL-adequate (suc a) zero (numAt ∷ γ))) (cong sucV (sym qa)) hpr : ⟨ (cS ∷ numAt ∷ γ) ⊨ prAtL (suc (suc s)) (suc zero) zero ⟩ hpr = subst ⟨_⟩ (sym (prAtL-adequate (suc (suc s)) (suc zero) zero (cS ∷ numAt ∷ γ))) q
The elimination recovers the two data: the code-set membership of s, and the truncated statement that s is the pair of the successor numeral with some code. The existential chain of the formula is unpacked step by step.
keyIn-out : ⟨ γ ⊨ keyIn s a ⟩
→ ⟨ fst (lookup s γ) ∈ˢ fst C₀ ⟩
× ∥ Σ[ c ∈ V ℓ ] (fst (lookup s γ) ≡ pr (# (suc k)) c) ∥₁
keyIn-out (h , hk) = h , PT.rec squash₁ atNum hk
where
The intermediate binder names the numeral at the successor slot, and the adequacy of the successor coding converts its satisfaction into the equation of the underlying sets.
atNum : Σ[ z ∈ CS.S ] ( ⟨ (z ∷ γ) ⊨ sucAtL (suc a) zero ⟩ × ⟨ (z ∷ γ) ⊨ ∃̇ (prAtL (suc (suc s)) (suc zero) zero) ⟩ ) → ∥ Σ[ c ∈ V ℓ ] (fst (lookup s γ) ≡ pr (# (suc k)) c) ∥₁ atNum (z , (hs , hc)) = PT.map (λ { (c , hp) → fst c
The inner existential then yields the code c with a satisfaction of the pair clause; the adequacy transports it to the equation of pairs, composed with the identifications of the numeral and its successor. The equation recovered is exactly the truncated statement sought.
, ( subst ⟨_⟩ (prAtL-adequate (suc (suc s)) (suc zero) zero (c ∷ z ∷ γ)) hp ∙ cong (λ u → pr u (fst c)) (qz ∙ cong sucV qa) ) }) hc where qz : fst z ≡ sucV (fst (lookup a γ))
The seven-slot environment is now assembled: the satisfaction table, the extended environment, the parameter environment, the key, the numeral, the witness and the current set, in the order the body will read them.
qz = subst ⟨_⟩ (sucAtL-adequate (suc a) zero (z ∷ γ)) hs Env : CS.S → CS.S → CS.S → CS.S → CS.S → CS.S → CS.S → CS.S ^ 7 Env T e' e s k w Z = T ∷ e' ∷ e ∷ s ∷ k ∷ w ∷ Z ∷ []
The minimality subformula quantifies over the stage's alphabet. It says: if some extension of the parameter environment by a stage element satisfies the coded formula, then no such element stands before the witness in the stage's well-order. It is bounded by the constant A, so the quantifier runs over the stage and not over the universe.
opaque minFo : Formula CS.S 7 minFo = ∀̇∈ (con A) ( (∃̇ ( consAtL i0 i1 i4 ∧̇ (var i0 ∈̇ var i2) )) ⇒̇ ¬̇ (appC Rel i0 i6) )
The body conjuncts now say, in order: the numeral lies in the internal ωʟ; s is a key of arity one more; the parameter environment codes a vector over the current set; the extended environment extends it by the witness.
bodyFo : Formula CS.S 7 bodyFo = (var i4 ∈̇ con ωʟ) ∧̇ ( keyIn i3 i4 ∧̇ ( envOverAt i2 i4 i6 ∧̇ ( consAtL i1 i5 i2
The remaining conjuncts say: the pair of the key and the table lies in the satisfaction graph; the extended environment lies in the table; the witness lies in the stage; and minimality holds. There are eight conjuncts in all. The stage bounds the witness and the candidates used by minimality, while the coding conjuncts supply the auxiliary objects that connect the record to the satisfaction table.
∧̇ ( appC SM.pairs i3 i0 ∧̇ ( (var i1 ∈̇ var i0) ∧̇ ( (var i5 ∈̇ con A) ∧̇ minFo ))))))
Fix the seven objects T,e',e,s,k,w,Z. At their joint environment, the body is a concrete proposition whose eight conjuncts can be projected and assembled in both directions.
module BodyRd (T e' e s k w Z : CS.S) where
The seven-slot environment is recorded, and the host-side minimality is stated relative to a family presenting the parameter environment: no extension by a smaller stage element lands in the satisfaction table while ranking before the witness.
γ₇ : CS.S ^ 7 γ₇ = Env T e' e s k w Z Min : {m : ℕ} (g : Fin m → V ℓ) → Type (ℓ-suc ℓ) Min g = (w' : CS.S) → ⟨ fst w' ∈ˢ fst A ⟩ → (e'' : CS.S) → fst e'' ≡ env (cons (fst w') g) → ⟨ fst e'' ∈ˢ fst T ⟩
The clause ends in the empty type: minimality is refutation, and the data of a counterexample, a smaller extension with the pair membership, is exactly what must be impossible.
→ ⟨ pr (fst w') (fst w) ∈ˢ fst Rel ⟩ → Empty.⊥
Because the body is a nested conjunction, each of its eight conditions can be read by projection, while a proof of all eight conditions can be assembled back into satisfaction of the body.
opaque unfolding bodyFo
The first reading projects the numeral clause. Membership in the internal ωʟ lets us recover a natural number n; together with the key clause, this identifies s as a key of arity n+1, with one slot reserved for the witness.
b-num : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ fst k ∈ˢ fst ωʟ ⟩ b-num h = h .fst
The second projection is the key clause: at slots s and k, the formula asserts that s is a recognized key whose arity is one more than the numeral k.
b-key : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ γ₇ ⊨ keyIn i3 i4 ⟩ b-key h = h .snd .fst
The third reading projects the environment clause: the parameter environment codes a vector over the current set at the recorded slots.
b-env : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ γ₇ ⊨ envOverAt i2 i4 i6 ⟩ b-env h = h .snd .snd .fst
The fourth reading states the extension equation, transported along the adequacy of the cons coding: the extended environment is the parameter environment extended by the witness.
b-cons : {m : ℕ} (g : Fin m → V ℓ) → fst e ≡ env g → ⟨ γ₇ ⊨ bodyFo ⟩ → fst e' ≡ env (cons (fst w) g) b-cons g hE h = subst ⟨_⟩ (consAtL-adequate i1 i5 i2 γ₇ g hE) (h .snd .snd .snd .fst)
The fifth reading states the graph membership of the pair of the key and the table, transported along the adequacy of the application coding.
b-tab : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ pr (fst s) (fst T) ∈ˢ fst SM.pairs ⟩ b-tab h = subst ⟨_⟩ (appC-adequate SM.pairs i3 i0 γ₇) (h .snd .snd .snd .snd .fst)
The sixth reading is the membership of the extended environment in the satisfaction table, the fact that says the witness satisfies the coded formula at the parameters.
b-mem : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ fst e' ∈ˢ fst T ⟩ b-mem h = h .snd .snd .snd .snd .snd .fst
The seventh projection states that the witness belongs to the stage A, so the witness and all candidates compared with it range over the same stage.
b-stage : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ fst w ∈ˢ fst A ⟩ b-stage h = h .snd .snd .snd .snd .snd .snd .fst
The eighth reading is the minimality clause, read refutationally: a smaller candidate with a satisfying extension would contradict the bounded quantifier, after the relation entry is transported through the application's adequacy.
b-min : {m : ℕ} (g : Fin m → V ℓ) → fst e ≡ env g → ⟨ γ₇ ⊨ bodyFo ⟩ → Min g b-min g hE h w' hw' e'' qe hm hr = lower (h .snd .snd .snd .snd .snd .snd .snd w' hw' ∣ e'' , (hc , hm) ∣₁ (subst ⟨_⟩ (sym (appC-adequate Rel i0 i6 (w' ∷ γ₇))) hr)) where
The cons clause of the candidate extension is transported from its host equation, exactly mirroring the coding of the extension in the inner existential.
hc : ⟨ (e'' ∷ w' ∷ γ₇) ⊨ consAtL i0 i1 i4 ⟩ hc = subst ⟨_⟩ (sym (consAtL-adequate i0 i1 i4 (e'' ∷ w' ∷ γ₇) g hE)) qe
The filling reading assembles a satisfaction of the body from its eight components: the numeral clause, the key clause, the environment clause, the extension equation, the graph membership, the table membership, the stage membership, and minimality.
b-fill : {m : ℕ} (g : Fin m → V ℓ) → fst e ≡ env g → ⟨ fst k ∈ˢ fst ωʟ ⟩ → ⟨ γ₇ ⊨ keyIn i3 i4 ⟩ → ⟨ γ₇ ⊨ envOverAt i2 i4 i6 ⟩ → fst e' ≡ env (cons (fst w) g) → ⟨ pr (fst s) (fst T) ∈ˢ fst SM.pairs ⟩ → ⟨ fst e' ∈ˢ fst T ⟩ → ⟨ fst w ∈ˢ fst A ⟩ → Min g → ⟨ γ₇ ⊨ bodyFo ⟩
Five conjuncts are inserted directly. The extension equation and the graph entry are converted back into satisfactions by the reversed adequacy equations for consAtL and appC; minimality is supplied in the final clause.
b-fill g hE c1 c2 c3 c4 c5 c6 c7 mn = c1 , c2 , c3 , subst ⟨_⟩ (sym (consAtL-adequate i1 i5 i2 γ₇ g hE)) c4 , subst ⟨_⟩ (sym (appC-adequate SM.pairs i3 i0 γ₇)) c5 , c6 , c7
Minimality is filled by eliminating its truncated counterexample into the empty type: the counterexample is transported through both adequacy equations and handed to the refutation, so the filler needs only the contradiction, not a construction.
, λ w' hw' hex hr → lift (PT.rec Empty.isProp⊥ (λ { (e'' , (hc , hm)) → mn w' hw' e'' (subst ⟨_⟩ (consAtL-adequate i0 i1 i4 (e'' ∷ w' ∷ γ₇) g hE) hc) hm (subst ⟨_⟩ (appC-adequate Rel i0 i6 (w' ∷ γ₇)) hr) }) hex)
The witness formula wraps the body in five nested existentials, one per object: the satisfaction table, the extended environment, the parameter environment, the key, and the numeral. Satisfaction of the formula at w and Z says exactly that a complete record for a least witness at w over Z exists.
opaque witFo : Formula CS.S 2 witFo = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ bodyFo))))
The inward reading injects the five objects and the body satisfaction through the five binders, each injection carrying one object into its slot.
witFo-in : (w Z T e' e s k : CS.S) → ⟨ Env T e' e s k w Z ⊨ bodyFo ⟩ → ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩ witFo-in w Z T e' e s k h = ∣ k , ∣ s , ∣ e , ∣ e' , ∣ T , h ∣₁ ∣₁ ∣₁ ∣₁ ∣₁
The outward reading eliminates the five truncated existentials in binder order. At the innermost layer, PT.map merely rearranges the recovered objects into the displayed dependent tuple, leaving the body satisfaction unchanged.
witFo-out : (w Z : CS.S) → ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩ → ∥ Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ e ∈ CS.S ] Σ[ s ∈ CS.S ] Σ[ k ∈ CS.S ] ⟨ Env T e' e s k w Z ⊨ bodyFo ⟩ ∥₁ witFo-out w Z = PT.rec squash₁ (λ { (k , hk) → PT.rec squash₁ (λ { (s , hs) → PT.rec squash₁ (λ { (e , he) → PT.rec squash₁ (λ { (e' , he') → PT.map
Unwrapping witFo yields a table, an extended environment, a parameter environment, a key, and a numeral whose joint environment satisfies the body.
(λ { (T , hT) → T , e' , e , s , k , hT }) he' }) he }) hs }) hk })
The least-witness relation at a fixed key and environment
When e and s are fixed, LeastWitness Z e s z retains the truncated existence of the remaining table, extended environment, and numeral.
LeastWitness : CS.S → CS.S → CS.S → CS.S → Type (ℓ-suc ℓ) LeastWitness Z e s z = ∥ Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ k ∈ CS.S ] ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩ ∥₁
To bind the table, extended environment, and numeral while retaining six ambient variables, the body is renamed from seven slots to nine. The map places its seven meaningful entries at T,e',e,s,k,z,Z.
private
ρ₉ : Fin 7 → Fin 9
ρ₉ zero = i0
ρ₉ (suc zero) = i1
ρ₉ (suc (suc zero)) = i4
The remaining four cases place the key s, the numeral k, the candidate z, and the current set Z. The final slots p and q are unused, so satisfaction is independent of their values.
ρ₉ (suc (suc (suc zero))) = i5 ρ₉ (suc (suc (suc (suc zero)))) = i2 ρ₉ (suc (suc (suc (suc (suc zero))))) = i6 ρ₉ (suc (suc (suc (suc (suc (suc zero)))))) = i3
Γ₉ displays this placement, and each agreement with the original seven-slot environment is judgmental reflexivity.
Γ₉ : (T e' k Z e s z p q : CS.S) → CS.S ^ 9 Γ₉ T e' k Z e s z p q = T ∷ e' ∷ k ∷ Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []
The agreements say that, at each renamed slot, the two environments carry the same carrier element. The first three are proved by reflexivity, one per renamed position.
ag₉ : (T e' k Z e s z p q : CS.S) → Ren.Agrees ρ₉ (Γ₉ T e' k Z e s z p q) (Env T e' e s k z Z) ag₉ T e' k Z e s z p q zero = refl ag₉ T e' k Z e s z p q (suc zero) = refl ag₉ T e' k Z e s z p q (suc (suc zero)) = refl
The remaining four agreements are again reflexivity, one per slot; every agreement is a computation, which is what makes the renaming usable inside a satisfaction.
ag₉ T e' k Z e s z p q (suc (suc (suc zero))) = refl ag₉ T e' k Z e s z p q (suc (suc (suc (suc zero)))) = refl ag₉ T e' k Z e s z p q (suc (suc (suc (suc (suc zero))))) = refl ag₉ T e' k Z e s z p q (suc (suc (suc (suc (suc (suc zero)))))) = refl
The renamed body is the body formula pushed through the slot map, living over nine slots while saying the same thing as before.
body₉ : Formula CS.S 9 body₉ = renameFo ρ₉ bodyFo
The reading equation says that satisfying the renamed body over the nine-slot environment is the same proposition as satisfying the body over the seven-slot environment.
body₉-read : (T e' k Z e s z p q : CS.S) → ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩ ≡ ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩ body₉-read T e' k Z e s z p q = cong ⟨_⟩ (Ren.⊨-rename ρ₉ bodyFo (Γ₉ T e' k Z e s z p q)
The proof is the renaming theorem applied with the slot agreement, transported under the bracket of satisfaction.
(Env T e' e s k z Z) (ag₉ T e' k Z e s z p q))
The least-witness formula wraps the renamed body in three more existentials: the numeral, the extended environment, and the table. Satisfaction at the six-slot environment says that a least-witness record exists for the candidate at the current set, key and parameter environment.
opaque leastWitnessFo : Formula CS.S 6 leastWitnessFo = ∃̇ (∃̇ (∃̇ body₉))
The inward reading eliminates the truncated least-witness data and injects the three objects, transporting the body satisfaction along the reading equation of the renamed body.
leastWitness-in : (Z e s z p q : CS.S) → LeastWitness Z e s z → ⟨ (Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ leastWitnessFo ⟩ leastWitness-in Z e s z p q = PT.rec (snd ((Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ leastWitnessFo)) (λ { (T , e' , k , h) → ∣ k , ∣ e' , ∣ T , transport (sym (body₉-read T e' k Z e s z p q)) h ∣₁ ∣₁ ∣₁ })
The outward reading eliminates the three nested existentials in order, each into the truncated continuation, so the formula satisfaction becomes a least-witness record again.
leastWitness-out : (Z e s z p q : CS.S)
→ ⟨ (Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ leastWitnessFo ⟩
→ LeastWitness Z e s z
leastWitness-out Z e s z p q = PT.rec squash₁ at₁
where
The innermost elimination rebuilds the least-witness data from the named table, extended environment and numeral, transporting the body satisfaction along the reading equation. The two outer eliminations supply the bound objects required by this construction.
at₃ : (k e' : CS.S) → Σ[ T ∈ CS.S ] ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩ → LeastWitness Z e s z at₃ k e' (T , h) = ∣ T , e' , k , transport (body₉-read T e' k Z e s z p q) h ∣₁ at₂ : (k : CS.S) → Σ[ e' ∈ CS.S ] ∥ Σ[ T ∈ CS.S ] ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩ ∥₁ → LeastWitness Z e s z
At this point two nested truncations remain: the outer one hides the extension environment e', and the inner one hides the table T. The two eliminations expose them in turn, after which at₃ transports the renamed body proof back to a LeastWitness.
at₂ k (e' , h) = PT.rec squash₁ (at₃ k e') h at₁ : Σ[ k ∈ CS.S ] ∥ Σ[ e' ∈ CS.S ] ∥ Σ[ T ∈ CS.S ] ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩ ∥₁ ∥₁ → LeastWitness Z e s z at₁ (k , h) = PT.rec squash₁ (at₂ k) h
The numeral slot carries a member of the internal ω, and decode-num decodes it: a truncated natural number n together with the equation identifying the entry with the ambient numeral # n. Decoding is the bridge between the internal numbering and the natural-number bookkeeping of the witness data.
private
decode-num : (q : CS.S) → ⟨ fst q ∈ˢ fst ωʟ ⟩ → ∥ Σ[ n ∈ ℕ ] (fst q ≡ # n) ∥₁
decode-num q h = PT.map (λ { (n , e) → lower n , (e ∙ numeralL-fst (lower n)) })
(subst ⟨_⟩ (ω-specL q) h)
LeastWitnessData is the honest data behind a least witness: a natural number n, an assignment g of n indices into the presentation of Z, the equation saying that e is the environment naming those values, and the stage membership placing s in Lset ω.
LeastWitnessData : CS.S → CS.S → CS.S → Type (ℓ-suc ℓ) LeastWitnessData Z e s = Σ[ n ∈ ℕ ] Σ[ g ∈ (Fin n → ⟪ fst Z ⟫) ] ((fst e ≡ env (λ i → ⟪ fst Z ⟫↪ (g i))) × (⟨ fst s ∈ Lset ω ⟩))
The theorem leastWitness-data says that a formula-level least witness determines, up to propositional truncation, a natural arity, an indexed parameter environment over Z, and a proof that the key lies in Lset ω.
opaque leastWitness-data : (Z e s z : CS.S) → LeastWitness Z e s z → ∥ LeastWitnessData Z e s ∥₁ leastWitness-data Z e s z = PT.rec squash₁ body where
The body of the conversion consumes the body satisfaction: it unpacks into the table T, the extension e', the key k, and the body proof, and the numeral entry of the key is decoded first.
body : Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ k ∈ CS.S ] ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩ → ∥ LeastWitnessData Z e s ∥₁ body (T , e' , k , hb) = PT.map at (decode-num k (BodyRd.b-num T e' e s k z Z hb)) where
With the numeral n and the equation naming the key, the data assembles: the length n, the recovered assignment g, the recovery equation for the environment, and the stage membership of s. The seven-entry context is named once so the recovery can address its slots.
at : Σ[ n ∈ ℕ ] (fst k ≡ # n) → LeastWitnessData Z e s at (n , qk) = n , R.g , R.recovers , s∈Lω where γ : CS.S ^ 7 γ = Env T e' e s k z Z
The environment clause recovers an assignment g of indices in Z and proves that e is the graph of their values. Independently, the key clause says that s is a code and is an ordered pair of the successor arity numeral with a formula code.
module R = Recover Z n γ i2 i4 i6 qk refl (BodyRd.b-env T e' e s k z Z hb) using ( g; recovers ) kr : ⟨ fst s ∈ fst C₀ ⟩ × ∥ Σ[ c ∈ V ℓ ] (fst s ≡ pr (# (suc n)) c) ∥₁ kr = KeyIn.keyIn-out i3 i4 γ n qk (BodyRd.b-key T e' e s k z Z hb) s∈Lω : ⟨ fst s ∈ Lset ω ⟩
The stage membership of the key's value is the last piece of the data. It is proved from the pair equation: the second component c of the key is a code, and codes are constructible by the limit stage.
s∈Lω = PT.rec (snd (fst s ∈ Lset ω)) read (kr .snd) where read : Σ[ c ∈ V ℓ ] (fst s ≡ pr (# (suc n)) c) → ⟨ fst s ∈ Lset ω ⟩ read (c , qs) = PT.rec (snd (fst s ∈ Lset ω)) (λ { (χ , qc) → subst (λ w → ⟨ w ∈ Lset ω ⟩) (sym qs)
Both components of the key therefore live in Lset ω: the successor numeral belongs to the limit by the numerals' membership, and pairs of members of a limit stage stay in the limit. Transporting along the pair equation places s in Lset ω, completing LeastWitnessData.
(pr∈limit (# (suc n)) c (numeral∈limit (suc n)) (subst (λ w → ⟨ w ∈ˢ Lset ω ⟩) (sym qc) (snd (limitCode χ)))) }) (freeCode-out (suc n) c (subst (λ u → ⟨ u ∈ fst C₀ ⟩) qs (kr .fst)))
The outward reading of the witness formula now assembles: satisfaction of witFo at (z, Z) unpacks into a table, an extension, a key, and the body proof, and the body proof converts into a truncated LeastWitness. This is the form in which the satisfaction of the Skolem clause is consumed.
witFo-leastWitness : (z Z : CS.S) → ⟨ (z ∷ Z ∷ []) ⊨ witFo ⟩ → ∥ Σ[ e ∈ CS.S ] Σ[ s ∈ CS.S ] LeastWitness Z e s z ∥₁ witFo-leastWitness z Z h = PT.map (λ { (T , e' , e , s , k , hb) → e , s , ∣ T , e' , k , hb ∣₁ }) (witFo-out z Z h)
For comparing two witnesses, we retain seven of the eight body clauses: the numeral, environment, extension, table, membership, stage, and minimality clauses. The key clause is not needed here, because the two witnesses already share s, and uniqueness of the value associated with that key identifies their tables.
private
module WitnessBody (z T e' e s k Z : CS.S)
(hb : ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩) where
module Rd = BodyRd T e' e s k z Z
using ( b-num; b-env; b-cons; b-tab; b-mem; b-stage; b-min )
Two retained clauses immediately give that the extended environment lies in the table and that the witness lies in Lset lam. Once the key numeral is identified with # n, the environment clause also recovers an n-tuple of indices from Z.
h6 = Rd.b-mem hb h7 = Rd.b-stage hb module AtNum (n : ℕ) (qk : fst k ≡ # n) where module R = Recover Z n (Env T e' e s k z Z) i2 i4 i6 qk refl (Rd.b-env hb) using ( g; recovers )
The recovered indices name their ambient values through the presentation of Z, and the recovery equation says that the extension environment names exactly these ambient values, in the order the indices list them.
g′ : Fin n → V ℓ g′ i = ⟪ fst Z ⟫↪ (R.g i) hE : fst e ≡ env g′ hE = R.recovers
To prove uniqueness, take two body witnesses with the same Z, parameter environment e, and formula key s. Decoding the first arity numeral fixes a common length n for the recovered parameter sequence.
module WitnessUnique (Z e s z T e' k : CS.S) (hb : ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩) (z' T₂ e'₂ k₂ : CS.S) (hb₂ : ⟨ Env T₂ e'₂ e s k₂ z' Z ⊨ bodyFo ⟩) (n : ℕ) (qk : fst k ≡ # n) where
The stage clauses turn z and z' into elements of Lset lam. They can therefore be compared by the well-order of that stage, while the decoded first witness supplies the common parameter sequence used for both bodies.
module A₁ = WitnessBody z T e' e s k Z hb module A₂ = WitnessBody z' T₂ e'₂ e s k₂ Z hb₂ module N = A₁.AtNum n qk zS : SL zS = fst z , A₁.h7
The second element is packaged likewise. The extension equations say that each body's environment is the parameter environment extended by its own witnessed element: e' names z consed onto the recovered values, and e'₂ names z' the same way.
z'S : SL z'S = fst z' , A₂.h7 e'≡ : fst e' ≡ env (cons (fst z) N.g′) e'≡ = A₁.Rd.b-cons N.g′ N.hE hb e'₂≡ : fst e'₂ ≡ env (cons (fst z') N.g′)
The two table slots are then shown to agree. Both bodies assert that the pair of the key s and their table belongs to the table family's pairs, and the injectivity of the code naming forces two tables paired with the same key to be equal.
e'₂≡ = A₂.Rd.b-cons N.g′ N.hE hb₂ T≡ : fst T ≡ fst T₂ T≡ = let p = SM.pairs-out s T (A₁.Rd.b-tab hb) q = SM.pairs-out s T₂ (A₂.Rd.b-tab hb₂)
The table equality is assembled from the outward readings of the two table clauses: each table is the value named by the key, and the injectivity of code naming identifies the two keys' code indices. The statement not-below is then prepared: a strictly smaller constructible element with its own body witness cannot have its extension inside the other's table.
in snd p ∙ cong (λ m → fst (SM.valOf s m)) (snd (fst s ∈ fst (AllCodes A)) (fst p) (fst q)) ∙ sym (snd q) not-below : (a b : CS.S) (ha : ⟨ fst a ∈ fst A ⟩) (hb' : ⟨ fst b ∈ fst A ⟩) (Ta e'a ka : CS.S) (hba : ⟨ Env Ta e'a e s ka a Z ⊨ bodyFo ⟩) (e'b : CS.S) → fst e'b ≡ env (cons (fst b) N.g′) → ⟨ fst e'b ∈ fst Ta ⟩
If a constructible candidate lies below one witness and its extended environment belongs to the same table, the minimality clause gives a contradiction. The stage well-order supplies the internal comparison relation needed by that clause.
→ relOf wL (fst b , hb') (fst a , ha) → Empty.⊥ not-below a b ha hb' Ta e'a ka hba e'b qe hm b<a = BodyRd.b-min Ta e'a e s ka a Z N.g′ N.hE hba b hb' e'b qe hm (relL-fill lam λ-isL ordλ (fst b , hb') (fst a , ha) b<a) result : fst z ≡ fst z'
The result follows by the trichotomy of the internal well-order on the two packaged witnesses. If z were below z', the smaller element z would contradict the minimality recorded by z''s body, the shared table supplied through the table equality.
result = go (SWO.tri∙ wL zS z'S) where go : Tri∙ (relOf wL zS z'S) (zS ≡ z'S) (relOf wL z'S zS) → fst z ≡ fst z' go (tri-lt h) = Empty.rec (not-below z' z A₂.h7 A₁.h7 T₂ e'₂ k₂ hb₂ e' e'≡ (subst (λ t → ⟨ fst e' ∈ t ⟩) T≡ A₁.h6) h)
If the two packaged witnesses are equal, their underlying sets are equal. The remaining strict case is symmetric: if z' lies below z, the minimality of z gives a contradiction.
go (tri-eq q) = cong fst q go (tri-gt h) = Empty.rec (not-below z z' A₁.h7 A₂.h7 T e' k hb e'₂ e'₂≡ (subst (λ t → ⟨ fst e'₂ ∈ t ⟩) (sym T≡) A₂.h6) h)
Uniqueness of least witnesses is assembled: two witnesses for the same Z, e and s have equal underlying elements. The two truncations are consumed together, the goal being an equality in an h-set.
opaque leastWitness-unique : (Z e s z z' : CS.S) → LeastWitness Z e s z → LeastWitness Z e s z' → fst z ≡ fst z' leastWitness-unique Z e s z z' = PT.rec2 (setIsSet (fst z) (fst z')) inner where
The inner lemma receives both unpacked body witnesses: tables, extensions, keys, and body satisfactions for the two candidate elements z and z'.
inner : (Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ k ∈ CS.S ] ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩) → (Σ[ T₂ ∈ CS.S ] Σ[ e'₂ ∈ CS.S ] Σ[ k₂ ∈ CS.S ] ⟨ Env T₂ e'₂ e s k₂ z' Z ⊨ bodyFo ⟩) → fst z ≡ fst z'
The first key is decoded to a numeral, allowing the preceding uniqueness argument to run at that arity. The same decoding principle is recorded as ω-num: every member of the internal ω is, up to truncation, an ambient numeral # n.
inner (T , e' , k , hb) (T₂ , e'₂ , k₂ , hb₂) = PT.rec (setIsSet (fst z) (fst z')) (λ { (n , qk) → WitnessUnique.result Z e s z T e' k hb z' T₂ e'₂ k₂ hb₂ n qk }) (decode-num k (BodyRd.b-num T e' e s k z Z hb)) ω-num : (q : CS.S) → ⟨ fst q ∈ˢ fst ωʟ ⟩ → ∥ Σ[ n ∈ ℕ ] (fst q ≡ # n) ∥₁
The decoding maps a member of the internal ω to a natural number with the numeral equation, and vecOf turns a function on Fin k into a length-k vector of constructible elements, the form the satisfaction clauses consume.
ω-num q h = PT.map (λ { (n , e) → lower n , (e ∙ numeralL-fst (lower n)) }) (subst ⟨_⟩ (ω-specL q) h) vecOf : {k : ℕ} → (Fin k → SL) → Vec SL k vecOf {zero} f = [] vecOf {suc k} f = f zero ∷ vecOf (λ i → f (suc i))
Lookups in vecOf f recover f entry by entry. Now fix a set Z, an arity k, a formula χ with one witness variable and k parameter variables, a parameter vector vs drawn from Z, and evidence that χ has a witness at vs.
lookup-vecOf : {k : ℕ} (f : Fin k → SL) (i : Fin k) → lookup i (vecOf f) ≡ f i
lookup-vecOf {suc k} f zero = refl
lookup-vecOf {suc k} f (suc i) = lookup-vecOf (λ j → f (suc j)) i
module Least (Z : CS.S) (k : ℕ) (χ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec SL k)
(from : From Z vs) (w₀ : Sat k χ vs) where
The predicate to be minimized says of an element a that the extended environment (a ∷ vs) satisfies χ. It is packaged as a proposition, so it can serve as the leastness predicate of a well-order.
P : SL → hProp (ℓ-suc ℓ)
P a = (a ∷ vs) ⊨₀ χ
The least witness a is selected by the least-element search along the internal well-order of L, applied to this predicate and the nonemptiness record.
a : SL a = leastOf wL {ℓ'' = ℓ-suc ℓ} lem P w₀ .fst
Its leastness data is kept in full: a satisfies the predicate, and no smaller element of the well-order satisfies it.
a-least : IsLeast wL P a a-least = leastOf wL {ℓ'' = ℓ-suc ℓ} lem P w₀ .snd
Because the chosen witness a belongs to Lset lam, it is constructible and can be viewed as an element aS of the constructible carrier. For each parameter position, g chooses an index in the presentation of Z naming that parameter.
aS : CS.S aS = fst a , Lset→isL lam ordλ (fst a) (snd a) g : Ix Z k g i = fiber (fst Z) (from i) .fst
The naming equation says that each parameter's index presents exactly that parameter: the embedded index equals the parameter as an element of L.
g-val : (i : Fin k) → ⟪ fst Z ⟫↪ (g i) ≡ fst (lookup i vs) g-val i = fiber (fst Z) (from i) .snd
The ambient values of the parameters are collected in g′, one per slot, so that the parameter environment can be described both internally and ambiently.
g′ : Fin k → V ℓ g′ i = ⟪ fst Z ⟫↪ (g i)
The parameter environment e is the internal graph of these values over Z, and ext b is the extension environment for a candidate b: the parameters with b consed in front.
e : CS.S e = envS Z g ext : SL → CS.S ext b = envFor A (b ∷ vs)
The extension's graph equation says that its underlying set is the graph of the candidate consed onto the ambient parameter values, the two readings of the extension being identified entry by entry.
ext-graph : (b : SL) → fst (ext b) ≡ env (cons (fst b) g′) ext-graph b = envFor-graph A (b ∷ vs) ∙ cong env (funExt (λ { zero → refl ; (suc i) → sym (g-val i) }))
The extension belongs to the satisfaction table of χ at arity suc k exactly when the extended environment satisfies χ. The table here is the one for this formula alone, and the equation is what lets membership in the table be traded for satisfaction.
ext-sat : (b : SL) → (ext b CS.∈ˢ Tof (suc k) χ) ≡ ((b ∷ vs) ⊨₀ χ) ext-sat b = sat-at (suc k) χ (b ∷ vs) (ext b) (envFor-graph A (b ∷ vs))
The key sS names the formula and its arity: it is the pair by which the table family indexes the table of χ.
sS : CS.S sS = keyOf (suc k) χ
The table T is the satisfaction table of χ at arity suc k, the set in which satisfying extensions are collected.
T : CS.S T = Tof (suc k) χ
The seven-entry environment γ₇ assembles the whole picture: the table, the extension by the least witness, the parameter environment, the key, the numeral of the arity, the packaged witness, and the base set Z.
γ₇ : CS.S ^ 7 γ₇ = Env T (ext a) e sS (nn k) aS Z
The first clause records that the numeral of the arity belongs to the internal ω, the length of an environment being a natural number.
c1 : ⟨ γ₇ ⊨ (var i4 ∈̇ con ωʟ) ⟩ c1 = #∈ω k
The key clause says that the key belongs to the code set and pairs the successor numeral with the code of χ; the code is a free code, and free codes live in the limit stage of ω.
c2 : ⟨ γ₇ ⊨ keyIn i3 i4 ⟩ c2 = KeyIn.keyIn-in i3 i4 γ₇ k refl (subst (λ u → ⟨ u ∈ˢ fst C₀ ⟩) (sym (keyOf-fst (suc k) χ)) (freeCode-in (suc k) χ)) (fst (limitCode χ)) (keyOf-fst (suc k) χ)
The environment clause says that the parameter environment is an environment of length nn k over Z, with the values g′; it is transported from the environment lemma of e to the seven-entry context.
c3 : ⟨ γ₇ ⊨ envOverAt i2 i4 i6 ⟩ c3 = envOverAt-transport (Z ∷ nn k ∷ e ∷ []) γ₇ i2 i1 i0 i2 i4 i6 refl refl refl (envOver Z g)
The extension equation repeats that the extension by the least witness is the graph of the witness consed onto the parameter values.
c4 : fst (ext a) ≡ env (cons (fst a) g′) c4 = ext-graph a
The pair of the key and the table belongs to the pairs of the table family, which is how the table is indexed by its key.
c5 : ⟨ pr (fst sS) (fst T) ∈ˢ fst SM.pairs ⟩ c5 = Tof-pair (suc k) χ
The extension by the least witness belongs to the table: the table's membership equation reads it as satisfaction of χ, and the leastness data supplies exactly that satisfaction.
c6 : ⟨ fst (ext a) ∈ˢ fst T ⟩ c6 = transport (sym (cong ⟨_⟩ (ext-sat a))) (a-least .fst)
The least witness belongs to the stage Lset lam; in the internal presentation A = LsetS lam ordλ, this is exactly the membership proof carried by a.
c7 : ⟨ fst aS ∈ˢ fst A ⟩ c7 = snd a
The minimality clause excludes every candidate w' in Lset lam whose extended environment belongs to the table: its packaged form cannot lie strictly below the chosen witness. This is precisely the leastness property of a.
c8 : BodyRd.Min T (ext a) e sS (nn k) aS Z g′ c8 w' w'∈ e'' q hm hr = a-least .snd w'S sat lt' where w'S : SL w'S = fst w' , w'∈
The internal relation between the smaller candidate and a is filled from the ambient well-order restricted to constructible elements, and the candidate satisfies χ: its extension belongs to the table, read as satisfaction through the extension equation.
lt' : relOf-at w'S a lt' = relL-rep lam λ-isL ordλ w'S a hr sat : ⟨ (w'S ∷ vs) ⊨₀ χ ⟩ sat = transport (cong ⟨_⟩ (ext-sat w'S)) (subst (λ t → ⟨ t ∈ˢ fst T ⟩) (q ∙ sym (ext-graph w'S)) hm)
The eight clauses together show that witFo holds at (aS, Z): a is the least witness of χ over the chosen parameters, expressed entirely inside the constructible structure. We next read the same body data outward under the assumption that every member of Z lies in Lset lam.
least : ⟨ (aS ∷ Z ∷ []) ⊨ witFo ⟩
least = witFo-in aS Z T (ext a) e sS (nn k)
(BodyRd.b-fill T (ext a) e sS (nn k) aS Z g′ refl c1 c2 c3 c4 c5 c6 c7 c8)
module Out (Z : CS.S) (Z⊆ : (z : S) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
(w T e' e s k : CS.S) (h : ⟨ Env T e' e s k w Z ⊨ bodyFo ⟩) where
A body witness provides eight facts: the arity numeral, key shape, recovered parameter environment, extension equation, indexed table, table membership, stage membership, and minimality. Their outward readings reconstruct the semantic search represented by the code.
module Rd = BodyRd T e' e s k w Z
using ( b-num; b-key; b-env; b-cons; b-tab; b-mem; b-stage; b-min )
The stage clause proves that the witnessed set w belongs to Lset lam. Pairing w with this proof gives wS, the corresponding element of the stage carrier.
wS : SL wS = fst w , Rd.b-stage h
The arity component of a decoded key belongs to the internal ω. Thus, up to propositional truncation, it is some numeral # n; fixing such an n lets us analyze the key at an ordinary natural-number arity.
module AtNum (n : ℕ) (qk : fst k ≡ # n) where
Inside this case, the first fact says that the slot component s of the key is itself a code, that is, a member of C₀. This follows from the key inversion: a key is the ordered pair of an arity numeral and a code, and reading the pair apart exhibits the code.
s∈ : ⟨ fst s ∈ˢ fst C₀ ⟩ s∈ = KeyIn.keyIn-out i3 i4 (Env T e' e s k w Z) n qk (Rd.b-key h) .fst
With the arity identified as n, the environment clause recovers a function g : Fin n → ⟪ fst Z ⟫ and proves that the coded parameter environment is the graph of the values named by those indices.
module R = Recover Z n (Env T e' e s k w Z) i2 i4 i6 qk refl (Rd.b-env h) using ( g; recovers )
The recovered environment lists indices into the starting set. Each index is presented as an ambient element by the embedding of its presentation, giving the vector g′ of underlying sets.
g′ : Fin n → V ℓ g′ i = ⟪ fst Z ⟫↪ (R.g i)
The vector vs collects the same elements as entries of the constructible carrier, pairing each with the proof that it is constructible.
vs : Vec SL n vs = vecOf (λ i → g′ i , Z⊆ (g′ i) (member (fst Z) (R.g i)))
For every position i, the first component of lookup i vs is g′ i. Thus vs and g′ describe the same parameter sequence, once as elements of the stage carrier and once as ambient sets.
vs-val : (i : Fin n) → fst (lookup i vs) ≡ g′ i vs-val i = cong fst (lookup-vecOf (λ i → g′ i , Z⊆ (g′ i) (member (fst Z) (R.g i))) i)
The recovered environment genuinely comes from the starting set: each entry of vs, read as a set, is a member of Z. This is the From Z vs record.
from : From Z vs from i = subst (λ u → ⟨ u ∈ˢ fst Z ⟩) (sym (vs-val i)) (member (fst Z) (R.g i))
The recovery equation identifies the original environment component e with env g′, the graph formed from the recovered ambient values.
hE : fst e ≡ env g′ hE = R.recovers
The witness slot is compared with other candidates by extending the recovered environment by one entry: ext b is the environment with b prepended to vs.
ext : SL → CS.S ext b = envFor A (b ∷ vs)
The underlying environment of this extension computes to the cons of the underlying set of b with g′: the graph description of the extended environment matches entry by entry.
ext-graph : (b : SL) → fst (ext b) ≡ env (cons (fst b) g′) ext-graph b = envFor-graph A (b ∷ vs) ∙ cong env (funExt (λ { zero → refl ; (suc i) → vs-val i }))
The key's own environment component is identified with ext wS: extending the recovered environment by the witness slot is exactly what the key recorded.
e'≡ : fst e' ≡ fst (ext wS) e'≡ = Rd.b-cons g′ hE h ∙ sym (ext-graph wS)
Now choose the formula χ decoded from the code component and identify s with its canonical key keyOf (suc n) χ. The environment, formula, and key then all describe the same satisfaction query.
module AtCode (χ : Formula (⊥* {ℓ}) (suc n)) (qs : fst s ≡ fst (keyOf (suc n) χ)) where
The predicate P b says that b, prepended to the recovered environment, satisfies χ. It is the property that the least-witness search minimizes over.
P : SL → hProp (ℓ-suc ℓ) P b = (b ∷ vs) ⊨₀ χ
Membership in the satisfaction table of χ agrees with P b, because the environment of ext b computes to the graph of b ∷ vs. This converts between the coded and the semantic readings of satisfaction.
ext-sat : (b : SL) → ⟨ ext b CS.∈ˢ Tof (suc n) χ ⟩ ≡ ⟨ P b ⟩ ext-sat b = cong ⟨_⟩ (sat-at (suc n) χ (b ∷ vs) (ext b) (envFor-graph A (b ∷ vs)))
The table component of the key is next identified with the satisfaction table of χ at the raised arity; with both components decoded, the key's member can be read semantically.
module AtTable (qT : fst T ≡ fst (Tof (suc n) χ)) where
The witness slot satisfies the recovered formula: the membership recorded in the key is transported along the environment and table identifications into satisfaction of χ at the extended environment.
sat : ⟨ P wS ⟩ sat = transport (ext-sat wS) (subst2 (λ u t → ⟨ u ∈ˢ t ⟩) e'≡ qT (Rd.b-mem h))
Leastness says that no stage element b satisfying χ lies below wS. Satisfaction of χ is converted into membership of ext b in the recovered table, and the stage well-order is converted into the internal relation required by the body's minimality clause.
min : (b : SL) → ⟨ P b ⟩ → relOf-at b wS → Empty.⊥ min b pb lt = Rd.b-min g′ hE h bS (snd b) (ext b) (ext-graph b) hm (relL-fill lam λ-isL ordλ b wS lt) where bS : CS.S
The smaller candidate is packaged as a constructible element bS, and its extended environment is shown to lie in the table, which is exactly the membership the minimality of the key refutes.
bS = fst b , Lset→isL lam ordλ (fst b) (snd b) hm : ⟨ fst (ext b) ∈ˢ fst T ⟩ hm = subst (λ t → ⟨ fst (ext b) ∈ˢ t ⟩) (sym qT) (transport (sym (ext-sat b)) pb)
The two facts combine into a satisfiability witness for χ at the recovered environment: the witness slot, together with its satisfaction, is truncated into Sat.
w₀ : Sat n χ vs w₀ = ∣ wS , sat ∣₁
The recovered arity n, formula χ, parameter vector vs, and witness w₀ form a semantic search. Uniqueness of least elements identifies its result search n χ vs w₀ with the original witnessed set w; separately, the table clause begins the proof that the recovered table is the satisfaction table of χ.
searched : Searched Z (fst w) searched = n , χ , vs , w₀ , (from , sym (cong (λ q → fst (fst q)) (isPropLeastOf wL P (leastOf wL {ℓ'' = ℓ-suc ℓ} lem P w₀) (wS , (sat , min))))) table : ∥ Searched Z (fst w) ∥₁ table = ∣ AtTable.searched
The table clause presents the underlying set of T as the value associated with the key s. Since s has already been identified with the canonical key of χ at arity suc n, uniqueness of the value at that key yields fst T ≡ fst (Tof (suc n) χ).
(snd p ∙ cong fst (valOf-same s (fst p) (suc n) χ qs)) ∣₁ where p : Σ[ m ∈ ⟨ s CS.∈ˢ AllCodes A ⟩ ] (fst T ≡ fst (SM.valOf s m)) p = SM.pairs-out s T (Rd.b-tab h)
To decode the code component s, freeCode-out supplies a formula χ whose free code is that component. The equation for the slot, the decoded code equation, and the computation of keyOf then identify s with the canonical key of χ.
code : ∥ Searched Z (fst w) ∥₁ code = PT.rec squash₁ (λ { (c , qc) → PT.rec squash₁ (λ { (χ , ec) → AtCode.table χ (qc ∙ cong (pr (# (suc n))) ec ∙ sym (keyOf-fst (suc n) χ)) })
The key equation supplies the final link between the coded slot and the decoded formula. Consequently this numeral case yields a truncated Searched Z (fst w): the witnessed set is exactly the least-witness search result for parameters recovered from Z.
(freeCode-out (suc n) c (subst (λ u → ⟨ u ∈ˢ fst C₀ ⟩) qc s∈)) }) (KeyIn.keyIn-out i3 i4 (Env T e' e s k w Z) n qk (Rd.b-key h) .snd)
Since the arity recorded in every body witness belongs to the internal ω, numeral decoding turns the preceding analysis into a truncated semantic search for every such witness. For separation, choose the bound Bnd Z = Z ∪ A, where A is the internal presentation of Lset lam.
searched : ∥ Searched Z (fst w) ∥₁ searched = PT.rec squash₁ (λ { (n , qk) → AtNum.code n qk }) (ω-num k (Rd.b-num h)) Bnd : CS.S → CS.S Bnd Z = cupʟ Z A
Members of Z lie in the bound by the left inclusion of the union.
bnd-Z : (Z z : CS.S) → ⟨ fst z ∈ˢ fst Z ⟩ → ⟨ z CS.∈ˢ Bnd Z ⟩ bnd-Z Z z = cupʟ-inl Z A (fst z)
Every member of Lset lam lies in Bnd Z through the right inclusion. The one-step closure condition then has three cases: an old member of Z, the empty set used when no witness exists, or a set w satisfying witFo with base Z.
bnd-L : (Z z : CS.S) → ⟨ fst z ∈ˢ Lset lam ⟩ → ⟨ z CS.∈ˢ Bnd Z ⟩ bnd-L Z z = cupʟ-inr Z A (fst z) Body : CS.S → CS.S → Type (ℓ-suc ℓ) Body Z w = ⟨ fst w ∈ˢ fst Z ⟩ ⊎ ((fst w ≡ ∅) ⊎ ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩)
In the third case, the stage clause encoded by witFo proves directly that w ∈ Lset lam. Thus every newly adjoined least witness lies inside the fixed stage.
wit-L : (Z w : CS.S) → ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩ → ⟨ fst w ∈ˢ Lset lam ⟩ wit-L Z w hw = PT.rec (snd (fst w ∈ˢ Lset lam)) (λ { (T , e' , e , s , k , h) → BodyRd.b-stage T e' e s k w Z h }) (witFo-out w Z hw) opaque
The separation formula expresses these three cases inside the constructible structure: membership in Z, equality with the empty set, or the renamed formula witFo. The renaming places its two free variables in the slots created by the existential wrapper.
sepFo : CS.S → Formula CS.S 1 sepFo Z = (var i0 ∈̇ con Z) ∨̇ ( (var i0 ≐ con ∅ʟ) ∨̇ ∃̇ ( (var i0 ≐ con Z) ∧̇ renameFo ρs witFo ) )
The renaming merely exchanges the two environment entries. Hence evaluating the renamed witFo at (Z'', w) has the same truth value as evaluating the original witFo at (w, Z'').
private rs : (Z'' w : CS.S) → ⟨ (Z'' ∷ w ∷ []) ⊨ renameFo ρs witFo ⟩ ≡ ⟨ (w ∷ Z'' ∷ []) ⊨ witFo ⟩ rs Z'' w = cong ⟨_⟩ (Ren.⊨-rename ρs witFo (Z'' ∷ w ∷ []) (w ∷ Z'' ∷ []) (ags Z'' w))
Satisfaction of the separation formula decomposes into the three truncated cases of the body: membership in Z, equality with the empty set, or an existential whose witness identifies the domain.
sep-out : (Z w : CS.S) → ⟨ (w ∷ []) ⊨ sepFo Z ⟩ → ∥ Body Z w ∥₁ sep-out Z w = PT.rec squash₁ (λ { (inl hz) → ∣ inl hz ∣₁ ; (inr h') → PT.rec squash₁ (λ { (inl e) → ∣ inr (inl e) ∣₁
In the existential case, its witness Z'' is equal to the fixed parameter Z. Transporting along this equality and then along the renaming path yields witFo at (w, Z).
; (inr hw) → PT.map (λ { (Z'' , (eZ , hr)) → inr (inr (subst (λ u → ⟨ (w ∷ u ∷ []) ⊨ witFo ⟩) (S≡ {x = Z''} {y = Z} eZ) (transport (rs Z'' w) hr))) }) hw }) h' })
Conversely, each of the three cases of the body produces the corresponding satisfaction of the separation formula, re-wrapping the renaming where needed.
sep-in : (Z w : CS.S) → Body Z w → ⟨ (w ∷ []) ⊨ sepFo Z ⟩ sep-in Z w (inl hz) = ∣ inl hz ∣₁ sep-in Z w (inr (inl e)) = ∣ inr ∣ inl e ∣₁ ∣₁ sep-in Z w (inr (inr hw)) = ∣ inr ∣ inr ∣ Z , (refl , transport (sym (rs Z w)) hw) ∣₁ ∣₁ ∣₁
Separation inside L selects from Bnd Z exactly the sets satisfying sepFo Z; call the resulting constructible set Φ Z. Its membership path identifies membership in Φ Z with membership in the bound together with satisfaction of the formula.
opaque Φ : CS.S → CS.S Φ Z = hasSeparationL (Bnd Z) (sepFo Z) .fst .fst
The membership specification reads: w belongs to Φ Z exactly when w belongs to the bound and satisfies the separation formula.
Φ-mem : (Z w : CS.S) → (w CS.∈ˢ Φ Z) ≡ ((w CS.∈ˢ Bnd Z) ⊓ ((w ∷ []) ⊨ sepFo Z)) Φ-mem Z = hasSeparationL (Bnd Z) (sepFo Z) .fst .snd
Every body case lands in Φ Z. The membership case enters through the bound; the proof packages the bound membership produced from each disjunct together with its separation satisfaction.
Φ-in : (Z w : CS.S) → Body Z w → ⟨ fst w ∈ˢ fst (Φ Z) ⟩ Φ-in Z w b = subst ⟨_⟩ (sym (Φ-mem Z w)) (bnd b , sep-in Z w b) where bnd : Body Z w → ⟨ w CS.∈ˢ Bnd Z ⟩ bnd (inl hz) = bnd-Z Z w hz
The empty-set case lies in the bound because ∅ ∈ Lset lam. The witness case lies there because the stage clause of witFo proves its value belongs to Lset lam.
bnd (inr (inl e)) = bnd-L Z w (subst (λ u → ⟨ u ∈ˢ Lset lam ⟩) (sym e) HSH.∅∈Lsetα) bnd (inr (inr hw)) = bnd-L Z w (wit-L Z w hw)
Conversely, membership in Φ Z yields a truncated body case, by the membership specification and the separation reading. For the biconditional formula, the body is then rewritten in a three-slot arrangement.
Φ-out : (Z w : CS.S) → ⟨ fst w ∈ˢ fst (Φ Z) ⟩ → ∥ Body Z w ∥₁ Φ-out Z w h = sep-out Z w (subst ⟨_⟩ (Φ-mem Z w) h .snd) opaque bodyF : Formula CS.S 3 bodyF = (var i0 ∈̇ var i2) ∨̇ ((var i0 ≐ con ∅ʟ) ∨̇ renameFo ρf witFo)
The graph formula ΦFo quantifies over a fresh set w and states both implications between w ∈ Z' and the three-case condition Body Z w. Thus (Z', Z) satisfies ΦFo exactly when Z' has the same members as Φ Z.
ΦFo : Formula CS.S 2
ΦFo = ∀̇ ( ((var i0 ∈̇ var i1) ⇒̇ bodyF) ∧̇ (bodyF ⇒̇ (var i0 ∈̇ var i1)) )
The renaming equivalence for the graph is proved like the earlier one: the renaming permutes the environment, and satisfaction transfers along the permutation.
private rf : (w Z' Z : CS.S) → ⟨ (w ∷ Z' ∷ Z ∷ []) ⊨ renameFo ρf witFo ⟩ ≡ ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩ rf w Z' Z = cong ⟨_⟩ (Ren.⊨-rename ρf witFo (w ∷ Z' ∷ Z ∷ []) (w ∷ Z ∷ []) (agf w Z' Z))
The body transfers across the three-slot arrangement in both directions: membership in Z is direct, and the remaining disjuncts are mapped through the truncation.
bodyF-out : (w Z' Z : CS.S) → ⟨ (w ∷ Z' ∷ Z ∷ []) ⊨ bodyF ⟩ → ∥ Body Z w ∥₁ bodyF-out w Z' Z = PT.rec squash₁ (λ { (inl hz) → ∣ inl hz ∣₁ ; (inr h') → PT.map (λ { (inl e) → inr (inl e)
In the witness case, the renaming path converts satisfaction of the three-slot formula back to witFo at (w, Z), completing the forward implication from the graph body to Body Z w.
; (inr hw) → inr (inr (transport (rf w Z' Z) hw)) }) h' })
The converse assembles the three cases into the three-slot reading, transporting the witness disjunct against the renaming.
bodyF-in : (w Z' Z : CS.S) → Body Z w → ⟨ (w ∷ Z' ∷ Z ∷ []) ⊨ bodyF ⟩ bodyF-in w Z' Z (inl hz) = ∣ inl hz ∣₁ bodyF-in w Z' Z (inr (inl e)) = ∣ inr ∣ inl e ∣₁ ∣₁ bodyF-in w Z' Z (inr (inr hw)) = ∣ inr ∣ inr (transport (sym (rf w Z' Z)) hw) ∣₁ ∣₁
The definability clause is then proved: the pair (Φ Z, Z) satisfies the graph formula. Each direction of the biconditional is the corresponding membership direction composed with the body transfer.
Φ-defines : (Z : CS.S) → ⟨ (Φ Z ∷ Z ∷ []) ⊨ ΦFo ⟩ Φ-defines Z w = (λ h → PT.rec (snd ((w ∷ Φ Z ∷ Z ∷ []) ⊨ bodyF)) (bodyF-in w (Φ Z) Z) (Φ-out Z w h)) , (λ h → PT.rec (snd (fst w ∈ˢ fst (Φ Z))) (Φ-in Z w) (bodyF-out w (Φ Z) Z h))
Uniqueness of the graph is proved by extensionality of the constructible structure: for any Z' whose pair with Z satisfies the graph formula, every member of Z' satisfies the body, and Φ-in places it in Φ Z.
Φ-only : (Z Z' : CS.S) → ⟨ (Z' ∷ Z ∷ []) ⊨ ΦFo ⟩ → Z' ≡ Φ Z Φ-only Z Z' h = extensionalL (λ v → ⇔toPath (fwd v) (bwd v)) where fwd : (v : CS.S) → ⟨ fst v ∈ˢ fst Z' ⟩ → ⟨ fst v ∈ˢ fst (Φ Z) ⟩ fwd v hv = PT.rec (snd (fst v ∈ˢ fst (Φ Z))) (Φ-in Z v) (bodyF-out v Z' Z (h v .fst hv))
The backward direction of the extensionality argument reads each member of Φ Z as a truncated body case and applies the graph formula at that member.
bwd : (v : CS.S) → ⟨ fst v ∈ˢ fst (Φ Z) ⟩ → ⟨ fst v ∈ˢ fst Z' ⟩ bwd v hv = h v .snd (PT.rec (snd ((v ∷ Z' ∷ Z ∷ []) ⊨ bodyF)) (bodyF-in v Z' Z) (Φ-out Z v hv))
We have therefore obtained a definable one-step operation Φ: the formula ΦFo characterizes its graph, and extensionality proves that any set satisfying that graph condition is equal to Φ Z.
pack : StepPack pack = record { Φ = Φ ; ΦFo = ΦFo ; defines = Φ-defines
This step contains every old member of Z, always contains the empty set, and contains the least witness for every satisfiable formula with parameters from Z. Conversely, its members arise only from these three cases, so Φ is exactly the desired one-step closure.
; only = Φ-only ; grows = λ Z z hz → Φ-in Z (z , isL-trans {x = fst Z} {y = z} hz (snd Z)) (inl hz) ; junk = λ Z → Φ-in Z ∅ʟ (inr (inl refl)) ; least = λ Z k χ vs from w₀ → Φ-in Z (Least.aS Z k χ vs from w₀) (inr (inr (Least.least Z k χ vs from w₀)))
Assume every member of Z lies in Lset lam. If z ∈ Φ Z, the membership characterization gives three possibilities: z was already in Z, z = ∅, or witFo holds at (z, Z). In the third case, decoding the body reconstructs a semantic search from parameters in Z whose result is z.
; out = λ Z Z⊆ z hz → PT.rec squash₁ (λ { (inl h') → ∣ inl h' ∣₁ ; (inr (inl e)) → ∣ inr (inl e) ∣₁ ; (inr (inr hw)) → PT.rec squash₁ (λ { (T , e' , e , s , k , hb) →
In the witness case, z ∈ Φ Z first makes z constructible, so it can be read as an element of the constructible carrier. The decoded body then proves Searched Z z, identifying z with the least-witness search determined by the recovered formula and parameters.
PT.map (λ sr → inr (inr sr)) (Out.searched Z Z⊆ (zS Z z hz) T e' e s k hb) }) (witFo-out (zS Z z hz) Z hw) }) (Φ-out Z (zS Z z hz) hz) } where zS : (Z : CS.S) (z : S) → ⟨ z ∈ˢ fst (Φ Z) ⟩ → CS.S
Since Φ Z is constructible and constructibility is transitive, every member z of Φ Z is constructible.
zS Z z hz = z , isL-trans {x = fst (Φ Z)} {y = z} hz (snd (Φ Z))
Supplying the constructibility premise for condensation
This supplies the carrier element needed in the preceding decoding and completes the construction of the definable one-step closure.
module Discharge (lam : S) (ordλ : IsOrd lam) (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩) (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩) (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
Assume that the hull M is itself constructible. This turns M into a constructible carrier, so the preceding collapse argument applies without requiring the hull to be transitive.
(M-isL : ⟨ isL (HullStage.M lam ordλ succλ X X⊆L ∅∈λ) ⟩) where
Regarded as a constructible carrier, M has a collapse image πX. Every member of this image is the collapse value of some member of M, and the constructible-carrier theorem proves that such values belong to L.
module HS = HullStage lam ordλ succλ X X⊆L ∅∈λ using ( M ) module HSC = HullStage.C lam ordλ succλ X X⊆L ∅∈λ using ( πX ) module P = PiIn (HS.M , M-isL) using ( πX-isL )
Consequently, every x ∈ πX is constructible. We now return to the hull generated from X inside Lset λ, assuming that λ is an ordinal closed under successors and that every member of X lies in this stage.
pixL : (x : S) → ⟨ x ∈ˢ HSC.πX ⟩ → ⟨ isL x ⟩ pixL = P.πX-isL module Condense′ (lam : S) (ordλ : IsOrd lam) (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩) (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)
We also assume that ∅ ∈ λ, that the hull frame generated by X is elementary, that λ is superadequate, and that X itself is constructible. The last assumption supplies the base of the internal finite iteration; elementarity and superadequacy supply the hypotheses needed for condensation.
(∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) (elem : Frame.A.Elementary lam ordλ succλ X X⊆L ∅∈λ) (sup : Superadequate lam) (X-isL : ⟨ isL X ⟩) where
The construction has three connected parts. Codes name the initial elements and the values selected by later searches, using the empty set when a search has no witness; one definable operation Φ performs a closure step; and finite iteration of Φ, followed by union, builds a constructible set that will be identified with the Skolem hull.
module T = Telescope lam ordλ succλ X X⊆L ∅∈λ using ( Code; val; Reads; module StepPack ) module TB = Telescope.Build lam ordλ succλ X X⊆L ∅∈λ using ( pack; Φ ) module HI = Telescope.HullIter lam ordλ succλ X X⊆L ∅∈λ X-isL TB.pack using ( hullL; hullL-spec; hullStep; hullStep-suc; hullStep-in; hullStep⊆Hull; depth; M-isL ) module HS = HullStage lam ordλ succλ X X⊆L ∅∈λ using ( M )
The union of the finite closure stages is already an element hullL of the constructible universe. The next equality shows that its underlying set is precisely the externally defined hull M; this will supply the constructibility premise used above for the collapse image.
module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ using ( Hull⊆L ) module HSC = HullStage.C lam ordλ succλ X X⊆L ∅∈λ using ( πX ) module D = Discharge lam ordλ succλ X X⊆L ∅∈λ HI.M-isL using ( pixL ) hullL : CS.S hullL = HI.hullL
The underlying set of hullL is exactly M. Hence the external characterization of the Skolem hull and the constructible set obtained by iteration describe the same members, while hullL additionally carries a proof of constructibility.
hullL-spec : fst hullL ≡ HS.M hullL-spec = HI.hullL-spec
The closure stages of the hull are indexed by natural numbers: hullStep n is the stage reached after n applications of the closure step.
hullStep : ℕ → CS.S hullStep = HI.hullStep
At a successor index, the next stage is Φ applied to the current one. This operation retains the current members, includes the empty set, and adjoins the least witness for each coded search whose parameters are already present.
hullStep-suc : (n : ℕ) → hullStep (suc n) ≡ TB.Φ (hullStep n) hullStep-suc = HI.hullStep-suc
Each code has a finite depth, and the value it denotes belongs to the closure stage at that depth. Since every hull member is represented by a code, this gives a finite stage containing it, without choosing a canonical code for the member.
hullStep-in : (c : T.Code) → ⟨ fst (T.val c) ∈ˢ fst (hullStep (HI.depth c)) ⟩ hullStep-in = HI.hullStep-in
Conversely, every member of every finite closure stage belongs to M. Together with the coded description of hull members, this proves that the union of the stages and the Skolem hull have exactly the same elements.
hullStep⊆Hull : (n : ℕ) (z : S) → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ HS.M ⟩ hullStep⊆Hull = HI.hullStep⊆Hull
The union of the stages is constructible: the hull stage M is an element of L. This is the first of the two membership facts the chapter set out to prove.
M-isL : ⟨ isL HS.M ⟩ M-isL = HI.M-isL
The second follows through the discharge: every value of the collapse πX of the hull stage is constructible, because the carrier M is.
pixL : (x : S) → ⟨ x ∈ˢ HSC.πX ⟩ → ⟨ isL x ⟩ pixL = D.pixL
Condensation now yields an ordinal β for which the collapse image is exactly Lset β. The earlier memberwise constructibility statement is thereby strengthened to an identification of the whole image with one stage of the constructible hierarchy. The conclusion asserts this equality and the ordinality of β; it makes no further comparison between β and λ.
condenses′ : Σ[ β ∈ S ] (IsOrd β × (HSC.πX ≡ Lset β)) condenses′ = Condense.condenses lam ordλ succλ X X⊆L ∅∈λ elem sup D.pixL