BedrockWell-formed keys
The half of "is a code" that closedness does not say.
closedAt is eight implications keyed by tag: if a member has this tag, then its parts are members too. Nothing there rules out a member with no recognized tag at all, and such a member satisfies all eight vacuously. So a closed set may hold junk, and the predicate that says otherwise is this one: every member is an arity-tagged pair whose tag is one of the twelve, with a payload of the shape that tag calls for.
The four leaf tags are delegated to a parameter. Their payloads mention term codes and a numeral, never a formula code, so nothing about them descends and nothing about them belongs in the same induction; they are written once, elsewhere, and handed in.
Shapedness is stated at two slots, not one: the set, and a carrier the terms inside it draw their constants from. The second slot is what makes a member the key of a formula over that carrier rather than over the whole model, and it is the conjunct the code set was caught between two statements without. Written at a slot rather than as a constant, it is threaded through everything below and re-indexes nothing.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth module L.Coding.Shape {ℓ : Level} where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Term; Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇ ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) open import FOL.Manipulation.Relabelling using ( mapTm; mapFo ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr; #mono; module VCode ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_; sucV ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Model {ℓ} using ( tagAtL; tagAtL-adequate ; closedAt; binShapeAt; unShapeAt; bothSameAt; oneSameAt ; oneSuccAt; succSndAt ; binSameClosed-out; unSameClosed-out ; unSuccClosed-out; binSuccClosed-out ; arityTagAtL; arityTagAtL-adequate ; arityTagPairAtL; arityTagPairAtL-adequate; numL ) open import L.Coding.InL {ℓ} using ( closure-inv; key; codeL; codeTmL ) open import L.Coding.Closed {ℓ} using ( clo ) open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst ) open import L.Ordinal {ℓ} using ( ∈#-elim ) open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.FinData using ( toℕ ) open import Cubical.Data.FinData.Properties using ( fromℕ'; toFromId'; toℕ<n ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁; squash₁ ) open import Cubical.Data.Sum using ( _⊎_; inl; inr ) open import Cubical.Data.Unit using ( tt* ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
The two payload frames
A tag whose payload is a pair, and a tag whose payload is a single code. Twelve tags, two shapes: which one a tag takes is the only thing that varies, and the rest of what a tag demands of its payload is a relation the frame carries. That is the same division the closedness predicate makes, and for the same reason.
module _ {n : ℕ} where binForm : ℕ → Formula S (4 + n) → Formula S (suc n) binForm k rel = ∃̇ (∃̇ (∃̇ (arityTagPairAtL (suc (suc (suc zero))) (suc (suc zero)) k (suc zero) zero ∧̇ rel))) unForm : ℕ → Formula S (3 + n) → Formula S (suc n) unForm k rel = ∃̇ (∃̇ (arityTagAtL (suc (suc zero)) (suc zero) k zero ∧̇ rel))
Term codes
The four tags whose payloads reach outside the formula codes need one predicate, and it is not recursive: a term is a constant or a variable, and neither has a part. Both alternatives are bounded, and by different things.
A variable's index must lie below the arity, which is what makes the formula the code of a term at that arity rather than at some larger one. A constant must be a member of the carrier, which is what makes it the code of a term over that alphabet rather than over the whole model. This second conjunct is the one the code set was caught between two statements without: with no bound on a constant, a payload read back as one is an arbitrary element of L, and the class the decode lands in is wider than the class the introduction starts from.
Both bounds are memberships at a slot, and both slots are named by the caller. The carrier is a slot rather than a constant on purpose. A constant would pin every predicate below this line to one carrier, and everything indexed by them would be re-indexed at the pair; a slot is threaded, and threading is free.
isTmAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n isTmAt t N A = ∃̇ (tagAtL (suc t) 0 zero ∧̇ (var zero ∈̇ var (suc A))) ∨̇ ∃̇ (tagAtL (suc t) 1 zero ∧̇ (var zero ∈̇ var (suc N)))
The twelve, as one predicate
Every member is a well-formed key: an arity-tagged pair carrying one of the twelve tags, with the payload that tag calls for. The relations say what closedness does not: that an atom's two parts are term codes, that a bounded quantifier's first part is one, and that a constant's payload is zero. The formula parts are left to closedness, which is where they belong, since they are the only parts anything descends into.
Being shaped is therefore relative to two slots and not one: the set, and the carrier its terms name their constants from. Only the four relations that mention a term look at the second, and they are the only four that could.
module _ {n : ℕ} where bothTm fstTm : Fin n → Formula S (4 + n) bothTm A = isTmAt (suc zero) (suc (suc zero)) (suc (suc (suc (suc A)))) ∧̇ isTmAt zero (suc (suc zero)) (suc (suc (suc (suc A)))) fstTm A = isTmAt (suc zero) (suc (suc zero)) (suc (suc (suc (suc A)))) noneB : Formula S (4 + n) noneB = ⊤̇ {n = 4 + n} zeroPay noneU : Formula S (3 + n) zeroPay = var zero ≐ con (numeralL 0) noneU = ⊤̇ {n = 3 + n} shapes : Fin n → Formula S (suc n) shapes A = binForm 0 (bothTm A) ∨̇ (binForm 1 (bothTm A) ∨̇ (binForm 2 noneB ∨̇ (binForm 3 noneB ∨̇ (binForm 4 noneB ∨̇ (unForm 5 noneU ∨̇ (unForm 6 zeroPay ∨̇ (unForm 7 zeroPay ∨̇ (unForm 8 noneU ∨̇ (unForm 9 noneU ∨̇ (binForm 10 (fstTm A) ∨̇ binForm 11 (fstTm A))))))))))) shapedAt : Fin n → Fin n → Formula S n shapedAt C A = ∀̇∈ (var C) (shapes A)
What a member is, read flat
Twelve alternatives. The two frames are read once each, generically in the relation they carry, so that the walk over the disjunction below is twelve applications of two readers rather than twelve copies of the same unnesting.
BinWit : ∀ {n} → ℕ → Formula S (4 + n) → S ^ n → S → Type (ℓ-suc ℓ) BinWit k rel γ c = Σ[ N ∈ S ] (Σ[ a ∈ S ] (Σ[ b ∈ S ] ((fst c ≡ pr (fst N) (pr (# k) (pr (fst a) (fst b)))) × ⟨ (b ∷ a ∷ N ∷ c ∷ γ) ⊨ rel ⟩))) UnWit : ∀ {n} → ℕ → Formula S (3 + n) → S ^ n → S → Type (ℓ-suc ℓ) UnWit k rel γ c = Σ[ N ∈ S ] (Σ[ a ∈ S ] ((fst c ≡ pr (fst N) (pr (# k) (fst a))) × ⟨ (a ∷ N ∷ c ∷ γ) ⊨ rel ⟩)) binForm-out : ∀ {n} (k : ℕ) (rel : Formula S (4 + n)) (γ : S ^ n) (c : S) → ⟨ (c ∷ γ) ⊨ binForm k rel ⟩ → ∥ BinWit k rel γ c ∥₁ binForm-out k rel γ c = PT.rec squash₁ (λ { (N , hN) → PT.rec squash₁ (λ { (a , ha) → PT.map (λ { (b , (hb , hr)) → N , (a , (b , (subst ⟨_⟩ (arityTagPairAtL-adequate (suc (suc (suc zero))) (suc (suc zero)) k (suc zero) zero (b ∷ a ∷ N ∷ c ∷ γ)) hb , hr))) }) ha }) hN }) unForm-out : ∀ {n} (k : ℕ) (rel : Formula S (3 + n)) (γ : S ^ n) (c : S) → ⟨ (c ∷ γ) ⊨ unForm k rel ⟩ → ∥ UnWit k rel γ c ∥₁ unForm-out k rel γ c = PT.rec squash₁ (λ { (N , hN) → PT.map (λ { (a , (ha , hr)) → N , (a , (subst ⟨_⟩ (arityTagAtL-adequate (suc (suc zero)) (suc zero) k zero (a ∷ N ∷ c ∷ γ)) ha , hr)) }) hN }) ShapeWit : ∀ {n} → Fin n → S ^ n → S → Type (ℓ-suc ℓ) ShapeWit A γ c = BinWit 0 (bothTm A) γ c ⊎ (BinWit 1 (bothTm A) γ c ⊎ (BinWit 2 noneB γ c ⊎ (BinWit 3 noneB γ c ⊎ (BinWit 4 noneB γ c ⊎ (UnWit 5 noneU γ c ⊎ (UnWit 6 zeroPay γ c ⊎ (UnWit 7 zeroPay γ c ⊎ (UnWit 8 noneU γ c ⊎ (UnWit 9 noneU γ c ⊎ (BinWit 10 (fstTm A) γ c ⊎ BinWit 11 (fstTm A) γ c)))))))))) shaped-out : ∀ {n} (C A : Fin n) (γ : S ^ n) → ⟨ γ ⊨ shapedAt C A ⟩ → (c : S) → ⟨ c ∈ˢ lookup C γ ⟩ → ∥ ShapeWit A γ c ∥₁ shaped-out C A γ h c c∈ = d1 (h c c∈) where d11 = PT.rec squash₁ (λ { (inl x) → PT.map inl (binForm-out 10 (fstTm A) γ c x) ; (inr x) → PT.map inr (binForm-out 11 (fstTm A) γ c x) }) d10 = PT.rec squash₁ (λ { (inl x) → PT.map inl (unForm-out 9 noneU γ c x) ; (inr x) → PT.map inr (d11 x) }) d9 = PT.rec squash₁ (λ { (inl x) → PT.map inl (unForm-out 8 noneU γ c x) ; (inr x) → PT.map inr (d10 x) }) d8 = PT.rec squash₁ (λ { (inl x) → PT.map inl (unForm-out 7 zeroPay γ c x) ; (inr x) → PT.map inr (d9 x) }) d7 = PT.rec squash₁ (λ { (inl x) → PT.map inl (unForm-out 6 zeroPay γ c x) ; (inr x) → PT.map inr (d8 x) }) d6 = PT.rec squash₁ (λ { (inl x) → PT.map inl (unForm-out 5 noneU γ c x) ; (inr x) → PT.map inr (d7 x) }) d5 = PT.rec squash₁ (λ { (inl x) → PT.map inl (binForm-out 4 noneB γ c x) ; (inr x) → PT.map inr (d6 x) }) d4 = PT.rec squash₁ (λ { (inl x) → PT.map inl (binForm-out 3 noneB γ c x) ; (inr x) → PT.map inr (d5 x) }) d3 = PT.rec squash₁ (λ { (inl x) → PT.map inl (binForm-out 2 noneB γ c x) ; (inr x) → PT.map inr (d4 x) }) d2 = PT.rec squash₁ (λ { (inl x) → PT.map inl (binForm-out 1 (bothTm A) γ c x) ; (inr x) → PT.map inr (d3 x) }) d1 = PT.rec squash₁ (λ { (inl x) → PT.map inl (binForm-out 0 (bothTm A) γ c x) ; (inr x) → PT.map inr (d2 x) })
The same twelve, written
A predicate written to be consumed proves nothing until something satisfies it. The decode takes a shaped set as a hypothesis, so whoever supplies the set owes that hypothesis, and owing it means building: an existential frame has its witnesses to produce and a disjunct to choose, where the elimination had only to take them apart.
The two frames are introduced once each, generically in the relation, for the reason that decided the elimination and for one more. The adequacy equation each frame carries is discharged here, with the tag, the relation and the environment all still variables. Discharged at a named tag instead, it would be twelve unfoldings of a formula three quantifiers deep, and that is the difference between a second and an afternoon.
binForm-in : ∀ {n} (k : ℕ) (rel : Formula S (4 + n)) (γ : S ^ n) (c : S) → BinWit k rel γ c → ⟨ (c ∷ γ) ⊨ binForm k rel ⟩ binForm-in k rel γ c (N , (a , (b , (e , hr)))) = ∣ N , ∣ a , ∣ b , (subst ⟨_⟩ (sym (arityTagPairAtL-adequate (suc (suc (suc zero))) (suc (suc zero)) k (suc zero) zero (b ∷ a ∷ N ∷ c ∷ γ))) e , hr) ∣₁ ∣₁ ∣₁ unForm-in : ∀ {n} (k : ℕ) (rel : Formula S (3 + n)) (γ : S ^ n) (c : S) → UnWit k rel γ c → ⟨ (c ∷ γ) ⊨ unForm k rel ⟩ unForm-in k rel γ c (N , (a , (e , hr))) = ∣ N , ∣ a , (subst ⟨_⟩ (sym (arityTagAtL-adequate (suc (suc zero)) (suc zero) k zero (a ∷ N ∷ c ∷ γ))) e , hr) ∣₁ ∣₁
The walk over the disjunction is the mirror of the walk that reads it: twelve injections into a right-nested chain, each level carrying its own truncation because a disjunction of the truth algebra is a truncated sum. The injections are written out rather than named, because a lemma generic in the two disjuncts would have to recover them from a goal that has already been unfolded, and no amount of unification recovers a formula from its meaning. What the caller is left owing is exactly one thing per member: which of the twelve that member is.
shaped-in : ∀ {n} (C A : Fin n) (γ : S ^ n) → ((c : S) → ⟨ c ∈ˢ lookup C γ ⟩ → ∥ ShapeWit A γ c ∥₁) → ⟨ γ ⊨ shapedAt C A ⟩ shaped-in C A γ g c c∈ = PT.rec (snd ((c ∷ γ) ⊨ shapes A)) fill (g c c∈) where fill : ShapeWit A γ c → ⟨ (c ∷ γ) ⊨ shapes A ⟩ fill (inl x) = ∣ inl (binForm-in 0 (bothTm A) γ c x) ∣₁ fill (inr (inl x)) = ∣ inr ∣ inl (binForm-in 1 (bothTm A) γ c x) ∣₁ ∣₁ fill (inr (inr (inl x))) = ∣ inr ∣ inr ∣ inl (binForm-in 2 noneB γ c x) ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inl x)))) = ∣ inr ∣ inr ∣ inr ∣ inl (binForm-in 3 noneB γ c x) ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inl x))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inl (binForm-in 4 noneB γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inr (inl x)))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inl (unForm-in 5 noneU γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inr (inr (inl x))))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inl (unForm-in 6 zeroPay γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inr (inr (inr (inl x)))))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inl (unForm-in 7 zeroPay γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inr (inr (inr (inr (inl x))))))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inl (unForm-in 8 noneU γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inr (inr (inr (inr (inr (inl x)))))))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inl (unForm-in 9 noneU γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inl x))))))))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inl (binForm-in 10 (fstTm A) γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ fill (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr x))))))))))) = ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr ∣ inr (binForm-in 11 (fstTm A) γ c x) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁
Terms, recovered
The first decode, and the only one that needs no induction. A term is a constant or a variable: the constant case reads its payload back as a constant of the alphabet, and the variable case reads an index out of the arity numeral. Each case spends exactly the bound its disjunct carries, and neither could be written without one. Nothing here descends, which is why it is separable from the recursion that follows and why it is written first.
What the term is produced over is a parameter, and it is what the chapter is for. The alphabet is any type with an embedding into the hierarchy, and the constant case needs one thing the shape predicate cannot supply: that the carrier's members are the alphabet's image. That is a hypothesis, because it is a fact about the pair (alphabet, carrier) and not about the code. At the one instantiation that matters, the alphabet is the carrier's own member type and the hypothesis is the presentation of a set by its members, so it costs a discharge rather than a construction.
The two disjuncts are read by two named lemmas and the reader is their case split, which is not a matter of taste. Written as two clauses of one function, each carrying its own truncation under a disjunction that also carries one, the chapter did not finish in ten minutes; with each disjunct's reading given a written type of its own it checks in under two seconds. The rule is the elaborator's, not the mathematics': a branch whose type is written is solved against that type, and a branch whose type is inferred is solved against the whole disjunction.
module _ {K : Type ℓ} (f : K → V ℓ) where TmWit : ℕ → V ℓ → Type (ℓ-suc ℓ) TmWit n x = Σ[ t ∈ Term K n ] (VCode.⌜ mapTm f t ⌝ᵗ ≡ x) Onto : ∀ {m} → Fin m → S ^ m → Type (ℓ-suc ℓ) Onto A γ = (y : V ℓ) → ⟨ y ∈ fst (lookup A γ) ⟩ → ∥ Σ[ c ∈ K ] (f c ≡ y) ∥₁ tmCon : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ) → Onto A γ → ⟨ γ ⊨ ∃̇ (tagAtL (suc t) 0 zero ∧̇ (var zero ∈̇ var (suc A))) ⟩ → ∥ TmWit n (fst (lookup t γ)) ∥₁ tmCon t N A γ n onto = PT.rec squash₁ (λ { (y , (hy , y∈)) → PT.map (λ { (c , qc) → con c , ( cong (VCode.mkTag 0) qc ∙ sym (subst ⟨_⟩ (tagAtL-adequate (suc t) 0 zero (y ∷ γ)) hy) ) }) (onto (fst y) y∈) }) tmVar : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ) → fst (lookup N γ) ≡ # n → ⟨ γ ⊨ ∃̇ (tagAtL (suc t) 1 zero ∧̇ (var zero ∈̇ var (suc N))) ⟩ → ∥ TmWit n (fst (lookup t γ)) ∥₁ tmVar t N A γ n qN = PT.rec squash₁ (λ { (z , (hz , z∈)) → PT.map (λ { (j , (j<n , ez)) → var (fromℕ' n j j<n) , ( cong (VCode.mkTag 1) (cong #_ (toFromId' n j j<n) ∙ sym ez) ∙ sym (subst ⟨_⟩ (tagAtL-adequate (suc t) 1 zero (z ∷ γ)) hz) ) }) (∈#-elim n (fst z) (subst (λ w → ⟨ fst z ∈ w ⟩) qN z∈)) }) isTmAt-decode : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ) → fst (lookup N γ) ≡ # n → Onto A γ → ⟨ γ ⊨ isTmAt t N A ⟩ → ∥ TmWit n (fst (lookup t γ)) ∥₁ isTmAt-decode t N A γ n qN onto = PT.rec squash₁ (λ { (inl h) → tmCon t N A γ n onto h ; (inr h) → tmVar t N A γ n qN h })
Terms, encoded
The same two clauses read backwards, and the only place in the introduction half where anything has to be computed rather than repackaged. Each clause now owes its own bound as well as its tag equation, and the two are owed to different parties. A constant is its own code, so its tag equation is nothing at all, and what it owes is that the constant is a member of the carrier: a hypothesis here, because only the caller knows which carrier it meant. A variable has to put its index inside the arity numeral, which is the other bound working in the direction it was designed for: the decode read an index out of a numeral, and here a numeral is shown to hold one. That second fact was already on hand, since a smaller numeral belonging to a larger one is exactly what made distinct numerals distinct.
module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where isTmAt-in : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ) → fst (lookup N γ) ≡ # n → ((c : K) → ⟨ f c ∈ fst (lookup A γ) ⟩) → TmWit f n (fst (lookup t γ)) → ⟨ γ ⊨ isTmAt t N A ⟩ isTmAt-in t N A γ n qN into (con c , e) = ∣ inl ∣ y , ( subst ⟨_⟩ (sym (tagAtL-adequate (suc t) 0 zero (y ∷ γ))) (sym e) , into c ) ∣₁ ∣₁ where y : S y = f c , h c isTmAt-in t N A γ n qN into (var i , e) = ∣ inr ∣ z , ( subst ⟨_⟩ (sym (tagAtL-adequate (suc t) 1 zero (z ∷ γ))) (sym e ∙ cong (VCode.mkTag 1) (sym (numeralL-fst (toℕ i)))) , subst (λ w → ⟨ fst z ∈ w ⟩) (sym qN) (subst (λ w → ⟨ w ∈ (# n) ⟩) (sym (numeralL-fst (toℕ i))) (#mono (toℕ i) n (toℕ<n i))) ) ∣₁ ∣₁ where z : S z = numeralL (toℕ i)
One layer off
The two halves meet. Shapedness says which of the twelve a member is and hands back its parts; closedness says those parts are members too, at the arity the tag calls for. Neither half alone gives a step of a recursion, and together they give exactly one.
The equation shapedness produces is, letter for letter, the one closedness consumes, so the two compose with nothing in between. That is not luck: both were written against the same reading of an arity-tagged pair.
module Peel {m : ℕ} (C A : Fin m) (γ : S ^ m) (hcl : ⟨ γ ⊨ closedAt C ⟩) (hsh : ⟨ γ ⊨ shapedAt C A ⟩) where private D : V ℓ D = fst (lookup C γ) BinSame BinSucc : ℕ → S → Type (ℓ-suc ℓ) BinSame k c = Σ[ N ∈ S ] (Σ[ a ∈ S ] (Σ[ b ∈ S ] ((fst c ≡ pr (fst N) (pr (# k) (pr (fst a) (fst b)))) × (⟨ pr (fst N) (fst a) ∈ D ⟩ × ⟨ pr (fst N) (fst b) ∈ D ⟩)))) BinSucc k c = Σ[ N ∈ S ] (Σ[ a ∈ S ] (Σ[ b ∈ S ] ((fst c ≡ pr (fst N) (pr (# k) (pr (fst a) (fst b)))) × (⟨ (a ∷ N ∷ c ∷ γ) ⊨ isTmAt zero (suc zero) (suc (suc (suc A))) ⟩ × ⟨ pr (sucV (fst N)) (fst b) ∈ D ⟩)))) UnSame UnSucc : ℕ → S → Type (ℓ-suc ℓ) UnSame k c = Σ[ N ∈ S ] (Σ[ a ∈ S ] ((fst c ≡ pr (fst N) (pr (# k) (fst a))) × ⟨ pr (fst N) (fst a) ∈ D ⟩)) UnSucc k c = Σ[ N ∈ S ] (Σ[ a ∈ S ] ((fst c ≡ pr (fst N) (pr (# k) (fst a))) × ⟨ pr (sucV (fst N)) (fst a) ∈ D ⟩)) PeelWit : S → Type (ℓ-suc ℓ) PeelWit c = BinWit 0 (bothTm A) γ c ⊎ (BinWit 1 (bothTm A) γ c ⊎ (BinSame 2 c ⊎ (BinSame 3 c ⊎ (BinSame 4 c ⊎ (UnSame 5 c ⊎ (UnWit 6 zeroPay γ c ⊎ (UnWit 7 zeroPay γ c ⊎ (UnSucc 8 c ⊎ (UnSucc 9 c ⊎ (BinSucc 10 c ⊎ BinSucc 11 c)))))))))) peel : (c : S) → ⟨ c ∈ˢ lookup C γ ⟩ → ∥ PeelWit c ∥₁ peel c c∈ = PT.map fill (shaped-out C A γ hsh c c∈) where bs : (k : ℕ) → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩ → BinWit k noneB γ c → BinSame k c bs k h (N , (a , (b , (e , _)))) = N , (a , (b , (e , binSameClosed-out C k γ h c N a b c∈ e))) us : (k : ℕ) → ⟨ γ ⊨ unShapeAt C k (oneSameAt C) ⟩ → UnWit k noneU γ c → UnSame k c us k h (N , (a , (e , _))) = N , (a , (e , unSameClosed-out C k γ h c N a c∈ e)) uz : (k : ℕ) → ⟨ γ ⊨ unShapeAt C k (oneSuccAt C) ⟩ → UnWit k noneU γ c → UnSucc k c uz k h (N , (a , (e , _))) = N , (a , (e , unSuccClosed-out C k γ h c N a c∈ e)) bz : (k : ℕ) → ⟨ γ ⊨ binShapeAt C k (succSndAt C) ⟩ → BinWit k (fstTm A) γ c → BinSucc k c bz k h (N , (a , (b , (e , hr)))) = N , (a , (b , (e , (hr , binSuccClosed-out C k γ h c N a b c∈ e)))) fill : ShapeWit A γ c → PeelWit c fill (inl x) = inl x fill (inr (inl x)) = inr (inl x) fill (inr (inr (inl x))) = inr (inr (inl (bs 2 (hcl .fst) x))) fill (inr (inr (inr (inl x)))) = inr (inr (inr (inl (bs 3 (hcl .snd .fst) x)))) fill (inr (inr (inr (inr (inl x))))) = inr (inr (inr (inr (inl (bs 4 (hcl .snd .snd .fst) x))))) fill (inr (inr (inr (inr (inr (inl x)))))) = inr (inr (inr (inr (inr (inl (us 5 (hcl .snd .snd .snd .fst) x)))))) fill (inr (inr (inr (inr (inr (inr (inl x))))))) = inr (inr (inr (inr (inr (inr (inl x)))))) fill (inr (inr (inr (inr (inr (inr (inr (inl x)))))))) = inr (inr (inr (inr (inr (inr (inr (inl x))))))) fill (inr (inr (inr (inr (inr (inr (inr (inr (inl x))))))))) = inr (inr (inr (inr (inr (inr (inr (inr (inl (uz 8 (hcl .snd .snd .snd .snd .fst) x))))))))) fill (inr (inr (inr (inr (inr (inr (inr (inr (inr (inl x)))))))))) = inr (inr (inr (inr (inr (inr (inr (inr (inr (inl (uz 9 (hcl .snd .snd .snd .snd .snd .fst) x)))))))))) fill (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inl x))))))))))) = inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inl (bz 10 (hcl .snd .snd .snd .snd .snd .snd .fst) x))))))))))) fill (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr x))))))))))) = inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (bz 11 (hcl .snd .snd .snd .snd .snd .snd .snd) x)))))))))))
The closure is shaped
What the predicate is for. A recursion over codes is handed an index set, and that set has to be closed or the clauses constrain nothing, and shaped or they admit junk. Closedness was discharged for the closure a chapter ago; this is the other half, and it is the shorter one, because shapedness asks nothing about what a member drags in with it. Half of what the inversion returns is therefore dropped on the floor.
The analysis is on the constructor alone. The tag is not a second index to be matched against: it is computed from the constructor, exactly as
byTag computes the closedness demand from it, so the table is twelve lines and not twelve times twelve. Nothing here recurses either, because the key of a named constructor already computes to the arity-tagged pair the witness type asks for, and no transport is needed anywhere in the twelve tuples.
The one thing a tuple cannot compute is the term witness: a payload slot holding a term code must be certified as one, and the certificate is the encoder above applied to the term the constructor carries. That certificate now has a second half, and the caller pays it: every constant of the alphabet is a member of the carrier. It is one hypothesis, discharged once per call rather than once per constructor, because the alphabet is fixed before the formula is.
The first half, on the other hand, got cheaper. The witness a term owes is that its code is the code of some term, and over the alphabet the code of a term already is that: the encoder is the identity with refl beside it. On the model's own coding it had to bridge two codings first.
module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where private cd : ∀ {n} → Formula K n → S cd φ = VCode.⌜ mapFo f φ ⌝ , codeL f h φ ct : ∀ {n} → Term K n → S ct t = VCode.⌜ mapTm f t ⌝ᵗ , codeTmL f h t nn : ℕ → S nn n = # n , numL n tw : ∀ {n} (t : Term K n) → TmWit f n (fst (ct t)) tw t = t , refl closureShaped : ∀ {n m} (φ : Formula K n) (A : Fin m) (γ : S ^ m) → ((k : K) → ⟨ f k ∈ fst (lookup A γ) ⟩) → ⟨ (clo f h φ ∷ γ) ⊨ shapedAt zero (suc A) ⟩ closureShaped φ A γ into = shaped-in zero (suc A) (clo f h φ ∷ γ) (λ c c∈ → PT.map (λ { (_ , ψ , q , _) → go ψ c q }) (closure-inv f h φ (fst c) c∈)) where tm1 : ∀ {k} (t : Term K k) (b c : S) → ⟨ (b ∷ ct t ∷ nn k ∷ c ∷ clo f h φ ∷ γ) ⊨ isTmAt (suc zero) (suc (suc zero)) (suc (suc (suc (suc (suc A))))) ⟩ tm1 {k} t b c = isTmAt-in f h (suc zero) (suc (suc zero)) (suc (suc (suc (suc (suc A))))) (b ∷ ct t ∷ nn k ∷ c ∷ clo f h φ ∷ γ) k refl into (tw t) tm0 : ∀ {k} (u : Term K k) (a c : S) → ⟨ (ct u ∷ a ∷ nn k ∷ c ∷ clo f h φ ∷ γ) ⊨ isTmAt zero (suc (suc zero)) (suc (suc (suc (suc (suc A))))) ⟩ tm0 {k} u a c = isTmAt-in f h zero (suc (suc zero)) (suc (suc (suc (suc (suc A))))) (ct u ∷ a ∷ nn k ∷ c ∷ clo f h φ ∷ γ) k refl into (tw u) go : ∀ {k} (ψ : Formula K k) (c : S) → fst c ≡ key f h ψ → ShapeWit (suc A) (clo f h φ ∷ γ) c go {k} (t ∈̇ u) c q = inl (nn k , (ct t , (ct u , (q , (tm1 t (ct u) c , tm0 u (ct t) c))))) go {k} (t ≐ u) c q = inr (inl (nn k , (ct t , (ct u , (q , (tm1 t (ct u) c , tm0 u (ct t) c)))))) go {k} (a ∧̇ b) c q = inr (inr (inl (nn k , (cd a , (cd b , (q , tt*)))))) go {k} (a ∨̇ b) c q = inr (inr (inr (inl (nn k , (cd a , (cd b , (q , tt*))))))) go {k} (a ⇒̇ b) c q = inr (inr (inr (inr (inl (nn k , (cd a , (cd b , (q , tt*)))))))) go {k} (¬̇ a) c q = inr (inr (inr (inr (inr (inl (nn k , (cd a , (q , tt*)))))))) go {k} ⊤̇ c q = inr (inr (inr (inr (inr (inr (inl (nn k , (nn 0 , (q , sym (numeralL-fst 0)))))))))) go {k} ⊥̇ c q = inr (inr (inr (inr (inr (inr (inr (inl (nn k , (nn 0 , (q , sym (numeralL-fst 0))))))))))) go {k} (∃̇ a) c q = inr (inr (inr (inr (inr (inr (inr (inr (inl (nn k , (cd a , (q , tt*))))))))))) go {k} (∀̇ a) c q = inr (inr (inr (inr (inr (inr (inr (inr (inr (inl (nn k , (cd a , (q , tt*)))))))))))) go {k} (∀̇∈ t a) c q = inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inl (nn k , (ct t , (cd a , (q , tm1 t (cd a) c)))))))))))))) go {k} (∃̇∈ t a) c q = inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (inr (nn k , (ct t , (cd a , (q , tm1 t (cd a) c))))))))))))))