Scoped signatures and explicit substitution

The signature of chapter 23 is a pair $(\mathrm{\Sigma },\mathrm{\Gamma })$ of endofunctors on $\mathbf{Set}$. In polynomial form, $$\mathrm{\Sigma }X=\coprod _{o\in \mathcal{O}}{P}_o\times X^{R_o},\mathrm{\Gamma }X=\coprod _{s\in \mathcal{S}}{P}_s\times X^{Q_s}.$$ Its exact nested syntax is the initial solution of $$(\mathcal{G}H)A=A+\mathrm{\Sigma }(HA)+\mathrm{\Gamma }(H(HA)),T=\mu \mathcal{G},$$ with constructors $$\mathsf{Var}:A\to TA,\mathsf{Op}:\mathrm{\Sigma }(TA)\to TA,\mathsf{Scope}:\mathrm{\Gamma }(T(TA))\to TA.$$ For the elementwise recursion and induction rules below, Chapter 23 assumes that the transfinite initial chain of $\mathcal{G}$ is monic and converges to $T$; it does not claim a general existence theorem for arbitrary $(\mathrm{\Sigma },\mathrm{\Gamma })$.

For a polynomial scoped symbol $s$, the equivalent elementwise scope data are $$p:P_s,X:\mathbf{Set},m:Q_s\to TX,k:X\to TA,$$ written ${\mathsf{Scope}}_s(p;X;m;k)$, modulo $${\mathsf{Scope}}_s(p;X;m;k^{\prime }\circ h)={\mathsf{Scope}}_s(p;Y;\lambda q.Th(m(q));k^{\prime })(h:X\to Y).$$ The canonical nested representative is $$[X,m,k]⟼\lambda q.Tk(m(q)):Q_s\to T(TA),$$ and the inverse sends $u:Q_s\to T(TA)$ to $[TA,u,{\mathsf{id}}_{TA}]$.

For a reindexing-respecting predicate family ${\mathcal{P}}_A(t)$, the well-founded elementwise recursion and induction principle has constructor premises $$\begin{array}{l}{\mathcal{P}}_A(\mathsf{Var}(a)),\\ (\mathrm{\forall }r.{\mathcal{P}}_A(k(r)))⟹{\mathcal{P}}_A({\mathsf{Op}}_o(p,k)),\\ (\mathrm{\forall }q.{\mathcal{P}}_X(m(q)))\wedge (\mathrm{\forall }x.{\mathcal{P}}_A(k(x)))⟹{\mathcal{P}}_A({\mathsf{Scope}}_s(p;X;m;k)).\end{array}$$ It is obtained from the assumed monic convergent initial chain of $\mathcal{G}$; the scoped premises come from the two nested earlier-stage occurrences.

For $f:A\to TB$, explicit substitution is In nested form, if $b_f(u)=u[f]$, the scoped clause is $$\mathsf{Scope}(v)[f]=\mathsf{Scope}(\mathrm{\Gamma }(T{b}_f)(v)).$$ Return and bind are $$\mathsf{return}a=\mathsf{Var}(a),t\gg =f=t[f].$$ The proved equations are $$\mathsf{Var}(a)[f]=f(a),t[\mathsf{Var}]=t,t[f][g]=t[\lambda a.f(a)[g]].$$ They imply the three monad laws. No operational handler rules are part of the signature in chapter 23.