--- title: "Syntax as sets" module: FOL.Coding lang: en site: "Bedrock" description: "Syntax as sets" stage: "First-order logic" reading_order: 19 canonical: https://bedrock.institute/en/FOL.Coding.html html: FOL.Coding.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Coding.lagda.md prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax] routes: [common-foundations] translations: [https://bedrock.institute/zh/FOL.Coding.md, https://bedrock.institute/ja/FOL.Coding.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Syntax as sets A model can quantify only over elements of its carrier, whereas terms and formulas initially live in the surrounding type theory. To make syntax available inside the model, this chapter assigns each term and formula an element of the carrier. A code is a tagged pair: the numeric tag identifies the outer constructor, and the payload contains the codes of its immediate parts. Set constants can appear directly as payloads because they already belong to the carrier. The construction assumes an injective pairing operation and an injective map from natural numbers. These hypotheses make both components recoverable from a tagged pair. The chapter first proves that term codes are injective, then defines formula codes for all ten constructors. It also gives the constant and membership cases of relational coding through `CodesT` and `Codes`. Finally, a tag-indexed description of constructor shapes supports the proof that equal codes determine equal formulas of the same arity. To encode syntax as sets, two operations on the carrier would suffice on their own, but injectivity is what makes decoding possible: if two pieces of syntax received the same set, the coding could not be inverted. This chapter therefore works over a structure `๐’ฎ` of type `ZFStructure`, whose equality and membership take values in `hProp โ„“`, and takes the encoding data as explicit module parameters. Every definition below is stated for an arbitrary structure with such data; the cumulative hierarchy will supply an instance in a later chapter. ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import FOL.ZFStructure using ( ZFStructure ) module FOL.Coding {โ„“} (๐’ฎ : ZFStructure โ„“) ``` The two pieces of data are an injective pairing and an injective numeral map. `pr` takes two elements of the carrier `S` to their pair, and `pr-inj` says the pairing can be taken apart again: an equality `pr a b โ‰ก pr c d` returns both `a โ‰ก c` and `b โ‰ก d` as a pair of paths. `encโ„•` sends each natural number to an element of `S`, and `encโ„•-inj` says distinct numbers land at distinct elements. These are exactly the hypotheses the tagged-pair construction will consume; nothing else about `๐’ฎ` enters the chapter. ```agda (pr : ZFStructure.S ๐’ฎ โ†’ ZFStructure.S ๐’ฎ โ†’ ZFStructure.S ๐’ฎ) (pr-inj : โˆ€ {a b c d} โ†’ pr a b โ‰ก pr c d โ†’ (a โ‰ก c) ร— (b โ‰ก d)) (encโ„• : โ„• โ†’ ZFStructure.S ๐’ฎ) (encโ„•-inj : โˆ€ {j k} โ†’ encโ„• j โ‰ก encโ„• k โ†’ j โ‰ก k) where ``` The objects being coded come from the syntax layer: the inductive types `Term` and `Formula`, built from two term constructors (`con` for a set constant, `var` for a variable) and ten formula constructors, from the atoms `_โˆˆฬ‡_` and `_โ‰_` through the connectives and the bounded and unbounded quantifiers. From the structure itself, only the carrier `S` is used, since coding attaches no set-theoretic operation to syntax. The empty type appears only as the codomain of impossible equations, in proofs that certain codes cannot coincide. ```agda open ZFStructure ๐’ฎ using ( S ) open import FOL.Syntax using ( Term; con; var; Formula ; _โˆˆฬ‡_; _โ‰_; _โˆงฬ‡_; _โˆจฬ‡_; _โ‡’ฬ‡_; โŠฅฬ‡; โˆƒฬ‡_; โˆ€ฬ‡_; โˆ€ฬ‡โˆˆ; โˆƒฬ‡โˆˆ ) import Cubical.Data.Empty as Empty ``` Two small arithmetic facts support the injectivity proofs. First, structurally distinct numerals are never equal: the lemmas `znots` and `snotz` refute `0 โ‰ก suc k` and `suc j โ‰ก 0`, and these are exactly the clashes that occur when two formulas with different tags are assumed to share a code. Second, a variable index in `Fin n` is converted to a natural number by `toโ„•`, and `inj-toโ„•` records that this conversion is injective, so coding a variable by its index loses no information. ```agda open import Cubical.Data.Nat using ( znots; snotz ) open import Cubical.Data.FinData using ( toโ„•; inj-toโ„• ) ``` ## Tagged pairs The one construction: a constructor index paired with a payload. Injectivity comes straight from the two parameters, and the clash pattern packages the case that will recur whenever two different constructors are compared. The building block is `mkTag k x = pr (encโ„• k) x`: the tag is the numeral of `k` and the payload is `x`, both elements of `S` since `pr` returns one. A small example shows how the tag separates shapes: the code of a constant will be `mkTag 0 x`, while the code of a variable with index `i` will be `mkTag 1 (encโ„• (toโ„• i))`. If two tagged pairs were equal, the tags would have to agree; `mkTag-inj` makes this precise, composing `pr-inj` and `encโ„•-inj` to return `(j โ‰ก k) ร— (x โ‰ก y)`. Its dual, `clash`, handles the negative case: given a proof that the tags `j` and `k` cannot be equal, it extracts the tag equation from an equality of tagged pairs and contradicts that proof, concluding in any type `A` of the ambient level. ```agda mkTag : โ„• โ†’ S โ†’ S mkTag k x = pr (encโ„• k) x mkTag-inj : โˆ€ {j k x y} โ†’ mkTag j x โ‰ก mkTag k y โ†’ (j โ‰ก k) ร— (x โ‰ก y) mkTag-inj p = encโ„•-inj (pr-inj p .fst) , pr-inj p .snd clash : โˆ€ {j k x y} {A : Type โ„“} โ†’ (j โ‰ก k โ†’ Empty.โŠฅ) โ†’ mkTag j x โ‰ก mkTag k y โ†’ A ``` The body of `clash` runs this argument in one line. `mkTag-inj p .fst` is the equation `j โ‰ก k` extracted from the assumed equality of codes; feeding it to the hypothesis `ne` yields an element of the empty type, and `Empty.rec` eliminates that element to return a value of the arbitrary type `A`. Whenever two constructor shapes force numerals `0` and `suc _` to be equal, `clash` converts the arithmetic refutation into the needed conclusion. ```agda clash ne p = Empty.rec (ne (mkTag-inj p .fst)) ``` ## Codes Terms first, where the promised elegance appears: a set constant needs no encoding, since it is already a set, and only the variable index has to be injected. Terms are separated enough that their injectivity is immediate. A term in context `n` codes as an element of `S` by the two clauses above. A constant `con x` gets tag `0` and payload `x`, the set itself: the promised economy, since no encoding of the payload is needed. A variable `var i` gets tag `1` and payload the numeral of `toโ„• i`, so the tag and the index live on different sides of the pair and cannot be confused. The injectivity proof splits by the constructors of both terms. In the constant-constant case only the payloads can differ, so `mkTag-inj p .snd` is directly `x โ‰ก y`, and `cong con` lifts it to `con x โ‰ก con y`. ```agda โŒœ_โŒแต— : โˆ€ {n} โ†’ Term S n โ†’ S โŒœ con x โŒแต— = mkTag 0 x โŒœ var i โŒแต— = mkTag 1 (encโ„• (toโ„• i)) โŒœโŒแต—-inj : โˆ€ {n} (t u : Term S n) โ†’ โŒœ t โŒแต— โ‰ก โŒœ u โŒแต— โ†’ t โ‰ก u โŒœโŒแต—-inj (con x) (con y) p = cong con (mkTag-inj p .snd) ``` The remaining branches complete the argument. In a mixed case, an equality of codes would force the numerals `0` and `1` to be equal; since `1` is a successor, `znots` or `snotz` refutes this, and `clash` turns the refutation into an equality of terms. In the variable-variable case the payload equation says `encโ„• (toโ„• i) โ‰ก encโ„• (toโ„• j)`; `encโ„•-inj` yields `toโ„• i โ‰ก toโ„• j`, and `inj-toโ„•` promotes it to `i โ‰ก j`, from which `cong var` gives `var i โ‰ก var j`. Every branch ends in an equation of terms, so for each fixed `n` the code function is injective on `Term S n`. Note that `n` here is the number of available variable slots, not the number of variables a particular term actually uses. ```agda โŒœโŒแต—-inj (con x) (var j) p = clash znots p โŒœโŒแต—-inj (var i) (con y) p = clash snotz p โŒœโŒแต—-inj (var i) (var j) p = cong var (inj-toโ„• (encโ„•-inj (mkTag-inj p .snd))) ``` Then formulas: ten constructors, ten tags. Binary constructors pair the two sub-codes, unary ones take the sub-code bare, and falsity takes a dummy payload since its tag already determines it. Formulas use the same tagged-pair scheme, with tags `0` through `4` on the five binary constructors. A membership atom `t โˆˆฬ‡ u` codes as tag `0` paired with the pair of the two term codes, and equality likewise at tag `1`; each connective pairs the codes of its two immediate subformulas. Compare this with terms: there the payload was a bare set or a numeral, here it may itself be a built-up code, so the whole structure of a formula nests inside payloads. The recursion happens on the host inductive types `Term` and `Formula`, never on the sets themselves. ```agda โŒœ_โŒ : โˆ€ {n} โ†’ Formula S n โ†’ S โŒœ t โˆˆฬ‡ u โŒ = mkTag 0 (pr โŒœ t โŒแต— โŒœ u โŒแต—) โŒœ t โ‰ u โŒ = mkTag 1 (pr โŒœ t โŒแต— โŒœ u โŒแต—) โŒœ ฯ† โˆงฬ‡ ฯˆ โŒ = mkTag 2 (pr โŒœ ฯ† โŒ โŒœ ฯˆ โŒ) โŒœ ฯ† โˆจฬ‡ ฯˆ โŒ = mkTag 3 (pr โŒœ ฯ† โŒ โŒœ ฯˆ โŒ) ``` Implication takes tag `4` like the other connectives. Falsity `โŠฅฬ‡` is the one constructor with no parts: its tag `5` alone determines it, so the payload is the dummy numeral `encโ„• 0`, present only so every code has the uniform form of a tagged pair. The unbounded quantifiers `โˆƒฬ‡` and `โˆ€ฬ‡` are unary; their codes are tag `6` or `7` paired directly with the subformula's code. ```agda โŒœ ฯ† โ‡’ฬ‡ ฯˆ โŒ = mkTag 4 (pr โŒœ ฯ† โŒ โŒœ ฯˆ โŒ) โŒœ โŠฅฬ‡ โŒ = mkTag 5 (encโ„• 0) โŒœ โˆƒฬ‡ ฯ† โŒ = mkTag 6 โŒœ ฯ† โŒ โŒœ โˆ€ฬ‡ ฯ† โŒ = mkTag 7 โŒœ ฯ† โŒ โŒœ โˆ€ฬ‡โˆˆ t ฯ† โŒ = mkTag 8 (pr โŒœ t โŒแต— โŒœ ฯ† โŒ) ``` The bounded quantifiers close the list with tags `8` and `9`. Each pairs the code of its bounding term with the code of its body. The arities reflect binding: the bounding term lives in the same context `n` as the whole formula, while the body has arity `suc n`, one extra variable slot for the bound variable. With this, every formula constructor has a distinct tag, and the tag plus payload determines the formula, which the next section proves. ```agda โŒœ โˆƒฬ‡โˆˆ t ฯ† โŒ = mkTag 9 (pr โŒœ t โŒแต— โŒœ ฯ† โŒ) ``` ## The coding relation The module next records the first cases of a relational presentation of coding. `CodesT s t` relates a set to a term, and `Codes s ฯ†` relates a set to a formula. In this file the former contains the constant case and the latter the membership case. `CodesT` has the constructor `c-con`, which relates the code `mkTag 0 x` to the constant `con x`. The constructor `c-โˆˆ` of `Codes` takes derivations for the two term codes and relates their paired payload under tag `0` to the membership formula. These declarations cover exactly the cases shown here; the formula-code injectivity proof below proceeds directly from `โŒœ_โŒ`. ```agda data CodesT {n : โ„•} : S โ†’ Term S n โ†’ Type โ„“ where c-con : (x : S) โ†’ CodesT (mkTag 0 x) (con x) data Codes : {n : โ„•} โ†’ S โ†’ Formula S n โ†’ Type โ„“ where c-โˆˆ : โˆ€ {n s s'} {t u : Term S n} โ†’ CodesT s t โ†’ CodesT s' u โ†’ Codes (mkTag 0 (pr s s')) (t โˆˆฬ‡ u) ``` ## Codes determine formulas Two formulas of the same arity with the same code are equal. Rather than compare every pair of the ten constructors directly, the proof separates a formula code into its numeric tag and payload. A type family indexed by the tag describes the corresponding constructor shape, and pairing injectivity supplies equalities of the tags and payloads. The proof then recurses only through the payload components. The section is a proof by tag separation. Its first ingredient, `tagOf`, extracts the constructor index of a formula as a natural number, using the same numbering that `โŒœ_โŒ` used to build codes: membership `0`, equality `1`, conjunction `2`, disjunction `3`. So `โŒœ_โŒ` builds the tag into a set while `tagOf` reads it back out, and the section works because these two numberings agree. ```agda tagOf : โˆ€ {n} โ†’ Formula S n โ†’ โ„• tagOf (t โˆˆฬ‡ u) = 0 tagOf (t โ‰ u) = 1 tagOf (a โˆงฬ‡ b) = 2 tagOf (a โˆจฬ‡ b) = 3 ``` The remaining clauses assign `4` through `9` to implication, falsity, the two unbounded quantifiers, and the two bounded quantifiers. Every formula therefore has a tag in `0` through `9`, and no two constructors share one, which is exactly what makes the tag able to identify the constructor shape. ```agda tagOf (a โ‡’ฬ‡ b) = 4 tagOf โŠฅฬ‡ = 5 tagOf (โˆƒฬ‡ a) = 6 tagOf (โˆ€ฬ‡ a) = 7 tagOf (โˆ€ฬ‡โˆˆ t a) = 8 ``` The second ingredient, `payOf`, extracts the payload the same way: for membership and equality it is the pair of the two term codes, and for conjunction the pair of the two subformula codes. Each clause is the payload component of the matching clause of `โŒœ_โŒ`, so reading a code with `tagOf` and `payOf` recovers exactly the data `โŒœ_โŒ` put in. ```agda tagOf (โˆƒฬ‡โˆˆ t a) = 9 payOf : โˆ€ {n} โ†’ Formula S n โ†’ S payOf (t โˆˆฬ‡ u) = pr โŒœ t โŒแต— โŒœ u โŒแต— payOf (t โ‰ u) = pr โŒœ t โŒแต— โŒœ u โŒแต— payOf (a โˆงฬ‡ b) = pr โŒœ a โŒ โŒœ b โŒ ``` Disjunction and implication pair the two sub-codes, and the unbounded quantifiers return the single sub-code. Falsity is the case where extraction must agree with construction by convention: since `โŒœ โŠฅฬ‡ โŒ` named the dummy numeral `encโ„• 0` as payload, `payOf โŠฅฬ‡` names the same value rather than omitting the clause. ```agda payOf (a โˆจฬ‡ b) = pr โŒœ a โŒ โŒœ b โŒ payOf (a โ‡’ฬ‡ b) = pr โŒœ a โŒ โŒœ b โŒ payOf โŠฅฬ‡ = encโ„• 0 payOf (โˆƒฬ‡ a) = โŒœ a โŒ payOf (โˆ€ฬ‡ a) = โŒœ a โŒ ``` The bounded quantifiers complete `payOf`, each pairing the code of its bounding term with the code of its body. Then `shape` records the bridge between the two directions: for every formula `ฯ†`, the code `โŒœ ฯ† โŒ` equals `mkTag (tagOf ฯ†) (payOf ฯ†)`. Since `tagOf` and `payOf` were transcribed from the clauses of `โŒœ_โŒ`, matching on `ฯ†` reduces both sides to the same tagged pair, and each case holds by `refl`. ```agda payOf (โˆ€ฬ‡โˆˆ t a) = pr โŒœ t โŒแต— โŒœ a โŒ payOf (โˆƒฬ‡โˆˆ t a) = pr โŒœ t โŒแต— โŒœ a โŒ shape : โˆ€ {n} (ฯ† : Formula S n) โ†’ โŒœ ฯ† โŒ โ‰ก mkTag (tagOf ฯ†) (payOf ฯ†) shape (t โˆˆฬ‡ u) = refl shape (t โ‰ u) = refl ``` The clauses shown here carry the same justification for disjunction, implication, falsity and the unbounded existential: in every case the equation is definitional, because `โŒœ_โŒ`, `tagOf` and `payOf` were built from the same recursion on the formula. The next block finishes the remaining constructors and then turns to the converse direction. ```agda shape (a โˆงฬ‡ b) = refl shape (a โˆจฬ‡ b) = refl shape (a โ‡’ฬ‡ b) = refl shape โŠฅฬ‡ = refl shape (โˆƒฬ‡ a) = refl ``` The last `shape` clauses close the bounded cases, and the construction now turns around: given a tag, describe what a formula with that tag looks like. The type family `Match` does this. For tag `k`, `Match k ฯ†` is the type of ways `ฯ†` can arise from a constructor of index `k`: one dependent-pair layer per subformula slot, ending in a path `ฯ† โ‰ก` the constructor applied to those slots. For tags `0` and `1` the slots are two terms, closing with the constructors `_โˆˆฬ‡_` and `_โ‰_`. ```agda shape (โˆ€ฬ‡ a) = refl shape (โˆ€ฬ‡โˆˆ t a) = refl shape (โˆƒฬ‡โˆˆ t a) = refl Match : โˆ€ {n} โ†’ โ„• โ†’ Formula S n โ†’ Type โ„“ Match {n} 0 ฯ† = ฮฃ[ t โˆˆ Term S n ] (ฮฃ[ u โˆˆ Term S n ] (ฯ† โ‰ก (t โˆˆฬ‡ u))) ``` Tags `2` through `4` repeat the pattern for the three binary connectives, each demanding two formulas of the same arity `n`. Tag `5` is the degenerate case: falsity has no slots, so `Match 5 ฯ†` is just the single path `ฯ† โ‰ก โŠฅฬ‡`, with no pair at all. This shows how the family adapts to the constructor's shape rather than imposing a uniform arity. ```agda Match {n} 1 ฯ† = ฮฃ[ t โˆˆ Term S n ] (ฮฃ[ u โˆˆ Term S n ] (ฯ† โ‰ก (t โ‰ u))) Match {n} 2 ฯ† = ฮฃ[ a โˆˆ Formula S n ] (ฮฃ[ b โˆˆ Formula S n ] (ฯ† โ‰ก (a โˆงฬ‡ b))) Match {n} 3 ฯ† = ฮฃ[ a โˆˆ Formula S n ] (ฮฃ[ b โˆˆ Formula S n ] (ฯ† โ‰ก (a โˆจฬ‡ b))) Match {n} 4 ฯ† = ฮฃ[ a โˆˆ Formula S n ] (ฮฃ[ b โˆˆ Formula S n ] (ฯ† โ‰ก (a โ‡’ฬ‡ b))) Match 5 ฯ† = ฯ† โ‰ก โŠฅฬ‡ ``` The quantifier tags carry the arity shift. For tags `6` and `7` the single slot is a formula of arity `suc n`; for tags `8` and `9` a term of arity `n` and a body of arity `suc n` fill the two slots, matching the constructors `โˆ€ฬ‡โˆˆ` and `โˆƒฬ‡โˆˆ`. Any other tag has no formulas to describe, so the family closes with the empty type `Empty.โŠฅ*`; `Match` is thereby defined for every natural-number tag. ```agda Match {n} 6 ฯ† = ฮฃ[ a โˆˆ Formula S (suc n) ] (ฯ† โ‰ก (โˆƒฬ‡ a)) Match {n} 7 ฯ† = ฮฃ[ a โˆˆ Formula S (suc n) ] (ฯ† โ‰ก (โˆ€ฬ‡ a)) Match {n} 8 ฯ† = ฮฃ[ t โˆˆ Term S n ] (ฮฃ[ a โˆˆ Formula S (suc n) ] (ฯ† โ‰ก โˆ€ฬ‡โˆˆ t a)) Match {n} 9 ฯ† = ฮฃ[ t โˆˆ Term S n ] (ฮฃ[ a โˆˆ Formula S (suc n) ] (ฯ† โ‰ก โˆƒฬ‡โˆˆ t a)) Match _ _ = Empty.โŠฅ* ``` The direction that computes witnesses is easy: `matches ฯ†` builds an inhabitant of `Match (tagOf ฯ†) ฯ†` by recursion on `ฯ†`. A binary formula `a โˆงฬ‡ b` supplies the two slots `a` and `b`, and the final path is `refl` because `a โˆงฬ‡ b` reassembles from its parts definitionally. For example, the witness for `t โˆˆฬ‡ u` is the triple `t , (u , refl)`. ```agda matches : โˆ€ {n} (ฯ† : Formula S n) โ†’ Match (tagOf ฯ†) ฯ† matches (t โˆˆฬ‡ u) = t , (u , refl) matches (t โ‰ u) = t , (u , refl) matches (a โˆงฬ‡ b) = a , (b , refl) matches (a โˆจฬ‡ b) = a , (b , refl) ``` The remaining constructors follow the shape of their `Match` rows: falsity contributes just `refl`, each unbounded quantifier pairs its body with `refl`, and each bounded quantifier supplies its bounding term and body. Once the last constructor is covered, `matches` shows that every formula matches its own tag, so the tag alone narrows any formula down to one constructor shape. ```agda matches (a โ‡’ฬ‡ b) = a , (b , refl) matches โŠฅฬ‡ = refl matches (โˆƒฬ‡ a) = a , refl matches (โˆ€ฬ‡ a) = a , refl matches (โˆ€ฬ‡โˆˆ t a) = t , (a , refl) ``` The theorem `โŒœโŒ-inj` is now within reach: for formulas `ฯ†` and `ฯˆ` of the same arity, an equality `โŒœ ฯ† โŒ โ‰ก โŒœ ฯˆ โŒ` should force `ฯ† โ‰ก ฯˆ`. The proof reduces to a helper `go`, stated inside a `private` block so only the theorem is exported. What `go` assumes is exactly what tag separation provides: `ฯˆ` re-presented as a match of `ฯ†`'s tag, and an equality of the payloads `payOf ฯ† โ‰ก payOf ฯˆ`. From these it must return `ฯ† โ‰ก ฯˆ`. ```agda matches (โˆƒฬ‡โˆˆ t a) = t , (a , refl) โŒœโŒ-inj : โˆ€ {n} (ฯ† ฯˆ : Formula S n) โ†’ โŒœ ฯ† โŒ โ‰ก โŒœ ฯˆ โŒ โ†’ ฯ† โ‰ก ฯˆ private go : โˆ€ {n} (ฯ† ฯˆ : Formula S n) โ†’ Match (tagOf ฯ†) ฯˆ โ†’ payOf ฯ† โ‰ก payOf ฯˆ โ†’ ฯ† โ‰ก ฯˆ go (t โˆˆฬ‡ u) ฯˆ (t' , (u' , q)) p = ``` The membership clause shows the whole mechanics, so it deserves a slow reading. The match presents `ฯˆ` as `t' โˆˆฬ‡ u'` up to a path `q : ฯˆ โ‰ก (t' โˆˆฬ‡ u')`, but the hypothesis `p` only equates the payloads of `ฯ†` and of `ฯˆ`, not of `t' โˆˆฬ‡ u'`. Composing `p` with `cong payOf q` transports the equation along `q`, producing `pr โŒœ t โŒแต— โŒœ u โŒแต— โ‰ก pr โŒœ t' โŒแต— โŒœ u' โŒแต—`, which `pr-inj` splits into equations of the term codes. Each goes through the already-proven `โŒœโŒแต—-inj`, `congโ‚‚ _โˆˆฬ‡_` rebuilds the constructor on both sides, and `sym q` retargets the right-hand side from `t' โˆˆฬ‡ u'` to `ฯˆ`. The equality clause repeats this word for word with `_โ‰_`. ```agda congโ‚‚ _โˆˆฬ‡_ (โŒœโŒแต—-inj t t' (pr-inj (p โˆ™ cong payOf q) .fst)) (โŒœโŒแต—-inj u u' (pr-inj (p โˆ™ cong payOf q) .snd)) โˆ™ sym q go (t โ‰ u) ฯˆ (t' , (u' , q)) p = congโ‚‚ _โ‰_ (โŒœโŒแต—-inj t t' (pr-inj (p โˆ™ cong payOf q) .fst)) (โŒœโŒแต—-inj u u' (pr-inj (p โˆ™ cong payOf q) .snd)) โˆ™ sym q ``` Every binary connective is handled by this one pattern, so the conjunction clause is worth stating as the general recipe. The match is a triple `a' , (b' , q)` with `q : ฯˆ โ‰ก (a' โˆงฬ‡ b')`. The transported payload equation has the shape `pr _ _ โ‰ก pr _ _`, so `pr-inj` yields equations of the two sub-codes, `โŒœโŒ-inj` lifts each recursively to an equality of subformulas, `congโ‚‚ _โˆงฬ‡_` rebuilds `a โˆงฬ‡ b โ‰ก a' โˆงฬ‡ b'`, and `sym q` points the right side at `ฯˆ`. This recipe is the whole content of the remaining connective clauses. ```agda go (a โˆงฬ‡ b) ฯˆ (a' , (b' , q)) p = congโ‚‚ _โˆงฬ‡_ (โŒœโŒ-inj a a' (pr-inj (p โˆ™ cong payOf q) .fst)) (โŒœโŒ-inj b b' (pr-inj (p โˆ™ cong payOf q) .snd)) โˆ™ sym q go (a โˆจฬ‡ b) ฯˆ (a' , (b' , q)) p = congโ‚‚ _โˆจฬ‡_ (โŒœโŒ-inj a a' (pr-inj (p โˆ™ cong payOf q) .fst)) ``` The disjunction and implication clauses instantiate the recipe with their own constructors, changing nothing else. Falsity is the only case with no payload work at all: the match is just `q : ฯˆ โ‰ก โŠฅฬ‡`, so `sym q : โŠฅฬ‡ โ‰ก ฯˆ` is already the required equation, and the payload hypothesis `p` goes unused. ```agda (โŒœโŒ-inj b b' (pr-inj (p โˆ™ cong payOf q) .snd)) โˆ™ sym q go (a โ‡’ฬ‡ b) ฯˆ (a' , (b' , q)) p = congโ‚‚ _โ‡’ฬ‡_ (โŒœโŒ-inj a a' (pr-inj (p โˆ™ cong payOf q) .fst)) (โŒœโŒ-inj b b' (pr-inj (p โˆ™ cong payOf q) .snd)) โˆ™ sym q go โŠฅฬ‡ ฯˆ q p = sym q ``` The unbounded quantifiers simplify the recipe: the payload is a single sub-code, so the transported equation is directly `โŒœ a โŒ โ‰ก โŒœ a' โŒ`, and one recursive call wrapped in `cong โˆƒฬ‡_` or `cong โˆ€ฬ‡_`, closed with `sym q`, suffices. The bounded quantifier `โˆ€ฬ‡โˆˆ` is where the two levels of coding meet in one constructor: after the `pr-inj` split, the term component is resolved by `โŒœโŒแต—-inj` and the formula component by the recursive `โŒœโŒ-inj`, and `congโ‚‚ โˆ€ฬ‡โˆˆ` reassembles both, with `sym q` finishing as always. ```agda go (โˆƒฬ‡ a) ฯˆ (a' , q) p = cong โˆƒฬ‡_ (โŒœโŒ-inj a a' (p โˆ™ cong payOf q)) โˆ™ sym q go (โˆ€ฬ‡ a) ฯˆ (a' , q) p = cong โˆ€ฬ‡_ (โŒœโŒ-inj a a' (p โˆ™ cong payOf q)) โˆ™ sym q go (โˆ€ฬ‡โˆˆ t a) ฯˆ (t' , (a' , q)) p = congโ‚‚ โˆ€ฬ‡โˆˆ (โŒœโŒแต—-inj t t' (pr-inj (p โˆ™ cong payOf q) .fst)) (โŒœโŒ-inj a a' (pr-inj (p โˆ™ cong payOf q) .snd)) โˆ™ sym q ``` The bounded existential mirrors the bounded universal, completing the ten cases. The top level then assembles the theorem. Given `e : โŒœ ฯ† โŒ โ‰ก โŒœ ฯˆ โŒ`, `go` needs a match of `ฯˆ` against the tag of `ฯ†`, but `matches ฯˆ` lives at the tag of `ฯˆ`. These may differ as numbers, so the match is transported: `tp .fst` is a path `tagOf ฯ† โ‰ก tagOf ฯˆ`, and `subst` along its symmetry re-indexes `matches ฯˆ` to the type `Match (tagOf ฯ†) ฯˆ`, which is exactly what `go` expects. ```agda go (โˆƒฬ‡โˆˆ t a) ฯˆ (t' , (a' , q)) p = congโ‚‚ โˆƒฬ‡โˆˆ (โŒœโŒแต—-inj t t' (pr-inj (p โˆ™ cong payOf q) .fst)) (โŒœโŒ-inj a a' (pr-inj (p โˆ™ cong payOf q) .snd)) โˆ™ sym q โŒœโŒ-inj ฯ† ฯˆ e = go ฯ† ฯˆ (subst (ฮป k โ†’ Match k ฯˆ) (sym (tp .fst)) (matches ฯˆ)) (tp .snd) ``` The local definition `tp` produces the pair of equations this transport needs. Chaining `sym (shape ฯ†)`, the hypothesis `e`, and `shape ฯˆ` rewrites the assumed equality of codes into an equality `mkTag (tagOf ฯ†) (payOf ฯ†) โ‰ก mkTag (tagOf ฯˆ) (payOf ฯˆ)` of tagged pairs, and `mkTag-inj` splits it into the tag equation and the payload equation. The tag equation drives the `subst`, the payload equation is `go`'s second argument, and the theorem is complete: no ten-by-ten comparison of constructors, only the tag arithmetic plus recursion on payloads. ```agda where tp = mkTag-inj (sym (shape ฯ†) โˆ™ e โˆ™ shape ฯˆ) ``` ## Recap Terms and formulas now have codes in `S`: `โŒœ_โŒ` attaches a constructor tag to the codes of the parts, while constants carry their underlying set as payload. The file records the constant and membership cases of relational coding, then proves that one code determines at most one formula of a fixed arity. The construction is generic in an injective pairing and an injection of the naturals.