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

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.

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.

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

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

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.

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.

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

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

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