Synthetic Phase Distinctions and Synthetic Tait Computability

Prerequisites. Direct starred prerequisites: Chapter 57. No later core chapter depends on this route.

A dependent theory with Booleans and dependent products has a question attached to it that its rules do not answer: is every closed term of Boolean type judgmentally equal to one of the two constructors? Tait’s method answers such questions by defining, for each type, a predicate on terms of that type, and then proving that every term satisfies the predicate of its type. The definition is by recursion on the type, and that is where the difficulty lies in a dependent theory, because the type of the result of an application is computed from the argument.

This chapter carries out that argument once, in a metalanguage where the recursion, the contexts, and the naturality conditions are all performed by a single modality. The object to be built is a glue type: a type former that fastens a semantic predicate onto a syntactic type so tightly that the composite is judgmentally the syntactic type again in one phase, and is the predicate in the other. Every construction below exists to make that former available and to use it.

The object theory as a signature

Three features of this presentation are used throughout and are worth naming before any calculation. Binding is carried by the metalanguage: the second argument of $\mathsf{pi}$ is a function $\mathsf{tm}(A)\to \mathsf{tp}$, so there is no separate account of variables, capture, or substitution for the object theory. Typing is carried by indexing: $\mathsf{tm}$ is a family over $\mathsf{tp}$, so an ill-typed object term cannot be written down. Equality is carried by equations between constants, so the object theory’s judgmental equality is the least congruence generated by the four displayed equations.

The motive $C$ of $\mathsf{if}$ is an arbitrary function $\mathsf{tm}(\mathsf{bool})\to \mathsf{tp}$ of the metalanguage. This is what makes the eliminator dependent, and it is the exact feature that the next section will show to obstruct a recursion on type structure.

Example 161.2 verifies one instance by hand. A proof must cover every closed term at once, and every closed term arises by applying the constants of $\mathrm{\Sigma }$ to arguments that are themselves not closed: the body of a $\mathsf{lam}$ has a free variable, and the motive of an $\mathsf{if}$ is a function.

What the external computability predicate must carry

Tait’s construction assigns to each type a predicate on its terms. For the signature $\mathrm{\Sigma }$ the intended clauses are the following two, in which ${\mathrm{C}}_A$ denotes a predicate on closed terms of type $\mathsf{tm}(A)$: Clause (161.2) refers to ${\mathrm{C}}_{Ba}$. In definition 161.1 the second argument of $\mathsf{pi}$ is a function $B:\mathsf{tm}(A)\to \mathsf{tp}$, so $Ba$ is the value of a function at an argument. It is therefore not a subterm of $\mathsf{pi}AB$, and the pair of clauses is not a definition by structural recursion on the first index.

The failure is not repaired by choosing a different measure. Take $A:=\mathsf{bool}$ and let $B$ be any function $\mathsf{tm}(\mathsf{bool})\to \mathsf{tp}$ of the metalanguage. Nothing in $\mathrm{\Sigma }$ constrains the values of $B$ beyond their type, so the family of types $\{Ba\}$ appearing in clause (161.2) is not generated by a smaller instance of the same grammar. In this presentation $\mathsf{tp}$ is a constant of the signature and carries no induction principle at all: there is no case analysis on a type, and hence no recursion on one.

A second obligation appears as soon as open terms are admitted, and they must be admitted, because clause (161.2) is used to type the body of a $\mathsf{lam}$. Indexing the predicate by a context $\mathrm{\Delta }$ turns each clause into a family ${\mathrm{C}}_A^{\mathrm{\Delta }}$, and each family must be stable under renaming: for every renaming $\rho$ from ${\mathrm{\Delta }}^{\prime }$ to $\mathrm{\Delta }$, $${\mathrm{C}}_A^{\mathrm{\Delta }}(a)\text{ implies }{\mathrm{C}}_{A[\rho ]}^{{\mathrm{\Delta }}^{\prime }}(a[\rho ]).$$ Obligation (161.3) is discharged separately for every clause of the definition, and again for every lemma proved about the clauses. It is bookkeeping in the exact sense that it never selects between two mathematical possibilities; it only records that a construction was uniform in the context.

Both obligations are removed by the same change of ambient setting. Work in a category whose objects already are context-indexed families and whose maps already are the natural ones, so that (161.3) holds by construction; and describe the predicate not by recursion on syntax but as a type in the internal language of that category, so that the missing recursion in (161.2) is never attempted. The rest of the chapter constructs that category and that internal language.

The gluing category and its two phases

Contexts of the object theory index the presheaves, and a map of presheaves is a family of functions commuting with reindexing. Obligation (161.3) is the commutation requirement, and it is part of what it means to be a map in $[{\mathcal{T}}^{\mathrm{op}},\mathbf{Set}]$.

An object $(S,\mathrm{y}(B),f)$ is to be read as a proof-relevant predicate on the closed terms of type $B$: the set $S$ is the collection of witnesses and $f$ records, for each witness, the term it is a witness for. The set $S_b:=f^{-1}(b)$ is the set of witnesses at the closed term $b$.

Example 161.7 already contains the shape of the canonicity argument: if every closed term $b$ receives such a map, canonicity follows. The work is to produce those maps uniformly, and that is done by interpreting the whole signature in $\mathcal{G}$ so that the interpretation of a term is a map whose presheaf component is that very term.

The condition “$\pi$ of the semantic object is the syntactic object” is a strict equation between objects, not an isomorphism. Keeping it strict is the single hardest requirement in the construction, and section 161.5 is devoted to the axiom that makes it available.

The synthetic phase distinction

The internal language of $\mathcal{G}$ is a dependent type theory with extensional equality types, dependent sums and products, coproducts, quotients, and a hierarchy of universes. All constructions below are written in that language; what makes them into gluing constructions is one additional constant.

The three constructors say exactly this: $\bullet A$ contains a copy of $A$, it contains a point supplied by the syntactic phase, and under the syntactic phase these two are identified. The third clause is the whole content of the definition and is used in every proof below.

Proof of Lemma 161.11 — The modalities are idempotent monads

Proof. For $\mathrm{\#}$: the action on maps is $\mathrm{\#}g:=\lambda u.\lambda z.g(uz)$, and the double application unfolds to $\mathrm{\#}\mathrm{\#}A=\mathsf{syn}\to \mathsf{syn}\to A$. Define $\mu :=\lambda w.\lambda z.wzz$. The two round trips are $$\mu ({\eta }_{\mathrm{\#}}u)\stackrel{def.}{=}\lambda z.uz\stackrel{funext}{=}u,{\eta }_{\mathrm{\#}}(\mu w)\stackrel{def.}{=}\lambda z.\lambda z^{\prime }.wzz\stackrel{z=z^{\prime }}{=}w,$$ the second because $\mathsf{syn}$ is a proposition, so its two proofs $z$ and $z^{\prime }$ are equal. The monad laws are the corresponding two calculations.

For $\bullet$: the functorial action is defined on constructors by $\bullet g(\eta a):=\eta (ga)$ and $\bullet g(\star z):=\star z$, which respects $\mathrm{law}$ because both sides are identified under $\mathsf{syn}$. For idempotence, define $\nu :\bullet \bullet A\to \bullet A$ by $\nu (\eta x):=x$ and $\nu (\star z):=\star z$; this respects $\mathrm{law}$ because $\mathrm{law}xz$ maps to $x=\star z$, which is an instance of $\mathrm{law}$ in $\bullet A$ when $x=\eta a$ and is $\mathrm{law}$-reflexivity when $x=\star z^{\prime }$, using that $\mathsf{syn}$ is a proposition. Then $\nu \circ \eta =\mathrm{id}$ by the first clause, and $\eta \circ \nu =\mathrm{id}$ by the eliminator’s uniqueness clause on the two constructors. ◻

Proof of Lemma 161.13 — Closed-modality criterion

Proof. Suppose $\mathrm{\#}B$ is contractible with centre $c$. Define $r:\bullet B\to B$ by $r(\eta b):=b$ and $r(\star z):=cz$; the clause for $\mathrm{law}$ requires $b=cz$ for $z:\mathsf{syn}$, and under $z$ the two elements ${\eta }_{\mathrm{\#}}b$ and $c$ of $\mathrm{\#}B$ are equal by contractibility, so their values at $z$ agree. Then $r\circ \eta =\mathrm{id}$ by the first clause and $\eta \circ r=\mathrm{id}$ by the eliminator’s uniqueness clause.

Conversely, suppose $\eta$ is an isomorphism with inverse $r$. Under $z:\mathsf{syn}$ every element of $\bullet B$ equals $\star z$ by $\mathrm{law}$, so $\bullet B$ is contractible under $z$; transporting along the isomorphism, $B$ is contractible under $z$, which is the statement that $\mathrm{\#}B$ is contractible. ◻

Proof of Lemma 161.15 — Computation of the modalities in G

Proof. The open modality is the exponential $\mathsf{syn}\to (-)$ in $\mathcal{G}$. In a comma category over a limit-preserving functor, the exponential by a subterminal object with empty set component has set component $\mathrm{pt}(X)$: a map $(S^{\prime },X^{\prime },f^{\prime })\to \mathrm{\#}T$ is a map $(S^{\prime },X^{\prime },f^{\prime })\times \mathsf{syn}\to T$, and $(S^{\prime },X^{\prime },f^{\prime })\times \mathsf{syn}=(\mathrm{\varnothing },X^{\prime },!)$, so such a map is just a presheaf map $X^{\prime }\to X$; that is exactly a map into $(\mathrm{pt}(X),X,\mathrm{id})$. Its unit is the identity on presheaves and $f$ on sets.

For the closed modality, $\bullet T$ is the pushout of the two projections of $\mathsf{syn}\times T=(\mathrm{\varnothing },X,!)$. Colimits in $\mathcal{G}$ are computed by taking the colimit of the set components and the colimit of the presheaf components and inducing the structure map, so the set component is the pushout of $\mathrm{\varnothing }\leftarrow \mathrm{\varnothing }\to S$, namely $S$, and the presheaf component is the pushout of $\mathrm{y}(1_{\mathcal{T}})\leftarrow X\to \mathrm{y}(1_{\mathcal{T}})$ along the two terminal maps, namely $\mathrm{y}(1_{\mathcal{T}})$. The structure map is the unique one into $\mathrm{pt}(\mathrm{y}(1_{\mathcal{T}}))=1$. ◻

Proof of Theorem 161.16 — Fracture

Proof. Commutation is the naturality of $\eta$ at ${\eta }_{\mathrm{\#}}$. For the pullback property, compute both sides in $\mathcal{G}$ using lemma 161.15 at $T=(S,X,f)$: $$\mathrm{\#}T=(\mathrm{pt}(X),X,\mathrm{id}),\bullet T=(S,\mathrm{y}(1_{\mathcal{T}}),!),\bullet \mathrm{\#}T=(\mathrm{pt}(X),\mathrm{y}(1_{\mathcal{T}}),!).$$ The map $\eta :\mathrm{\#}T\to \bullet \mathrm{\#}T$ has set component the identity on $\mathrm{pt}(X)$, and the map $\bullet {\eta }_{\mathrm{\#}}:\bullet T\to \bullet \mathrm{\#}T$ has set component $f:S⟶\mathrm{pt}(X)$, because $\bullet$ leaves set components unchanged and ${\eta }_{\mathrm{\#}}$ has set component $f$. Limits in $\mathcal{G}$ are computed componentwise, since $\mathrm{pt}$ preserves them. The set component of the pullback is therefore $\mathrm{pt}(X){\times }_{\mathrm{pt}(X)}S=S$ along $(\mathrm{id},f)$, and the presheaf component is $X{\times }_{\mathrm{y}(1_{\mathcal{T}})}\mathrm{y}(1_{\mathcal{T}})=X$. The induced structure map is $f$. Hence the pullback is $(S,X,f)=T$, and the comparison map is the identity. ◻

The fracture theorem is the exact sense in which nothing is lost by working with the two modalities instead of with the triples: a type is determined by its syntactic part, its semantic part, and the way the second sits over the first. Every definition in section 161.7 is given by specifying those three data.

Partial elements, extents, and realignment

For $\phi :=\mathsf{syn}$ the extent type is the internal form of the strictness condition of definition 161.8: an element of $\{A\mid \mathsf{syn}\hookrightarrow a\}$ is a semantic object that is, under the syntactic phase, the prescribed syntactic object.

Proof of Lemma 161.18 — Extents are closed-modal

Proof. By lemma 161.13 it suffices to show that $\mathrm{\#}\{A\mid \mathsf{syn}\hookrightarrow a\}$ is contractible. Assume $z:\mathsf{syn}$. Then every element $a^{\prime }$ of the extent type satisfies $a^{\prime }=az$ by definition 161.17, so the type has the element $az$ and all its elements are equal to $az$. Hence under $\mathsf{syn}$ it is contractible, which is the required statement. ◻

The strictness required in definition 161.8 does not follow from the constructions so far. Given a syntactic type $A$ and a semantic predicate on it, dependent sums produce a type that is isomorphic to $A$ under $\mathsf{syn}$, not equal to it. The next definition is the axiom that converts such an isomorphism into an equation.

Read the type in definition 161.19 as an instruction: given a type $A$, a proposition $\phi$, and a partially defined isomorph $B$ of $A$ available under $\phi$, produce a single isomorph $A_0$ of $A$ that is equal to $B$ wherever $B$ is defined. The conclusion is an equality of elements of $\mathrm{Iso}(A)$, so both the type and its isomorphism are pinned down.

Proof of Lemma 161.22 — Open and closed subuniverses

Proof. Both displayed expressions are instances of convention 161.20, so the two equations under $\mathsf{syn}$ hold by the defining equation of $\mathrm{realign}$. For the characterization of elements: an element of $\{\mathsf{syn}\}\mathcal{U}$ is a type defined only under $\mathsf{syn}$, and composing with the realignment isomorphism sends $A:\mathcal{U}$ to $\lambda z.A$, whose image is open-modal because $\mathrm{\#}A=\mathsf{syn}\to A$ and the unit is inverted by evaluation; conversely an open-modal $A$ equals $\mathrm{\#}A$, which is in the image. For the closed subuniverse, an element of $\{\mathcal{U}\mid \mathsf{syn}\hookrightarrow \mathbf{1}\}$ is a type equal to $\mathbf{1}$ under $\mathsf{syn}$, and by lemma 161.13 that is exactly the condition to be closed-modal. ◻

Strict glue types

Realignment is a statement about universes. The construction it is used for is always the same, and it is worth isolating as a type former so that it need not be re-derived at each constant of the signature.

The two rules Glue-Syn and Glue-Elt-Syn are the reason for the whole construction: under the syntactic phase the glue type collapses to its syntactic component and a glued element collapses to its syntactic part. In the notation of definition 161.17 these say $$\mathrm{\#}((x:A)⋉B(x)=A)\text{and}\mathrm{\#}([\mathsf{syn}\hookrightarrow a\mid b]=a).$$

Proof of Proposition 161.24 — Glue types from realignment

Proof. The only step needing an argument is the existence of $\iota$; the rest is the reading of convention 161.20.

Assume $z:\mathsf{syn}$. Then $(z^{\prime }:\mathsf{syn})\to A{z}^{\prime }$ is isomorphic to $Az$ by evaluation at $z$, with inverse $\lambda a.\lambda z^{\prime }.a$; these are mutually inverse because $\mathsf{syn}$ is a proposition, so $z^{\prime }=z$ and the two round trips are the identity. For the second component, the hypothesis of Glue-F gives $\mathrm{\#}B(x)\cong \mathbf{1}$, and evaluating that isomorphism at $z$ shows that $B(x)$ is contractible; hence the projection $\mathrm{\Sigma }\to (z^{\prime }:\mathsf{syn})\to A{z}^{\prime }$ is an isomorphism under $z$. Composing the two gives $\iota :\mathrm{\Sigma }\cong Az$.

Now convention 161.20 supplies a type equal to $Az$ under $\mathsf{syn}$ and isomorphic to $\mathrm{\Sigma }$; that equation is Glue-Syn. Transporting the introduction, projections, computation, and uniqueness rules of $\mathrm{\Sigma }$ across the realignment isomorphism gives Glue-I, Glue-E, Glue-C, and Glue-U. Finally, under $z:\mathsf{syn}$ the isomorphism $\iota$ sends a pair to the evaluation of its first component, so $({\pi }_{\circ }g)z=g$, which is Glue-Elt-Syn. ◻

Proof of Lemma 161.25 — Interpretation of the glue type in G

Proof. By proposition 161.24 the glue type is a realignment of $\mathrm{\Sigma }$, and realignment changes an object only within its isomorphism class, so it suffices to compute $\mathrm{\Sigma }$. A closed-modal family has presheaf component $\mathrm{y}(1_{\mathcal{T}})$ at each index by lemma 161.15, so the dependent sum has presheaf component $X$ and set component the disjoint union of the fibres, with the first projection as structure map. ◻

The canonicity model

The interpretation is now written as a list of definitions, one per constant of $\mathrm{\Sigma }$. Each carries an extent type recording which syntactic constant it must restrict to under $\mathsf{syn}$; that extent condition is the internal form of definition 161.8. Constants of the signature are written in lower case and their semantic counterparts in capitals.

Read $\mathsf{TP}$ as follows: a semantic type is a syntactic type together with a semantic collection of its terms, and that collection must restrict to the syntactic term collection under $\mathsf{syn}$. Three checks make the definition well formed, and each uses one rule of definition 161.23.

1. The semantic component $\{\mathcal{U}\mid \mathsf{syn}\hookrightarrow \mathsf{tm}(A)\}$ is closed-modal by lemma 161.18, so Glue-F applies.

2. The extent condition $\mathrm{\#}(\mathsf{TP}=\mathsf{tp})$ holds by Glue-Syn.

3. The definition of $\mathsf{TM}$ is well typed because ${\pi }_{\bullet }A$ inhabits the semantic component of $\mathsf{TP}$ by Glue-E, and the extent condition $\mathrm{\#}(\mathsf{TM}=\mathsf{tm})$ holds because that component is an extent type over $\mathsf{tm}(A)$ and $\mathrm{\#}(A={\pi }_{\circ }A)$ by Glue-Elt-Syn.

The inner glue type in $\mathsf{BOOL}$ is the semantic component supplied to the outer one. Its syntactic part is $\mathsf{tm}(\mathsf{bool})$ and its semantic part is the closed modality applied to the disjunction that names a constructor. Three conditions must hold, and the third is the reason the closed modality appears.

1. $\mathrm{\#}(\mathsf{BOOL}=\mathsf{bool})$, which is Glue-Elt-Syn for the outer glue type.

2. The semantic component of $\mathsf{BOOL}$ restricts to $\mathsf{tm}(\mathsf{bool})$ under $\mathsf{syn}$, as construction 161.26 demands. This is Glue-Syn for the inner glue type.

3. The family $b\mapsto \bullet ((b=\mathsf{true})+(b=\mathsf{false}))$ takes closed-modal values, so that Glue-F applies to the inner glue type. This holds by lemma 161.11, since every type of the form $\bullet C$ is closed-modal.

Proof of Proposition 161.30 — The eliminator is well defined

Proof. By definition 161.10 the eliminator of $\bullet C$ requires, for each $c:C$ and each $z:\mathsf{syn}$, that the value at $\eta c$ equal the value at $\star z$.

First branch. Take $c=\mathsf{inl}(p)$ with $p:b=\mathsf{true}$. Under $z:\mathsf{syn}$ the equality $p$ holds, so $b=\mathsf{true}$, and by equality reflection this is a judgmental equality. Therefore $$\mathsf{if}Cbtf\stackrel{p}{=}\mathsf{if}C\mathsf{true}tf\stackrel{\mathsf{if}{\beta }_1}{=}t,$$ which is the value assigned at $\eta (\mathsf{inl}(p))$.

Second branch. As in the first branch, with $\mathsf{inr}$ for $\mathsf{inl}$, $\mathsf{false}$ for $\mathsf{true}$, $\mathsf{if}{\beta }_2$ for $\mathsf{if}{\beta }_1$, and $f$ for $t$.

Extent condition. Under $\mathsf{syn}$ the element ${\pi }_{\bullet }b$ equals $\star z$ by $\mathrm{law}$, so the third branch is selected and $\mathsf{IF}Cbtf=\mathsf{if}Cbtf$, using Glue-Elt-Syn to identify $C$, $b$, $t$, $f$ with their syntactic parts. ◻

Proof of Proposition 161.32 — The product clauses are well typed

Proof. Formation. The semantic component of $\mathsf{PI}AB$ is an extent type, hence closed-modal by lemma 161.18, so Glue-F applies to the inner glue type. Its Glue-Syn equation gives $\mathrm{\#}(\mathsf{PI}AB=\mathsf{pi}AB)$, which is the extent condition on $\mathsf{PI}$.

Introduction. For $\mathsf{LAM}f$ to be an application of Glue-I to the inner glue type, the second component $f$ must inhabit $$\{(a:\mathsf{TM}(A))\to \mathsf{TM}(Ba)\mid \mathsf{syn}\hookrightarrow \mathsf{app}(\mathsf{lam}f)\},$$ that is, $f$ must equal $\mathsf{app}(\mathsf{lam}f)$ under $\mathsf{syn}$. Under $z:\mathsf{syn}$ we compute, for every $a$, $$\mathsf{app}(\mathsf{lam}f)a\stackrel{\mathsf{pi}\beta }{=}fa,$$ and function extensionality gives $\mathsf{app}(\mathsf{lam}f)=f$. The equation $\mathsf{pi}\beta$ of definition 161.1 is used exactly here, and by equality reflection it is available as a judgmental equality during type checking.

Elimination. ${\pi }_{\bullet }e$ inhabits the extent type displayed above by Glue-E, hence is a function $(a:\mathsf{TM}(A))\to \mathsf{TM}(Ba)$; applying it to $a$ gives the required type. Under $\mathsf{syn}$ it equals $\mathsf{app}e$ by the extent condition, which is the extent condition on $\mathsf{APP}$.

Computation. $$\mathsf{APP}(\mathsf{LAM}f)a\stackrel{Glue-C}{=}({\pi }_{\bullet }[\mathsf{syn}\hookrightarrow \mathsf{lam}f\mid f])a\stackrel{Glue-C}{=}fa.$$

Uniqueness. $$\mathsf{LAM}(\mathsf{APP}e)\stackrel{def.}{=}[\mathsf{syn}\hookrightarrow \mathsf{lam}(\mathsf{app}e)\mid {\pi }_{\bullet }e]\stackrel{\mathsf{pi}\eta }{=}[\mathsf{syn}\hookrightarrow {\pi }_{\circ }e\mid {\pi }_{\bullet }e]\stackrel{Glue-U}{=}e,$$ where the middle step uses $\mathsf{pi}\eta$ together with $\mathrm{\#}(e={\pi }_{\circ }e)$ from Glue-Elt-Syn. ◻

From the internal model to closed terms

The constructions of section 161.7 are definitions in the internal language of $\mathcal{G}$. Canonicity is a statement about closed terms of $\mathcal{T}$. One step joins the two, and it is the step named in remark 161.4: the recursion that builds $\mathcal{T}$ out of $\mathrm{\Sigma }$.

The statement imported is the categorical fundamental theorem of logical relations for Artin gluing, in the form used by Li, Yao and Harper, Mechanizing Synthetic Tait Computability in Istari, §1.1, together with the adequacy of the logical-framework presentation of a type theory by a free locally cartesian closed category, due to Gratzer and Sterling [LH26, Ste21]. What it supplies here is the single passage from internal definitions to closed terms. Everything else in this chapter is proved locally: the modal lemmas lemma 161.11, lemma 161.13, the fracture theorem theorem 161.16, the computation of the modalities and of the glue type inside $\mathcal{G}$ lemma 161.15, lemma 161.25, the derivation of the glue rules from realignment proposition 161.24, the well-typing of every clause of construction 161.26–construction 161.31, and the extraction below.

Proof of Theorem 161.34 — Canonicity

Proof. Let $\iota$ be the functor of theorem 161.33 for the interpretation of construction 161.26–construction 161.31.

The interpreted Boolean type. By construction 161.27 the semantic component of $\mathsf{BOOL}$ is the glue type $(c:\mathsf{tm}(\mathsf{bool}))⋉\bullet ((c=\mathsf{true})+(c=\mathsf{false}))$. Its base is open-modal, and $\bullet$ leaves set components unchanged by lemma 161.15, so lemma 161.25 computes the interpretation of $\mathsf{BOOL}$ in $\mathcal{G}$ as $$(\coprod _{c\in \mathrm{pt}(\mathrm{y}(\mathsf{bool}))}{S}_c,\mathrm{y}(\mathsf{bool}),{\mathsf{pr}}_1),S_c:=(c=\mathsf{true})+(c=\mathsf{false}),$$ where $\mathrm{pt}(\mathrm{y}(\mathsf{bool}))$ is the set $\mathrm{Nat}(\mathrm{y}(1_{\mathcal{T}}),\mathrm{y}(\mathsf{bool}))$ of closed terms of type $\mathsf{tm}(\mathsf{bool})$ modulo the equations of $\mathrm{\Sigma }$, by definition 161.5. Thus $S_c$ has an element exactly when $c=\mathsf{true}$ or $c=\mathsf{false}$.

Extraction. Apply $\iota$ to the global element $b:1_{\mathcal{T}}\to \mathsf{bool}$. The result is a map $\iota (b):1_{\mathcal{G}}\to \iota (\mathsf{bool})$ in $\mathcal{G}$; write it as a pair $(h,t)$ as in definition 161.6. The set component $h:1⟶\coprod _c{S}_c$ selects an element of $S_{c_0}$ for exactly one index $c_0$. The commutation condition of definition 161.6 applied to $(h,t)$ gives $$c_0\stackrel{{\mathsf{pr}}_1\circ h}{=}\mathrm{pt}(t)\stackrel{theorem161.33}{=}b.$$ Hence $S_b$ has an element, so $b=\mathsf{true}$ or $b=\mathsf{false}$. ◻

What this proof does and does not establish

Theorem 161.34 is a canonicity theorem for the signature $\mathrm{\Sigma }$. Four nearby statements are not consequences of it, and each fails for a different reason.

Normalization. Canonicity concerns closed terms of one base type. Normalization concerns open terms of every type and requires an interpretation in which types carry normal and neutral forms, not merely a predicate on closed terms. A normalization theorem proved by the method of this chapter, at a signature that includes modalities, is available: Gratzer, Normalization for multimodal type theory, proves in Theorem 6.4 that there is a function ${\mathrm{nf}}_{\mathrm{\Gamma }}(-,A)$ from terms to normal forms with $\mathrm{\Gamma }⊢|{\mathrm{nf}}_{\mathrm{\Gamma }}(M,A)|=M:A$ and with $\mathrm{\Gamma }⊢M=N:A$ implying ${\mathrm{nf}}_{\mathrm{\Gamma }}(M,A)={\mathrm{nf}}_{\mathrm{\Gamma }}(N,A)$; Corollary 6.6 derives decidability of conversion from decidability of the mode theory, and Corollary 6.11 recovers Boolean canonicity. That theorem is stated for multimodal type theory at its own signature, and is not proved here.

Other phase distinctions. The proposition $\mathsf{syn}$ of definition 161.10 separates syntax from semantics. It is not the strict/fibrant distinction of two-level type theory, whose two layers are two notions of equality on the same terms; it is not a parameter/state distinction, whose two layers are two run-times; it is not an erasure annotation, whose content is a usage discipline on variables; and it is not a stage separation, whose content is a temporal order on evaluation. What distinguishes $\mathsf{syn}$ from all four is that it is an ordinary proposition of the ambient theory, so that the two “layers” are the two subtopoi it cuts out, and the fracture theorem theorem 161.16 reassembles them.

Mechanization. Li, Yao and Harper check the constructions of construction 161.26–construction 161.31 in Istari, an extensional proof assistant with equality reflection; their development also treats a cost-aware framework. A successful check establishes the archived theories at their recorded signatures. It does not establish theorem 161.33, which is the step performed outside the internal language, and it is not a verified kernel.

Arbitrary signatures. Nothing above depends on the particular constants of $\mathrm{\Sigma }$ except construction 161.27–construction 161.31. Section 161.4–Section 161.6 are stated for an arbitrary proposition and an arbitrary strong universe. But a new type former requires a new semantic clause and a new verification of the three conditions, and a former whose semantic component cannot be made closed-modal has no clause of this shape at all. Exercise 161.4 is the smallest instance of that failure.