Accessibility, Mendler iteration, and guarded observations

Accessibility

For $A:{\mathcal{U}}_i$, $R:A\to A\to {\mathcal{U}}_j$, and $a:A$, the selected accessibility family is governed in the fixed order

$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$$\mathrm{\Gamma }⊢R:A\to A\to {\mathcal{U}}_j$$\mathrm{\Gamma }⊢a:A$

$\mathrm{\Gamma }⊢{\mathsf{Acc}}_R(a):{\mathcal{U}}_{i\bigsqcup j}$

$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢h:\prod _{b:A}bRa\to {\mathsf{Acc}}_R(b)$

$\mathrm{\Gamma }⊢{\mathsf{acc}}_a(h):{\mathsf{Acc}}_R(a)$

For $P:\prod _{a:A}{\mathsf{Acc}}_R(a)\to {\mathcal{U}}_k$, abbreviate Elimination and computation are

$\mathrm{\Gamma }⊢P:\prod _{a:A}{\mathsf{Acc}}_R(a)\to {\mathcal{U}}_k$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢s:{\mathsf{Step}}_P$$\mathrm{\Gamma }⊢p:{\mathsf{Acc}}_R(a)$

$\mathrm{\Gamma }⊢{\mathsf{accind}}_P(s,a,p):P(a,p)$

Put $${\mathsf{accStep}}_P(s,a,h):=s(a,h,\lambda b.\lambda r.{\mathsf{accind}}_P(s,b,hbr)).$$

$\mathrm{\Gamma }⊢P:\prod _{a:A}{\mathsf{Acc}}_R(a)\to {\mathcal{U}}_k$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢s:{\mathsf{Step}}_P$$\mathrm{\Gamma }⊢h:H(a)$

${\mathsf{accind}}_P(s,a,{\mathsf{acc}}_a(h))\equiv {\mathsf{accStep}}_P(s,a,h):P(a,{\mathsf{acc}}_a(h))$

The proof-relevant strict order on naturals used by chapter 32 has constructors

$\mathrm{\Gamma }⊢n:\mathbb{N}$

The selected Mendler interface

For the fixed interface of chapter 84, the complete rule sequence is

$\mathrm{\Gamma }⊢F:{\mathcal{U}}_i\to {\mathcal{U}}_i$

$\mathrm{\Gamma }⊢{\mu }^{\mathsf{M}}F:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢u:F({\mu }^{\mathsf{M}}F)$

$\mathrm{\Gamma }⊢{\mathsf{in}}_F^{\mathsf{M}}(u):{\mu }^{\mathsf{M}}F$

$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$$\mathrm{\Gamma }⊢\varphi :\prod _{R:{\mathcal{U}}_i}(R\to A)\to F(R)\to A$

$\mathrm{\Gamma }⊢{\mathsf{mfold}}_F(\varphi ):{\mu }^{\mathsf{M}}F\to A$

$\mathrm{\Gamma }⊢\varphi :\prod _{R:{\mathcal{U}}_i}(R\to A)\to F(R)\to A$$\mathrm{\Gamma }⊢u:F({\mu }^{\mathsf{M}}F)$

${\mathsf{mfold}}_F(\varphi )({\mathsf{in}}_F^{\mathsf{M}}(u))\equiv \varphi ({\mu }^{\mathsf{M}}F,{\mathsf{mfold}}_F(\varphi ),u):A$

There is no destructor and no implicit $F$-action.

Guarded streams and bounded approximants

The complete stream fragment is

$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢\mathsf{Stream}(A):{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢s:\mathsf{Stream}(A)$

$\mathrm{\Gamma }⊢\mathsf{head}(s):A$

$\mathrm{\Gamma }⊢s:\mathsf{Stream}(A)$

$\mathrm{\Gamma }⊢\mathsf{tail}(s):\mathsf{Stream}(A)$

$\mathrm{\Gamma }⊢S:{\mathcal{U}}_j$$\mathrm{\Gamma }⊢h:S\to A$$\mathrm{\Gamma }⊢t:S\to S$$\mathrm{\Gamma }⊢x:S$

$\mathrm{\Gamma }⊢{\mathsf{corec}}_A(S,h,t,x):\mathsf{Stream}(A)$

Its computation equations are For the finite record schema, destructors $o_i:C\to O_i$ and $d_j:C\to C$ satisfy Every recursive occurrence is the complete result of a $d_j$ observation.

For $\alpha :\mathsf{Size}$, bounded approximants have

$\mathrm{\Gamma }⊢A:{\mathcal{U}}_j$$\mathrm{\Gamma }⊢\alpha :\mathsf{Size}$

$\mathrm{\Gamma }⊢{\mathsf{Stream}}^{\alpha }(A):{\mathcal{U}}_j$

$\mathrm{\Gamma }⊢s:{\mathsf{Stream}}^{\alpha }(A)$

$\mathrm{\Gamma }⊢{\mathsf{head}}^{\alpha }(s):A$

$\mathrm{\Gamma }⊢s:{\mathsf{Stream}}^{\alpha }(A)$

$\mathrm{\Gamma }⊢{\mathsf{tail}}^{\alpha ,\beta }(r,s):{\mathsf{Stream}}^{\beta }(A)$

Given the $S,h,t$ of definition 85.22,

$\mathrm{\Gamma }⊢x:S(\alpha )$

$\mathrm{\Gamma }⊢{\mathsf{corec}}_A^{\alpha }(S,h,t,x):{\mathsf{Stream}}^{\alpha }(A)$

Its head computes to $h(\alpha ,x)$; its tail at computes to ${\mathsf{corec}}_A^{\beta }(S,h,t,t(\alpha ,\beta ,r,x))$.