Modal and Multimodal Dependent Type Theory

Proof. Both by induction on the typing derivation. For weakening the only interesting case is Box-E: the conclusion is at $\mathrm{\Delta }.\mathsf{L}$ and the premise at $\mathrm{\Delta }$, and $\mathrm{\Gamma }\le \mathrm{\Delta }$ gives the premise by the induction hypothesis. For substitution the hypothesis that ${\mathrm{\Gamma }}^{\prime }$ is lock-free is used exactly once, in the variable case: if ${\mathrm{\Gamma }}^{\prime }$ contained a lock, $x$ would not be usable at the leaf and the substitution would be vacuous, but the statement of the lemma would then be about a different context. In the Box-I case the premise is at $(\mathrm{\Gamma },x:A,{\mathrm{\Gamma }}^{\prime }).\mathsf{L}$, where $x$ is unusable, so nothing is substituted and the induction hypothesis is applied trivially. ◻

Proof. Evaluation sends $x$ to the semantic value in the environment; the clause for $\mathsf{unbox}$ moves one lock inward and the clause for $\mathsf{box}$ moves one lock outward, so the composite is the identity on semantic values. Reification at $◻b$ emits $\mathsf{box}$ and recurses; at the base type it emits the accumulated neutral, which for the displayed term is the variable. Hence the normal form is $\lambda x.x$, which is the $\eta$-equation of definition 160.1 read as a computation. Existence of normal forms in general is the usual logical-relations argument for normalization by evaluation, carried out over contexts indexed by lock depth. ◻

Proof. Soundness. DBox-F is clause (2), DBox-I and DBox-E are the two directions of clause (3), and their two equations are that the bijection is a bijection. The substitution laws of definition 160.5 are exactly the naturality requirements of definition 160.6: without them the interpretation of a substituted modal type would depend on the order of the two operations. The remaining rules are theorem 54.28.

Term model and initiality. The syntactic CwF of theorem 54.27 acquires $\mathsf{L}$ from the context former, which is functorial because $\gamma .\mathsf{L}$ is defined by recursion and preserves identities and composites; $R$ from $◻$; and the bijection from $\mathsf{box}$ and $\mathsf{unbox}$, which are mutually inverse by the two equations. Naturality is the two substitution laws. Initiality is the argument of theorem 54.27 with two further clauses in the induction, one for each new former, each forced by the requirement that the interpretation be a morphism of CwDRAs. ◻

Proof. Induction on the derivation of $t$. The only case that consults the annotation is MTT-Var: there the premise supplies $\alpha :\mu \Rightarrow \mathrm{locks}({\mathrm{\Gamma }}^{\prime })$, and the proviso is exactly that such an $\alpha$ exists, so the substituted term is $u$ transported along the substitution induced by $\alpha$. In the lock case the context grows by ${\mathsf{L}}_{\nu }$ and $\mathrm{locks}$ grows by $\nu$, so the proviso is preserved by whiskering $\alpha$. In MTT-I the premise is one lock deeper and the induction hypothesis applies with the whiskered $2$-cell. Functoriality of the induced substitutions in $\alpha$ is what makes the two possible orders of transport agree. ◻

Proof. Glue along the global-sections functor, as in construction 151.30, but with the displayed model indexed by modes: a displayed context over $\mathrm{\Gamma }$ at mode $m$ is a predicate on the closing substitutions of $\mathrm{\Gamma }$, and the clause for a lock is $$R_{\mathrm{\Gamma }.{\mathsf{L}}_{\mu }}(\rho )\text{iff}{R}_{\mathrm{\Gamma }}({\rho }^{\prime })\text{for the closing substitution }{\rho }^{\prime }\text{ determined by }\rho ,$$ which is well defined because $\mathsf{L}$ is functorial in $\mathrm{\Gamma }$ and the lock equations of definition 160.11 are strict. The clause for $⟨\mu \mid A⟩$ is: $S_{⟨\mu \mid A⟩}(\rho ,t)$ holds iff $t$ is judgmentally equal to ${\mathsf{mod}}_{\mu }(t^{\prime })$ for some $t^{\prime }$ with $S_A$ holding at the locked context. Closure under MTT-I is immediate; closure under the modal $\mathsf{let}$ uses the $\beta$-rule together with the induction hypothesis at the locked context; and closure under MTT-Var uses the $2$-cell $\alpha$, whose induced substitution acts on the witnesses — here decidable equality of $2$-cells is what makes the predicate a well-defined function of the annotation rather than of a chosen representative. The rest of the displayed model is lemma 151.31. Initiality supplies a section as in theorem 151.32, and instantiating it at a closed term of $\mathbf{2}$ gives the disjunction. ◻

Proof. (1) Under the lock ${\mathsf{L}}_{▹}$ the declaration $a{:}_{\mathbf{1}}A$ is usable exactly when a $2$-cell $\mathbf{1}\Rightarrow ▹$ exists, which is $\mathsf{next}$; MTT-Var then applies.

(2) Take $\lambda f.\lambda u.\mathsf{let}{\mathsf{mod}}_{▹}(g)=f\mathsf{in}\mathsf{let}{\mathsf{mod}}_{▹}(a)=u\mathsf{in}{\mathsf{mod}}_{▹}(ga)$. Both eliminations introduce a declaration at modality $▹$, and inside the final ${\mathsf{mod}}_{▹}$ the composite of locks is $▹$, so both variables are usable by MTT-Var at the identity $2$-cell.

(3) The isomorphism is the pair of the two projections and the pairing; it is an isomorphism because $\times$ is the product and $▹$ is applied only to the second component, so no lock separates the two directions.

(4) A term of that type would, by MTT-Var applied under no lock, require a $2$-cell $▹\Rightarrow \mathbf{1}$ in ${\mathcal{M}}_{\mathsf{g}}$. By definition 160.15 the $2$-cells are generated by $\mathsf{next}$ in the direction $\mathbf{1}\Rightarrow ▹$ and closed under the two compositions, so every $2$-cell out of $▹$ has target a composite containing $▹$; none has target $\mathbf{1}$. Hence no such term exists. ◻