Representing Continuous Functions between Greatest Fixed Points of Indexed Containers

TL;DR

This paper introduces a method to represent computable functions between coinductive types as transducers within type theory, extending previous work on streams to more complex coinductive structures, and formalizes these in Agda.

Contribution

It generalizes earlier models of functions between streams to a broader class of coinductive types using dependent type theory and inductive-recursive definitions.

Findings

Transducers can be defined without equality notions in dependent type theory.

Most properties rely on a mild notion of equality, enabling formalization in Agda.

The approach applies to a richer class of coinductive types beyond streams.

Abstract

We describe a way to represent computable functions between coinductive types as particular transducers in type theory. This generalizes earlier work on functions between streams by P. Hancock to a much richer class of coinductive types. Those transducers can be defined in dependent type theory without any notion of equality but require inductive-recursive definitions. Most of the properties of these constructions only rely on a mild notion of equality (intensional equality) and can thus be formalized in the dependently typed language Agda.

Equations

$$\forall s\in \mathtt{stream}(X),\forall k\ge 0,\exists n\ge 0,\forall t\in \mathtt{stream}(X),s_{\upharpoonright n}=t_{\upharpoonright n}\Rightarrow f(s{)}_k=f(t{)}_k.$$

$$\forall s\in V,\exists n\ge 0,\forall t\in \mathtt{stream}(X),s_{\upharpoonright n}=t_{\upharpoonright n}\Rightarrow t\in V.$$

$$\forall s\in f^{-1}(V_{k,y})\exists n\ge 0,\forall t\in \mathtt{stream}(X),s_{\upharpoonright n}=t_{\upharpoonright n}\Rightarrow t\in f^{-1}(V_{k,y}).$$

$${\mathtt{tree}}_{\mathbb{B}}(X)=X\times (\mathbb{B}\to X)\times ({\mathbb{B}}^2\to X)\times \cdots \times ({\mathbb{B}}^i\to X)\times \dots$$

$$\mathtt{tree}_{\mathbb{B}}(X)\quad=\quad\prod_{i\geq 0}\big{(}\mathbb{B}^{i}\to X\big{)}\quad=\quad\prod_{i\geq 0}\left(\prod_{t\in\mathbb{B}^{i}}X\right)\,.$$

$${\mathtt{tree}}_B(X)=\prod _{i\ge 0}\left(\prod _{t\in B^i}X\right),$$

$$\forall t\in {\mathtt{tree}}_A(X),\forall k\ge 0,\exists n\ge 0,\forall t^{\prime }\in {\mathtt{tree}}_A(X),t_{\upharpoonright k}=t_{\upharpoonright k}^{\prime }\Rightarrow f(t{)}_n=f(t^{\prime }{)}_n,$$

$$\mathsf{Pow}(A)=A\to \mathsf{Set}.$$

$$R^{\sim }(b,a)=R(a,b).$$

$$\mathsf{Fam}(C)\quad=\quad\left(\big{.}\Sigma\,I:\mathsf{Set}\right)\,{}I\to C\,.$$

$${\mathtt{T}}_1=\text{leavevmode}to37.9pt\text{vbox}to36.17pt\text{pgfpicture}\text{makeatletter}\text{lower}-32.31354ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.0-1.38889pt-0.52777pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}.\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.0-15.61526pt-28.98053pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}.\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@moveto}-2.02982pt-4.06078pt\text{pgfsys@lineto}-12.1963pt-24.39198pt\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@rect}-10.86305pt-18.33748pt7.5pt8.2222pt\text{pgfsys@fill}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.0-8.36305pt-15.83748pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}1\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.012.8375pt-28.98053pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}.\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@moveto}2.02982pt-4.06078pt\text{pgfsys@lineto}12.1963pt-24.39198pt\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@rect}3.36305pt-18.33748pt7.5pt8.2222pt\text{pgfsys@fill}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.05.86305pt-15.83748pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}2\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}{\mathtt{T}}_2=\text{leavevmode}to123.25pt\text{vbox}to64.63pt\text{pgfpicture}\text{makeatletter}\text{lower}-60.7663ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.0-1.38889pt-0.52777pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}.\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.0-44.06802pt-28.98053pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}.\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@moveto}-4.92189pt-3.28pt\text{pgfsys@lineto}-37.75725pt-25.17276pt\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.0-58.2944pt-57.43329pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}.\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@moveto}-44.70895pt-32.51353pt\text{pgfsys@lineto}-54.87544pt-52.84474pt\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@rect}-53.54219pt-46.79024pt7.5pt8.2222pt\text{pgfsys@fill}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.0-51.04219pt-44.29024pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}3\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.0-29.84164pt-57.43329pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}.\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@moveto}-40.64932pt-32.51353pt\text{pgfsys@lineto}-30.48283pt-52.84474pt\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@rect}-39.31609pt-46.79024pt7.5pt8.2222pt\text{pgfsys@fill}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.0-36.81609pt-44.29024pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}4\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@rect}-25.08957pt-18.33748pt7.5pt8.2222pt\text{pgfsys@fill}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.0-22.58957pt-15.83748pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}1\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.041.29025pt-28.98053pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}.\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@moveto}4.92189pt-3.28pt\text{pgfsys@lineto}37.75725pt-25.17276pt\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.027.06387pt-57.43329pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}.\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@moveto}40.64932pt-32.51353pt\text{pgfsys@lineto}30.48283pt-52.84474pt\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@rect}31.81609pt-46.79024pt7.5pt8.2222pt\text{pgfsys@fill}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.034.31609pt-44.29024pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}5\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.055.51663pt-57.43329pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}.\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@moveto}44.70895pt-32.51353pt\text{pgfsys@lineto}54.87544pt-52.84474pt\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@rect}46.04219pt-46.79024pt7.5pt8.2222pt\text{pgfsys@fill}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.048.54219pt-44.29024pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}6\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}[named]pgffillcolorrgb\mathrm{1,1,1}\text{pgfsys@color@gray@fill}1\text{pgfsys@invoke}\text{pgfsys@rect}17.58957pt-18.33748pt7.5pt8.2222pt\text{pgfsys@fill}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@transformcm}1.00.00.01.020.08957pt-15.83748pt\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}2\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}$$

$$\frac{\phantom{\big{(}}\quad{\displaystyle\sigma:X\to F(X)}\quad}{\phantom{\Big{(}}\quad{\displaystyle\nu_{\mathrm{intro}}\,\sigma:X\to\nu_{F}}\quad}\qquad\text{and}\qquad\frac{\phantom{\big{(}}\quad{\displaystyle}\quad}{\phantom{\Big{(}}\quad{\displaystyle\nu_{\mathrm{elim}}:\nu_{F}\to F(\nu_{F})}\quad}$$

$${\nu }_{\mathrm{elim}}({\nu }_{\mathrm{intro}}\sigma x)=F_{{\nu }_{\mathrm{intro}}\sigma }(\sigma x).$$

$$\frac{\phantom{\big{(}}\quad{\displaystyle\sigma:X\subset F(X)}\quad}{\phantom{\Big{(}}\quad{\displaystyle\nu_{\mathrm{intro}}\,\sigma:X\subset\nu_{F}}\quad}\qquad\text{and}\qquad\frac{\phantom{\big{(}}\quad{\displaystyle}\quad}{\phantom{\Big{(}}\quad{\displaystyle\nu_{\mathrm{elim}}:\nu_{F}\subset F(\nu_{F})}\quad}$$

$${\nu }_{\mathrm{elim}}({\nu }_{\mathrm{intro}}\sigma ix)=F_{{\nu }_{\mathrm{intro}}\sigma }i(\sigma ix).$$

$$T_1$$

$$F(C_1)$$

$$F(T_2)$$

$$R$$

$$i\mathrel{\epsilon}\left\llbracket w\right\rrbracket(X)\quad=\quad\left(\big{.}\Sigma\,a:A(i)\right)\,{}\left(\big{.}\Pi\,d:D(i,a)\right)\,{}i[a/d]\mathrel{\epsilon}X\,.$$

$$X\subset Y\quad\to\quad\left\llbracket w\right\rrbracket(X)\subset\left\llbracket w\right\rrbracket(Y)$$

$$\left\llbracket w_{2}\right\rrbracket\circ\left\llbracket w_{1}\right\rrbracket(X)==\left\llbracket w_{2}\circ w_{1}\right\rrbracket(X)$$

$$\left(\big{.}\Pi\,d:D\right)\,{}\left(\big{.}\Sigma\,a:A(d)\right)\,{}\varphi(d,a)\quad\leftrightarrow\quad\left(\big{.}\Sigma\,f:\left(\big{.}\Pi\,d:D\right)\,{}A(d)\right)\,{}\left(\big{.}\Pi\,d:D\right)\,{}\varphi(d,f\,d)$$

$$\begin{array}[b]{@{}c@{}}\displaystyle\begin{array}[]{rclr}i\mathrel{\epsilon}\left\llbracket w_{2}\right\rrbracket\circ\left\llbracket w_{1}\right\rrbracket(X)&=&\left(\big{.}\Sigma\,a_{1}:A_{1}(i)\right)\,{}\left(\big{.}\Pi\,d_{1}:D_{1}(i,a_{1})\right)\,{}\left(\big{.}\Sigma\,a_{2}:A_{2}(i[a_{1}/d_{1}])\right){}\\ &&\left(\big{.}\Pi\,d_{2}:D_{2}(i[a_{1}/d_{1}],a_{2})\right)\,{}i[a_{1}/d_{1}][a_{2}/d_{2}]\mathrel{\epsilon}X\\ \text{\footnotesize(axiom of choice)}&\leftrightarrow&\left(\big{.}\Sigma\,a_{1}\right)\,{}\left(\big{.}\Sigma\,f:\left(\big{.}\Pi\,d_{1}:D_{1}(i,a_{1})\right)\,{}A_{2}(i[a_{1}/d_{1}])\right)\,{}\left(\big{.}\Pi\,d_{1}\right){}\\ &&\left(\big{.}\Pi\,d_{2}\right)\,{}i[a_{1}/d_{1}][f\,d_{1}/d_{2}]\mathrel{\epsilon}X\\ &\leftrightarrow&\left(\big{.}\Sigma\,\textlangle a_{1},f\textrangle\right)\,{}\left(\big{.}\Pi\,\textlangle d_{1},d_{2}\textrangle\right)\,{}i[a_{1}/d_{1}][f\,d_{1}/d_{2}]\mathrel{\epsilon}X\\ &=&i\mathrel{\epsilon}\left\llbracket w_{2}\circ w_{1}\right\rrbracket(X)\,.\end{array}\\[-3.99994pt] \hrule height=0.0pt\cr\end{array}$$

$$i\mathrel{\epsilon}\left\llbracket w^{\bot}\right\rrbracket(X)\quad\longleftrightarrow\quad\left(\big{.}\Pi\,a:A(i)\right)\,{}\left(\big{.}\Sigma\,d:D(i,a)\right)\,{}i[a/d]\mathrel{\epsilon}X\,.$$

$$\left(\big{.}\Sigma\,f:A^{\bot}(i)\right)\,{}\left(\big{.}\Pi\,a:D^{\bot}(i,f)\right)\,{}\varphi(a,f\,a)\leftrightarrow\left(\big{.}\Pi\,a:A(i)\right)\,{}\left(\big{.}\Sigma\,d:D(i,a)\right)\,{}\varphi(a,d)\,.$$

$$\left(\big{.}\Sigma\,a_{1}\right)\,{}\left(\big{.}\Pi\,d_{1}\right)\,{}\left(\big{.}\Sigma\,a_{2}\right)\,{}\left(\big{.}\Pi\,d_{2}\right)\,{}\ \dots\ \ i[a_{1}/d_{1}][a_{2}/d_{2}]\dots\mathrel{\epsilon}X\,.$$

$$\frac{\phantom{\big{(}}\quad{\displaystyle}\quad}{\phantom{\Big{(}}\quad{\displaystyle\mathtt{Leaf}:A^{\ast}(i)}\quad}\quad\text{and}\quad\frac{\phantom{\big{(}}\quad{\displaystyle a:A(i)\qquad k:\left(\big{.}\Pi\,d:D(i,a)\right)\,{}A^{\ast}(n\,i\,a\,d)}\quad}{\phantom{\Big{(}}\quad{\displaystyle\mathtt{Node}(a,k):A^{\ast}(i)}\quad}\,.$$

$$\begin{array}[]{lclclcl}D^{\ast}\big{(}i,\mathtt{Leaf}(i)\big{)}&=&{\bf 1}:\mathsf{Set}\\ n^{\ast}\big{(}i,\mathtt{Leaf}(i),\star\big{)}&=&i:I\\ \end{array}$$

$$\begin{array}[]{lcl}D^{\ast}\big{(}i,\mathtt{Node}(a,k)\big{)}&=&\left(\big{.}\Sigma\,d:D(i,a)\right)\,{}D^{\ast}\big{(}i[a/d],f\,d\big{)}:\mathsf{Set}\\ n^{\ast}\big{(}i,\mathtt{Node}(a,k),\textlangle d,d^{\prime}\textrangle\big{)}&=&n^{\ast}\big{(}i[a/d],k\,d,d^{\prime}\big{)}:I\,.\end{array}$$

Full text

The author wants to thank both Peter Hancock and the reviewers. The former should get credits for many of the ideas developed in this paper. He visited Chambéry many years ago and most of the results started to take form then and there. The latter contributed many helpful comments much more recently when the paper was finally submitted.

Introduction

This paper gives a type theoretic representation theorem for continuous functions (Theorems 28 and 29) between a wide class of spaces of infinite values. By infinite, we understand a value having a coinductive type. Continuity means that finite information about a result of the function requires only finite information about its argument. Because of that, it is a necessary condition for computability.

The simplest coinductive space is the Cantor space of infinite boolean sequences. It corresponds to the coinductive type $\nu_{X}(X+X)$ and its topology is well known. Programs that implement continuous functions from the Cantor space to a discrete space $D$ can be represented by finite binary trees in which leaves are labelled by values in $D$. We extend this to a class of functors going beyond $X\mapsto X+X$ on the category $\mathsf{Set}$ by considering so-called (finitary) polynomial functors on $\mathsf{Set}^{I}$ for some index set $I$. The final coalgebra $\nu P$ of such a functor $P$ always exists and may be constructed as the inverse limit of: $1\leftarrow P({\bf 1})\leftarrow P^{2}({\bf 1})\leftarrow\cdots$. Those final coalgebras have a natural topology, and when the functor $F$ is finitary (commutes with filtered colimits), the topology enjoys a close connection with the intuitive notion of “finite amount of information” about potentially infinite values. However, representing such topologies inside a formalized system such as dependent type theory is far from trivial because their definition relies heavily on delicate topics like equality.

Our main result pertains to the question of how continuous functions between these natural classes of spaces can be represented in dependent type theory. It turns out that any such “implementation” can itself be put into the form of a potentially infinite data-structure, inhabiting a final coalgebra for an appropriate functor, albeit one which is in most cases no longer finitary. This settles a conjecture of P. Hancock about representability of continuous between “dependent streams” [GHP09b] by extending the work of P. Hancock, N. Ghani and D. Pattinson [GHP09a] from containers to indexed containers. The technology and root ideas are very similar.

We obtain this result via a more general construction, without any cardinality restrictions on the initial functors. One can still topologise the final coalgebras, though the topology that arises from the inverse chain construction no longer enjoys much connection with any intuition of finite information, and there are (classically) continuous functions that cannot be implemented by programs.

1. Preliminaries I. Streams and Trees in Point Set Topology

1.1. Streams

Given a set $X$ endowed with the discrete topology, the set of streams over $X$, written $\mathtt{stream}(X)$, is defined as the infinite product $\prod_{i\geq 0}X$. The product topology is generated from the basic open sets $\prod_{i\geq 0}U_{i}$ where finitely many $U_{i}$s are of the form $\{x_{i}\}$ for some $x_{i}\in X$ and the other $U_{i}$s are equal to $X$. This topological space is usually called the Cantor space (when $X$ is finite) or the Baire space (when $X$ is countably infinite). Continuity for functions between streams amounts to the following:

Lemma 1**.**

A function $f:\mathtt{stream}(X)\to\mathtt{stream}(Y)$ is continuous if and only if, for each stream $s$ in $\mathtt{stream}(X)$, each projection $f(s)_{k}$ of $f(s)$ depends on at most a finite prefix of $s$.

Writing $s_{\upharpoonright n}$ for the restriction of stream $s$ to its finite prefix of length $n$, the condition is equivalent to

[TABLE]

Before proving Lemma 1, let’s look at a preliminary result.

Lemma 2**.**

For any subset $V\subseteq\mathtt{stream}(X)$, we have: $V$ is open iff

[TABLE]

Proof 1.1**.**

The $\Rightarrow$ direction is immediate: an open set is a union of basic open sets, which satisfy the condition. (Recall that a basic open set is of the form $\prod_{i\geq 0}U_{i}$, where each $U_{i}$ is $X$, except for finitely many that are singleton sets.)

For the $\Leftarrow$ direction, we define, for each $s\in V$, the set $V_{s}=\{t\mid s_{\upharpoonright n_{s}}=t_{\upharpoonright n_{s}}\}$, where $n_{s}$ is the integer coming from condition. We have $V=\bigcup_{s\in V}V_{s}$.

Proof 1.2** (Proof of Lemma 1).**

Suppose the function $f:\mathtt{stream}(X)\to\mathtt{stream}(Y)$ satisfies condition $(\ref{eqn:prefix_condition})$. To show that $f$ is continuous, it is enough to show that the inverse image of any basic open set is an open set. Because the inverse image commutes with intersections, it is sufficient to look at pre basic open sets of the form $V_{k,y}=\{s\mid s_{k}=y\}$.

To show that $f^{-1}(V_{k,y})$ is open, we use Lemma 2 and show that $s\in f^{-1}(V_{k,y})$ implies

[TABLE]

Because $s\in f^{-1}(V_{k,y})$ is $f(s)_{k}=y$, this is implied by condition $(\ref{eqn:prefix_condition})$.

For the converse, suppose $f:\mathtt{stream}(X)\to\mathtt{stream}(Y)$ is continuous. We want to show that it satisfies condition $(\ref{eqn:prefix_condition})$. Let $s\in\mathtt{stream}(X)$ and $k\geq 0$. The set $\{t\mid f(t)_{k}=f(s)_{k}\}$ is open and because $f$ is continuous, its inverse image also is open. By Lemma 2, we now that there is some $n$ such that $s_{\upharpoonright n}=t_{\upharpoonright n}\Rightarrow f(t)_{k}=f(s)_{k}$. This finishes the proof.

Because of this, constructive functions between streams are usually held to be continuous. We expect them to arise as continuous functions with the additional properties that:

• •

finding the finite prefix needed to compute a chosen element of $f(s)$ is computable, and

• •

finding the value of the element of $f(s)$ from that finite prefix is computable.

Note that the discrete space $X$ may be generalized to a family $(X_{i})_{i\geq 0}$ that need not be constant. More interestingly, we can allow the set $X_{i}$ (giving the set of possible values for the $i$th element of a stream) to depend on the $i$th prefix of the stream. We can in this way obtain the space of increasing streams of natural numbers:

• •

the set $X_{0}$ does not depend on anything and is defined as $\mathbb{N}$,

• •

the set $X_{1}$ depends on the value of $x_{0}\in X_{0}$: $X_{1,x_{0}}=\{k\in\mathbb{N},x_{0}\leq k\}$,

• •

the set $X_{2}$ depends on $x_{1}\in X_{1,x_{0}}$, etc.

The set of increasing streams is not naturally a product space but is a subspace of $\mathtt{stream}(\mathbb{N})$. Because of that, the topology is the expected one and continuous functions are still characterized by Lemma 1.

1.2. Infinite Trees, Natural Topology

The natural topology for sets of infinite trees is less well known than the Cantor and Baire topologies. The simplest kind of infinite tree, the infinite binary tree has a root, and two distinguished “branches” going from that root to two “nodes”. Each of these two nodes also has two branches, etc. An infinite binary tree over $X$ is a way to label each node of the infinite binary tree with an element of $X$. If we write $\mathbb{B}$ for the set $\{0,1\}$, each node of the infinite binary tree can be identified by a list of elements of $\mathbb{B}$: this list simply represents the branch leading to this node from the root. The set of infinite binary trees over $X$, written $\mathtt{tree}_{\mathbb{B}}(X)$, can thus be defined as

[TABLE]

where each term gives the $i$th “layer” of the tree as a function from finite branches of length $i$ to $X$. We can rewrite this as

[TABLE]

By replacing the set $\mathbb{B}$ by some other set $B$, we obtain the ternary trees over $X$ or countably-branching trees over $X$, etc. Streams themselves are recovered by taking $B=\{\star\}$. If both $B$ and $X$ are endowed with the discrete topology, we obtain a natural topology on $\mathtt{tree}_{B}(X)$. Note that when $B$ is infinite, the spaces $B^{i}\to X$ are not discrete anymore. Nevertheless, we have:

Lemma 3**.**

Let $A$, $B$, $X$ and $Y$ be discrete spaces; a function $f:\mathtt{tree}_{A}(X)\to\mathtt{tree}_{B}(Y)$ is continuous iff for every $t\in\mathtt{tree}_{A}(X)$, the value at each node of $f(t)$ only depends on a finite subtree111A subtree is a set of nodes that contains the root of the tree and is closed by the ancestor relation. of $t$.

Proof 1.3**.**

The proof of this lemma is exactly the same as the proof of Lemma 1, except that we replace the natural number $n$ in $t_{\upharpoonright n}$ (for some $t\in\mathtt{tree}_{B}(Y)$) by a finite subtree. The only remark is that basic open sets of $\mathtt{tree}_{B}(Y)$ are of the form $\prod_{i\geq 0}\prod_{t\in B^{i}}X_{i,t}$ where all sets $X_{i,t}$ are equal to $X$, except for finitely many that are singletons of the form $\{x_{i,t}\}$ for some $x_{i,t}\in X$.

It is again possible to devise more general notions of trees by allowing the set $X$ at a node in the tree to depend on the values of its location as a path from the root. The resulting space is endowed with the subspace topology and Lemma 3 still holds. We will later generalize this notion further by allowing the branching of a node (given by the set $B$) to depend itself on the value stored at the node. With this generalisation we can model very general objects, such as infinite automata that issue commands and change to a new state (choose a branch) based on the responses.

1.3. Infinite Trees, Wild Topology

The topology we naturally get in this paper corresponds to a different topology on trees. When looking at

[TABLE]

we can endow the inner product space with the “box” topology, where basic opens are given by arbitrary products of open sets. Because $B$ and $X$ are discrete sets, this amounts to giving the discrete topology to each layers $B^{i}\to X$. Instead of being generated by “finite subtrees”, open sets are generated by “subtrees with finite depth”.

Lemma 4**.**

Let $A$, $B$, $X$ and $Y$ be discrete spaces; a function $f:\mathtt{tree}_{A}(X)\to\mathtt{tree}_{B}(Y)$ is continuous for the wild topology iff for every $t\in\mathtt{tree}_{A}(X)$, and $k\in\mathbb{N}$, there is an $n\in\mathbb{N}$ such that the nodes of $f(t)$ at depth less than $k$ depend only on the nodes of $t$ at depth less than $n$.

Formally, this looks very similar to condition $(\ref{eqn:prefix_condition})$ on page $\ast$ ‣ 1.1:

[TABLE]

where $t_{\upharpoonright k}$ is the complete subtree of $t$ up-to depth $k$. Intuitively, this topology considers infinite trees as streams of their layers, where layers are discrete.

When $A$ and $B$ are finite, the two notions of continuity (Lemma 3 and 4) coincide. When this is not the case, we cannot compare continuous functions for the two topologies.

• •

Consider $f:\mathtt{stream}(\mathbb{N})\to\mathtt{tree}_{\mathbb{N}}(\mathbb{N})$ sending the stream $s$ to the tree $f(s)$ where the node indexed by $(i_{0},\dots,i_{n})$ is $s_{i_{0}}+s_{i_{1}}+...+s_{i_{n}}$. This is certainly continuous for the natural topology. However, because the first layer of the output is infinite, we cannot bound the number of layers (elements) of the input stream $s$ that are needed to construct it: this function is not continuous for the wild topology.

• •

Consider $g:\mathtt{tree}_{\mathbb{N}}(\mathbb{B})\to\mathtt{stream}(\mathbb{B})$ where the $i$th element of $g(t)$ is the maximum of the complete $i$th layer of $t$ ($\mathbb{B}$ being the complete lattice with two elements). This function is continuous in the wild sense, but because we need to know the whole $i$th layer of the input to get the $i$th value of the output, this function is not continuous for the natural topology (and certainly not computable).

2. Preliminaries II. Martin Löf Type Theory

2.1. Basic Features

We work in a meta theory that is in essence Martin-Löf’s dependent type theory [ML01] with two additional features:

• •

coinductive types,

• •

inductive-recursive definitions.

All the constructions described in the paper have been defined using the dependently typed functional programming language Agda [tea19].

A Note about Equality

This paper is concerned with constructions in “pure” type theory, i.e. dependent type theory without identity. Those constructions enjoy many interesting properties, but proving them requires some notion of equality. Equality in Martin-Löf type theory is a complex subject about which whole books have been written [Uni13]. We try to be mostly agnostic about the flavor of equality we are using and only rely on the “simplest” one: intentional equality, written $a\equiv_{T}b$, or simply $a\equiv b$. This makes it possible to use vanilla Agda for checking proofs.222All the Agda code was checked using Agda 2.6.1.1 with the flag --without-K. The Agda code is available at http://www.lama.univ-smb.fr/~hyvernat/Files/Infinite/agda.tgz, with the file PAPER.agda referencing all the formalized results from the paper. For those without a working Agda installation, the code is also browsable directly from http://www.lama.univ-smb.fr/~hyvernat/Files/Infinite/browse/PAPER.html.

We annotate the proofs in the paper with

• •

[Agda✓] : for those that have been formalized using Agda,

• •

[Agda✗] : for those which have only partly been formalized, typically because the proof is too complex to write in Agda, or because it requires a much stronger version of equality than we have at our disposal.

Because we want to explain Agda code only slightly less than you want to read Agda code, the formalized proofs are either omitted from the paper, or explained informally.

We sometimes need to assume equality for functions is extensional, i.e. that $f\equiv g$ iff $f\,a\equiv_{B}g\,a$ for all $a:A$. Those proofs are clearly identified.

Notation

The notation for dependent types is standard. Here is a summary:

• •

We write $\Gamma\vdash B$ to mean that $B$ is a well-formed type in context $\Gamma$. We write $A=B$ to express that $A$ and $B$ are the same by definition.

• •

We write $\Gamma\vdash b:B$ to mean that $b$ is an element of type $B$ in context $\Gamma$. The context is often left implicit and we usually write $b:B$. We write $a=b:B$ to express that $a$ and $b$ are definitionally equal in type $B$. When the type $B$ can easily be deduced from the context, we will usually write just $a=b$.

• •

If $B$ is a type and $C$ is a type depending on $x:B$, i.e. , $x:B\vdash C$, we write

• –

\left(\big{.}\Sigma\,x:B\right)\,{}C for the dependent sum. Its canonical elements are pairs $\textlangle b,c\textrangle$ with $b:B$ and $c:C[x/b]$,

• –

\left(\big{.}\Pi\,x:B\right)\,{}C for the dependent product. Its canonical elements are functions $(\lambda\,x:B)\,{}u$ where $x:B\vdash u:C$.

When the type $C$ is constant, we abbreviate those by $B\times C$ and $B\to C$.

• •

The usual amenities are present: the natural numbers, W-types and so on.

We use a universe $\mathsf{Set}$ of “small types” containing ${\bf 0}$ (with no element), ${\bf 1}$ (with a single element $\star$) and ${\bf 2}$ (with two elements [math] and $1$). Moreover, the dependent sums and products are reflected in this universe, and we use the same notation \left(\big{.}\Sigma\,b:B\right)\,{}C and \left(\big{.}\Pi\,b:B\right)\,{}C whenever $B:\mathsf{Set}$ and $b:B\vdash C:\mathsf{Set}$. We assume that this universe is closed under many inductive-recursive and coinductive definitions which will be treated below.

We are not always consistent with notation for application of functions and usually write

• •

$f\,x$ when the result is an element of a small type (an element of $\mathsf{Set}$),

• •

$A(i)$ when the result is itself a small type (and thus, not an element of $\mathsf{Set}$).

Predicates and Families

The Curry-Howard isomorphism makes the type $\mathsf{Set}$ into a universe of propositions. {defi} If $A:\mathsf{Set}$, the collection of predicates on $A$ is defined as

[TABLE]

We introduce the following notations [SV93]: if $X$ and $Y$ are predicates on $A$,

• •

“$a\mathrel{\epsilon}X$” is “$X(a)$”,

• •

“$X\subset Y$” is “\left(\big{.}\Pi\,a:A\right)\,{}(a\mathrel{\epsilon}X)\to(a\mathrel{\epsilon}Y),

• •

“$X\between Y$” is “\left(\big{.}\Sigma\,a:A\right)\,{}(a\mathrel{\epsilon}X)\times(a\mathrel{\epsilon}Y)”,

• •

“$X\cap Y$” is “$(\lambda\,a:A)\,{}(a\mathrel{\epsilon}X)\times(a\in Y)$”,

• •

“$X\cup Y$” is “$(\lambda\,a:A)\,{}(a\mathrel{\epsilon}X)+(a\in Y)$”.

The intuition is that a predicate on $A$ is just a subset of $A$ in some constructive and predicative333if $A:\mathsf{Set}$, $\mathsf{Pow}(A)$ is not of type $\mathsf{Set}$ set theory. It is then natural to call a predicate on some $A\times B$ a binary relation. We sometimes identify a relation $R:\mathsf{Pow}(A\times B)$ with its curried version $R:A\to\mathsf{Pow}(B)$. Finally, we define the following trivial operation {defi} If $R:\mathsf{Pow}(A\times B)$, the converse $R^{\sim}$ is the predicate in $\mathsf{Pow}(B\times A)$ given by

[TABLE]

We will also need a notion of family. {defi} A family of $C$ is given by a set $I$ together with a function from $I$ to $C$. In other words,

[TABLE]

2.2. Inductive-recursive Definitions

Inductive definitions are a way to define (weak) initial algebras for endofunctors on $\mathsf{Set}$. A typical example is defining $\mathtt{list}(X)$ as the least fixed point of $Y\mapsto{\bf 1}+X\times Y$. In their simplest form, inductive-recursive definitions [Dyb00] give a way to define (weak) initial algebras for endofunctors on $\mathsf{Fam}(C)$.444To ensure the definition is healthy, the endofunctor has to be expressible according to a certain coding scheme [DS03]. It means we can define, at the same time:

• •

a inductive set $U$, called the index set,

• •

and a recursive function $f:U\to C$.

Of course, the set $U$ and the function $f$ may be mutually dependent.

The type $C$ may be large or small. Taking $C={\bf 1}$, we recover usual inductive types as the index part of such a definition, the recursive function $f$ always being trivial. In non-degenerate cases, the inductive clauses defining $U$ are expressed using the simultaneously defined function $f$. Here is a traditional example with $C=\mathsf{Set}$: complete binary trees indexed by $X$, defined one layer at a time. Here is the definition, first using Agda syntax:

mutual data Tree (X : Set) : Set where Empty : Tree X AddLayer : (t : Tree X) → (branches t $\times$ Bool → X) → Tree X branches : {X : Set} → Tree X → Set branches Empty = One branches (AddLayer t l) = (branches t) $\times$ Bool

While Empty corresponds to the empty tree, the definitions

T₁ = AddLayer Empty (λ b → if b.2 then 2 else 1) T₂ = AddLayer T₁ (λ b → if b.1.2 && b.2 then 6 elif b.1.2 && not b.2 then 5 elif not b.1.2 && b.2 then 4 else 3)

give trees labeled by natural numbers: (putting the “False” branch on the left, and the “True” branch on the right)

[TABLE]

The corresponding functor takes the family $\textlangle T:\mathsf{Set},b:T\to\mathsf{Set}\textrangle$ to the family

• •

index set: T^{\prime}={\bf 1}+\left(\big{.}\Sigma\,t:T\right)\,{}\big{(}(b\,t\times{\bf 2})\to\mathbb{N}\big{)},

• •

recursive function $b^{\prime}$ defined with

• –

$b^{\prime}\,\star={\bf 1}$, where $\star$ is the only element of ${\bf 1}$,

• –

$b^{\prime}\,\textlangle t,l\textrangle=(b\,t)\times{\bf 2}$.

We will, in Section 5.1, encounter a similar situation in which the type $C$ will be $\mathsf{Fam}(I)$, i.e. we will need to take the least fixed point of a functor from \mathsf{Fam}\big{(}\mathsf{Fam}(I)\big{)} to itself.

Another typical example involves defining a universe $U$ of types closed under dependent function space: $U$ needs to contains inductive elements of the form \left(\big{.}\Pi\,A:U\right)\,{}(B:\mathsf{fam}(A)), but $\mathsf{fam}(A)$ is defined as $\mathsf{El}(A)\to U$ and makes use of the decoding function $\mathsf{El}:U\to\mathsf{Set}$.

2.3. Greatest Fixed Points

In its simplest form a coinductive definition introduces some $\nu_{F}:\mathsf{Set}$ together with a weakly terminal coalgebra $c:\nu_{F}\to F(\nu_{F})$ for a sufficiently healthy555for our purposes, “sufficiently healthy” amounts to “polynomial” functor $F:\mathsf{Set}\to\mathsf{Set}$. For example, given a set $A$, the functor $F(X)=A\times X$ is certainly healthy and the set $\nu_{F}$ corresponds to the set of streams over $A$. The coalgebra $c$ “decomposes” a stream $[a_{0},a_{1},\ldots]$ into the pair $\textlangle a_{0},[a_{1},a_{2},\ldots]\textrangle$ of its head and its tail. Because the coalgebra is weakly terminal, for any other such coalgebra $x:X\to F(X)$ there is a map $X\to\nu_{F}$. The corresponding typing rules are given by

[TABLE]

and the computation rule is

[TABLE]

Such coinductive definitions can be extended to families of sets: given an index set $I$, we introduce weakly terminal coalgebras for a sufficiently healthy functor acting on $\mathsf{Pow}(I)$. The typing rules are extended as follows:

[TABLE]

together with the computation rule

[TABLE]

Note that it does not seem possible to guarantee the existence of strict terminal coalgebras [McB09] without extending considerably the type theory.666It is apparently possible to do so in univalent type theory [ACS15], where coinductive types can be defined from inductive ones, just like in plain old set theory!

Bisimulations

Equality in type theory is a delicate subject, and it is even more so in the presence of coinductive types. The usual (extensional or intensional) equality is easily defined and shown to enjoy most of the expected properties. However, it is not powerful enough to deal with infinite objects. Two infinite objects are usually considered “equal” when they are bisimilar. Semantically, bisimilarity has a simple definition [AM89, Sta11, ACS15]. In the internal language, two coalgebras are bisimilar if their decompositions are equal, coinductively. {defi} Given a locally cartesian closed category $\mathbb{C}$ with an endofunctor $F$ and two coalgebra $c_{i}:T_{i}\to F(T_{i})$ ($i=1,2$), a bisimulation between $T_{1}$ and $T_{2}$ is given by a span $T_{1}\leftarrow R\rightarrow T_{2}$ with a coalgebra structure such that the following diagram commutes.

[TABLE]

In particular, the identity span $T\leftarrow T\rightarrow T$ is always a bisimulation and the converse of a bisimulation between $T_{1}$ and $T_{2}$ is a bisimulation between $T_{2}$ and $T_{1}$.

Functions between coinductive types ought to be congruences for bisimilarity: {defi} If $f_{i}:C_{i}\to D_{i}$ ($i=1,2$) are morphisms from coalgebras $c_{i}:C_{i}\to F(C_{i})$ to coalgebras $d_{i}:D_{i}\to F(D_{i})$, we say that $f_{1}$ and $f_{2}$ are equal up to bisimulation, written $f_{1}\approx f_{2}$, if for every bisimulation $C_{1}\leftarrow R\rightarrow C_{2}$, there is a bisimulation $D_{1}\leftarrow S\rightarrow D_{2}$ and a morphism $h:R\to S$ making the following diagram commute.

[TABLE]

Translated in the internal language, $f_{1}\approx f_{2}$ means that if $x$ and $y$ are bisimilar, then $f_{1}\,x$ and $f_{2}\,y$ are also bisimilar. It is not difficult to show that

• •

$\approx$ is reflexive and symmetric,

• •

$\approx$ is compositional: if $f_{1}\approx f_{2}$ and $g_{1}\approx g_{2}$, then $f_{1}g_{1}\approx f_{2}g_{2}$ (if the composition makes sense).

Without additional properties (which hold in our context), $\approx$ is however not transitive.

Coinductive types are interpreted by weakly terminal coalgebras. There can be, in principle, several non-isomorphic weakly terminal coalgebras. We however have the following.

Lemma 5**.**

Let $T_{1}$ and $T_{2}$ be weakly terminal coalgebras for the endofunctor $F$,

• •

if $m:T_{1}\to T_{2}$ is a mediating morphisms, then $m\approx\mathrm{id}$,

• •

if $f:T_{1}\to T_{2}$ and $g:T_{2}\to T_{1}$ are mediating morphisms, then $gf\approx\mathrm{id}_{T_{1}}$ and $fg\approx\mathrm{id}_{T_{2}}$.

Proof 2.1**.**

Consider the following diagram:

[TABLE]

The only thing needed to make it commutative is that the bottom right square is commutative. This follows from the fact that $m$ is a mediating morphism between the weakly terminal coalgebras:

[TABLE]

*The second point is a direct consequence of the first one. *

{asm}

We assume our type theory is “compatible” with bisimilarity, in the sense that any definable function $f$ satisfies $f\approx f$.

Since it is possible to construct a dependent type theory where bisimilarity is intensional equality [ACS15, MV19], this assumption is reasonable. In our case, it allows to simplify some of the (pen and paper) proofs while not needing the extension of our type theory.

The only use of this assumption will be Lemma 11 on page 11, to reduce proofs of $f\approx g$ to proofs of “$f\ x$ and $g\ x$ are bisimilar for all $x$”.777instead of the much more tedious “$f\ x_{1}$ and $g\ x_{2}$ are bisimilar if $x_{1}$ and  $x_{2}$ are”

3. Indexed Containers

Indexed containers [AM09] were first considered (implicitly) in type theory 30 years ago by K. Petersson and D. Synek [PS89]. Depending on the context and the authors, they are also called interaction systems [HH06] or polynomial diagrams [GK13, Hyv14a]

{defi}

For $I:\mathsf{Set}$, an indexed container over $I$ is a triple $w=\textlangle A,D,n\textrangle$ where

• •

$i:I\vdash A(i):\mathsf{Set}$,

• •

$i:I,a:A\vdash D(i,a):\mathsf{Set}$,

• •

$i:I,a:A,d:D\vdash n(i,a,d):I$.888An abstract, but equivalent, way of defining indexed containers over $I$ is as functions I\to\mathsf{Fam}\big{(}\mathsf{Fam}(I)\big{)}.

In Agda, the definition looks like999The name IS comes from “Interaction System”, another name for indexed containers.

record IS (I : Set) where field A : I → Set D : (i : I) → A i → Set n : (i : I) → (a : A i) → D i a → I  

A useful intuition is that $I$ is a set of states and that $\textlangle A,D,n\textrangle$ is a game:

• •

$A(i)$ is the set of moves (or actions or commands) in state $i$

• •

$D(i,a)$ is the set of counter-moves (or reactions or responses) after move $a$ in state $i$,

• •

$n(i,a,d):I$ is the new state after move $a$ and counter-move $d$ have been played. When no confusion arises, we sometimes write $i[a/d]$ for $n(i,a,d)$.

Each indexed container gives rise to a monotone operator on predicates over $I$: {defi} If $w=\textlangle A,D,n\textrangle$ is an indexed container over $I:\mathsf{Set}$, the extension of $w$ is the operator: \left\llbracket w\right\rrbracket:\mathsf{Pow}(I)\to\mathsf{Pow}(I) where

[TABLE]

Lemma 6**.**

The operator \left\llbracket w\right\rrbracket is monotonic, i.e., the following type is inhabited:

[TABLE]

for every predicates $X$ and $Y$ of the appropriate type.

Proof 3.1**.**

[Agda✓]* This is direct: given $i:X\subset Y$ and \langle a,f\rangle:\left\llbracket w\right\rrbracket(X), we just need to “carry” $i$ through \left\llbracket w\right\rrbracket and return $\langle a,i\circ f\rangle$. *

Indexed containers form the objects of several categories of interest [HH06, GK13, AM09, Hyv14a], but that will only play a very minor role here.

Many indexed containers of interest have singleton actions or singleton reactions. {defi} An indexed container $\langle A,D,n\rangle$ is called

• •

angelic if $D(i,a)$ is always (isomorphic to) a singleton type,

• •

demonic if $A(i)$ is always (isomorphic to) a singleton type,

• •

lopsided if it is either angelic or demonic.

3.1. Composition

Extensions of indexed containers can be composed as functions. There is a corresponding operation on the indexed containers. {defi} If $w_{1}=\textlangle A_{1},D_{1},n_{1}\textrangle$ and $w_{2}=\textlangle A_{2},D_{2},n_{2}\textrangle$ are two indexed containers on $I$, the composition of $w_{1}$ and $w_{2}$ is the indexed container $w_{2}\circ w_{1}=\textlangle A,D,n\textrangle$ where

• •

A(i)=\left(\big{.}\Sigma\,a_{1}:A_{1}(i)\right)\,{}\left(\big{.}\Pi\,d_{1}:D_{1}(i,a_{1})\right)\,{}A_{2}\big{(}i_{1}[a_{1}/d_{1}]\big{)}=i\mathrel{\epsilon}\left\llbracket w_{1}\right\rrbracket(A_{2}),

• •

D\big{(}i,\textlangle a_{1},f\textrangle\big{)}=\left(\big{.}\Sigma\,d_{1}:D_{1}(i,a_{1})\right)\,{}D_{2}\big{(}i[a_{1}/d_{1}],f\,d_{1}\big{)},

• •

n\big{(}i,\textlangle a_{1},f\textrangle,\textlangle d_{1},d_{2}\textrangle\big{)}=n_{2}\big{(}n_{1}(i,a_{1},d_{1}),f\,d_{1},d_{2}\big{)}.

Lemma 7**.**

For every indexed containers $w_{1}$ and $w_{2}$ and predicate $X$, we have

[TABLE]

where $Y==Z$ is an abbreviation for $(X\subset Y)\times(Y\subset X)$.

If function extensionality holds, the pair of functions are inverse to each other.

Proof 3.2**.**

[Agda✓]* The main point is that the intensional axiom of choice*

[TABLE]

is provable in Martin-Löf type theory. We then have

[TABLE]

3.2. Duality

{defi}

If $w=\textlangle A,D,n\textrangle$ is an indexed container over $I$, we write $w^{\perp}$ for the indexed container $\textlangle A^{\perp},D^{\perp},n^{\perp}\textrangle$ where

• •

A^{\perp}(i)=\left(\big{.}\Pi\,a:A(i)\right)\,{}D(i,a),

• •

$D^{\perp}(i,{\texttt{\char 95\relax}})=A(i)$, (note that it does not depend on the value of $f:A^{\bot}(i)$)

• •

$i[f/a]=i[a/f\,a]$.

Lemma 8**.**

For every indexed container $w=\textlangle A,D,n\textrangle$, the following type is inhabited:

[TABLE]

With function extensionality, this is an isomorphism.

Proof 3.3** (Sketch of proof).**

[Agda✓]* Just like Lemma 7, the proof relies on the intensional axiom of choice, which shows that*

[TABLE]

It is interesting to note that lopsided containers are closed under duality, and that duality is involutive on them. For any family $X$ indexed by $I$ and t:\left(\big{.}\Pi\,i:I\right)\,{}X(i)\to I, the following containers are dual to each other:

• •

$A(i)=X(i)$,

• •

$D(i,x)=\{\star\}$,

• •

$i[x/\star]=t(i,x)$.

and

• •

$A(i)=\{\star\}$,

• •

$D(i,\star)=X(i)$,

• •

$i[\star/x]=t(i,x)$.

3.3. Free Monad

If $w=\textlangle A,D,n\textrangle$ is an indexed container on $I$, we can consider the free monad generated by \left\llbracket w\right\rrbracket. N. Gambino and M. Hyland proved that the free monad $F_{w}$ generated by some \left\llbracket w\right\rrbracket (a dependent polynomial functor) is of the form \left\llbracket w^{\ast}\right\rrbracket for some indexed container $w^{\ast}$ [GH03]. It is characterized by the fact that \left\llbracket w^{\ast}\right\rrbracket(X) is the least fixed point of Y\mapsto X\cup\left\llbracket w\right\rrbracket(Y). In other words, we are looking for an indexed container $w^{\ast}$ satisfying

• •

X\cup\left\llbracket w\right\rrbracket\big{(}\left\llbracket w^{\ast}\right\rrbracket(X)\big{)}\subset\left\llbracket w^{\ast}\right\rrbracket(X)

• •

X\cup\left\llbracket w\right\rrbracket(Y)\subset Y\to\left\llbracket w^{\ast}\right\rrbracket(X)\subset Y.

Informally, i\mathrel{\epsilon}\left\llbracket w\right\rrbracket^{\ast}(X) iff i\mathrel{\epsilon}X\cup w\big{(}X\cup w(X\cup w(X\cup\dots))\big{)}. Expending the definition of \left\llbracket w\right\rrbracket, this means that

[TABLE]

This pseudo formula depicts a well-founded tree (with branching on $d_{i}:D({\texttt{\char 95\relax}},{\texttt{\char 95\relax}})$) in which branches are finite: either they end at a $\Pi{d_{i}}$ because the corresponding domain $D({\texttt{\char 95\relax}},{\texttt{\char 95\relax}})$ is empty, or they end in a state $i[a_{1}/d_{1}][a_{2}/d_{2}]\dots$ which belongs to $X$. The length of the sequence $a_{1}/d_{1},a_{2}/d_{2},\dots$ is finite but may depend on what moves / counter-moves are chosen as the sequence grows longer. We can define $w^{\ast}$ inductively. {defi} Define $w^{\ast}=\textlangle A^{\ast},D^{\ast},n^{\ast}\textrangle$ over $I$ as:

• •

$A^{\ast}:\mathsf{Pow}(I)$ is a weak initial algebra for the endofunctor X\mapsto(\lambda\,i)\,{}\big{(}{\bf 1}+\left\llbracket w\right\rrbracket(X)(i)\big{)} on $\mathsf{Pow}(I)$. Concretely, there are two constructors for $A^{\ast}(i)$:

[TABLE]

Thus, an element of $A^{\ast}(i)$ is a well-founded tree where each internal node is labeled with an elements $a:A(i)$ and the branching is given by the set $D(i,a)$.

• •

The components $D^{\ast}$ and $n^{\ast}$ are defined by recursion:

• –

in the case of a $\mathtt{Leaf}$:

[TABLE]

• –

in the case of a $\mathtt{Node}$:

[TABLE]

The corresponding Agda definition is

module FreeMonad (I : Set) (w : IS I) where open IS w

    data A* : I → Set where
      Leaf : (i : I) → A* i
      Node : (i : I) → (a : A i) → (f : (d : (D i a)) → A* (n a d)) → A* i

    D* : (i : I) → (t : A* i) → Set
    D* i Leaf = One
    D* i (Node a f) = $\Sigma$ (D i a) (λ d → D* (n a d) (f d))

    n* : (i : I) → (t : A* i) → (b : D* i t) → I
    n* i Leaf ⋆ = i
    n* i (Node a f) ( d , ds ) = n* (f d) ds

In the presence of extensional equality, this particular inductive definition can be encoded using standard $W$-types [GK13]. As it is given, it avoids using equality but needs either a universe, or degenerate101010in the sense that the inductive set $A^{\ast}(i)$ does not depend on the recursive functions $D^{\ast}(i,{\texttt{\char 95\relax}})$ and $n^{\ast}(i,{\texttt{\char 95\relax}},{\texttt{\char 95\relax}})$. induction-recursion on $\mathsf{Fam}(I)$. This construction does indeed correspond to the free monad described by N. Gambino and M. Hyland:

Lemma 9**.**

If $w$ is a container indexed on $I:\mathsf{Set}$, we have

1. (1)

for all $X:\mathsf{Pow}(I)$, X\cup\left\llbracket w\right\rrbracket\big{(}\left\llbracket w^{\ast}\right\rrbracket(X)\big{)}\subset\left\llbracket w^{\ast}\right\rrbracket(X) 2. (2)

for all $X,Y:\mathsf{Pow}(I)$, X\cup\left\llbracket w\right\rrbracket(Y)\subset Y\to\left\llbracket w^{\ast}\right\rrbracket(X)\subset Y.

Proof 3.4**.**

[Agda✓]**

3.4. Greatest Fixed Points

Agda has some support for infinite values via the $\infty{\texttt{\char 95\relax}}$ type constructor making a type “lazy”, i.e. stopping computation. Using this and the operators $\natural:A\to\infty A$ (to freeze a value) and $\flat:\infty A\to A$ (to unfreeze it), it is possible to define the type \nu_{\left\llbracket w\right\rrbracket} (which we’ll write $\nu_{w}$) for any indexed container $w$. The termination checker used in Agda [AA01] also checks productivity of recursive definition, but since it is not clear that this is sound when inductive and coinductive types are mixed [AD12, Hyv20] we will only use the standard introduction and elimination rules in our developments:

[TABLE]

which are definable in Agda.

Elements of $\nu_{w}$ are formed by coalgebras for \left\llbracket w\right\rrbracket, and any element of $i\mathrel{\epsilon}\nu_{w}$ can be “unfolded” into an element of i\mathrel{\epsilon}\left\llbracket w\right\rrbracket(\nu_{w}) i.e. into an element of

[TABLE]

We can repeat this unfolding and informally decompose an element of $i\mathrel{\epsilon}\nu_{w}$ into an infinite “lazy” process of the form

[TABLE]

We therefore picture an element of $i\mathrel{\epsilon}\nu_{w}$ as an infinite tree (which need not be well-founded). Each node of such a tree has an implicit state in $I$, and the root has state $i$. If the state of a node is $j$, then the node contains an element $a$ of $A(j)$, and the branching of that node is given by $D(j,a)$. Note that some finite branches may be inextensible when they end at a node of state $j$ with label $a$ for which $D(j,a)$ is empty.

Examples

We will be particularly interested in fixed points of the form $\nu_{w^{\bot}}$. Because of Lemma 8, an element of $i\mathrel{\epsilon}\nu_{w^{\bot}}$ unfolds to a potentially infinite object of the form

[TABLE]

For such types, the branching comes from $A({\texttt{\char 95\relax}})$ and the labels from $D({\texttt{\char 95\relax}},{\texttt{\char 95\relax}})$. Here are some example of the kind of objects we get.

1. (1)

Streams on $X$ are isomorphic to “$\star\mathrel{\epsilon}\nu_{w^{\bot}}$” where $I={\bf 1}=\{\star\}$ and $w=\textlangle A,D,n\textrangle$ with

• •

$A(\star)={\bf 1}$,

• •

$D(\star,\star)=X$,

• •

$n(\star,\star,x)=\star$. 2. (2)

Increasing streams of natural numbers are isomorphic to “$0\mathrel{\epsilon}\nu_{w^{\bot}}$” where $I=\mathbb{N}$ and $w=\textlangle A,D,n\textrangle$ with

• •

$A(i)={\bf 1}$,

• •

D(i,\star)=\left(\big{.}\Sigma\,j:\mathbb{N}\right)\,{}(i<j),

• •

$n(i,\star,\textlangle j,p\textrangle)=j$. 3. (3)

Infinite, finitely branching trees labeled by $X$ are isomorphic to $\star\mathrel{\epsilon}\nu_{w^{\bot}}$ where $I={\bf 1}$ and $w=\textlangle A,D,n\textrangle$ to be

• •

A(\star)=\left(\big{.}\Sigma\,k:\mathbb{N}\right)\,{}N(k), where $N(k)$ is the set with exactly $k$ elements,

• •

$D(\star,\langle k,i\rangle)=X$,

• •

$n(\star,k,x)=\star$. 4. (4)

In general, non-losing strategies for the second player from state $i:I$ in game $w$ are given by $i\mathrel{\epsilon}\nu_{w^{\bot}}$.

Bisimulations

The appropriate equivalence relation on coinductive types is bisimilarity. Translating the categorical notion from page 2.3 for the type $\nu_{w}$,111111Note that we only define bisimilarity for elements of $i\mathrel{\epsilon}\nu_{w}$, and not for arbitrary  \left\llbracket w\right\rrbracket-coalgebras. we get that $T_{1}:i_{0}\mathrel{\epsilon}\nu_{w}$ is bisimilar to $T_{2}:i_{0}\mathrel{\epsilon}\nu_{w}$ if:

1. (1)

there is an $I$ indexed family $R_{i}:(i\mathrel{\epsilon}\nu_{w})\times(i\mathrel{\epsilon}\nu_{w})\to\mathsf{Set}$ (an “indexed relation”) s.t. 2. (2)

$R_{i_{0}}\langle T_{1},T_{2}\rangle$ is inhabited, 3. (3)

whenever $R_{i}\langle T_{1},T_{2}\rangle$ is inhabited, we have

• •

$a_{1}\equiv a_{2}$,

• •

for every $d_{1}:D(i,a_{1})$, the elements $f_{1}\,i[a_{1}/d_{1}]$ and $f_{2}\,i[a_{2}/d_{2}]$ are related by $R$,

where $\langle a_{1},f_{1}\rangle$ [resp. $\langle a_{2},f_{2}\rangle$] comes from the coalgebra structure \nu_{w}\subset\left\llbracket w\right\rrbracket\nu_{w} applied to $T_{1}$ [resp. $T_{2}$].

Expressing this formally is quite verbose as values need to be transported along equalities to have an appropriate type. For example, having $a_{1}\equiv a_{2}\in A(i)$ only entails that $D(i,a_{1})$ and $D(i,a_{2})$ are isomorphic, and thus, $d_{1}:D(i,a_{1})$ is not strictly speaking an element of $D(i,a_{2})$!

We noted on page 2.3 that categorically speaking, without hypotheses on the functor $F$, $\approx$ was not necessarily transitive. We have

Lemma 10**.**

If $w$ is a container indexed on $I$, then $\approx$ is an equivalence relation on any $i\mathrel{\epsilon}\nu_{w}$:

• •

for any $T:i\mathrel{\epsilon}\nu_{w}$, there is an element in $T\approx T$,

• •

for any $T_{1},T_{2}:i\mathrel{\epsilon}\nu_{w}$, there is a function in $(T_{1}\approx T_{2})\to(T_{2}\approx T_{1})$,

• •

for any $T_{1},T_{2},T_{3}:i\mathrel{\epsilon}\nu_{w}$, there is a function in $(T_{1}\approx T_{2})\to(T_{2}\approx T_{3})\to(T_{1}\approx T_{3})$.

Proof 3.5**.**

[Agda✓]* The result is intuitively obvious but while reflexivity is easy, proving transitivity (and to a lesser extent symmetry) in Agda is surprisingly tedious. Explaining the formal proof is probably pointless as it mostly consists of transporting elements along equalities back and forth.*

We will keep some of the bisimilarity proofs in the meta theory in order to simplify the arguments. The only consequence of the assumption from page 2.3 that we’ll need is the following.

Lemma 11**.**

Suppose that $f,g:i_{1}\mathrel{\epsilon}\nu_{w_{1}}\to i_{2}\mathrel{\epsilon}\nu_{w_{2}}$ are definable in type theory, then, to prove that $f\approx g$,121212i.e. $S\approx T\to f\,S\approx g\,T$ it is enough to show that $f\,T\approx g\,T$ for any $T:i_{1}\mathrel{\epsilon}\nu_{w_{1}}$.

Proof 3.6**.**

If $S\approx T$, we have $f\,S\approx f\,T\approx g\,T$ where the first bisimulation comes from the assumption $f\approx f$ from page 2.3 and the second bisimulation comes from the hypothesis of the lemma.

This makes proving $f\approx g$ simpler as we can replace the hypothesis $T_{1}\approx T_{2}$ by the stronger $T_{1}\equiv T_{2}$.

Weakly Terminal Coalgebras

We will have to show that some sets are isomorphic “up to bisimilarity”. To do that, we’ll use Lemma 5 by showing that the two sets are weakly terminal coalgebras for the same functor \left\llbracket w\right\rrbracket. (One of the sets will always be $\nu_{w}$, making half of this automatic.)

To show that $T:\mathsf{Pow}(I)$ is a weakly terminal coalgebra for \left\llbracket w\right\rrbracket, we have to define, mimicking the typing rules for coinductive types:

• •

\mathtt{elim}:T\subset\left\llbracket w\right\rrbracket(T),

• •

\mathtt{intro}:X\subset\left\llbracket w\right\rrbracket(X)\to X\subset T,

• •

\mathtt{comp}_{X,c,x,i}:\mathtt{elim}(\mathtt{intro}\,c\,i\,x)\equiv\left\llbracket w\right\rrbracket_{\mathtt{intro}\,c}i\,(c\,i\,x) whenever

• –

$X:\mathsf{Pow}(I)$, c:X\subset\left\llbracket w\right\rrbracket(X), $i:I$ and $x:i\mathrel{\epsilon}X$,

• –

\left\llbracket w\right\rrbracket_{\mathtt{intro}\,c}:\left\llbracket w\right\rrbracket(X)\subset\left\llbracket w\right\rrbracket(T) comes from Lemma 6.

By Lemma 5, we have

Corollary 12**.**

If $C$ is a weakly terminal coalgebra for \left\llbracket w\right\rrbracket, then there are functions $f:\nu_{w}\subset C$ and $g:C\subset\nu_{w}$ such that

[TABLE]

for any $T:i\mathrel{\epsilon}\nu_{w}$.

Proof 3.7**.**

[Agda✓]* This is the second point of Lemma 5, and it has been formalized in Agda.*

4. Simulations and Evaluation

4.1. Functions on Streams

Continuous function from $\mathtt{stream}(A)$ to $\mathtt{stream}(B)$ can be described by infinite, $A$-branching “decision trees” with two kinds of nodes: $\mathtt{input}$ and $\mathtt{output}_{b}$ with $b\in B$. The idea is that $f(s)=[b_{1},b_{2},\dots]$ if and only if the infinite branch corresponding to $s$ contains, in order, the nodes $\mathtt{output}_{b_{1}}$, $\mathtt{output}_{b_{2}}$, …, interspersed with $\mathtt{input}$ nodes. For that to be well defined, we need to guarantee that all infinite branches in the tree contain infinitely many $\mathtt{output}$ node, or equivalently, that no branch contains infinitely many consecutive $\mathtt{input}$ nodes.

Theorem 13** ([GHP09b]).**

The set of continuous functions from $\mathtt{stream}(A)$ to $\mathtt{stream}(B)$ is isomorphic to the set $\nu X.\mu Y.(B\times X)+(A\to Y)$.

The nested fixed points guarantee that along a branch, there can only be finitely many consecutive input nodes:

• •

$\mu Y.\,(B\times X)+(A\to Y)$: well-founded $A$-branching trees with leafs in $B\times X$, i.e. consisting of an $\mathtt{output}_{b}$ node and an element of $X$,

• •

$\nu X.\cdots$ the element in $X$ at each leaf for the well-founded trees is another such well-founded tree, ad infinitum.

We can evaluate each such tree into a continuous function, a process colloquially referred to as “stream eating”: we consume the elements of the stream to follow a branch in the infinite tree, and output $b$ (an element of the result) whenever we find an $\mathtt{output}_{b}$ node.131313The converse mechanism, of converting a function into process into a tree cannot be defined in type theory, see the discussion on page Thoughts about Completeness.

Our aim is to extend Theorem 13 to coinductive types of the form $i\mathrel{\epsilon}\nu_{w^{\bot}}$. The problem is doing so in a type-theoretic manner and even the case of dependent streams (where the type of an element may depend on the values of the previous elements) is not trivial. Retrospectively, the difficulty was that there are two generalizations of streams:

• •

adding states: we consider dependent streams instead of streams;

• •

adding branching: we consider trees instead of streams.

Both cases required the introduction of states and branching, making those seemingly simpler cases as hard as the general one.

4.2. Linear Simulations as Transducers

We are going to define a notion of “transducer” that can explore some branch of its input and produce some output along the way. Such notions have already been considered as natural notions of morphisms between dependent containers: linear simulations [Hyv14a] and general simulations [HH06]. These notions generalize morphisms as representations of pointwise inclusions \left\llbracket w_{1}\right\rrbracket\subset\left\llbracket w_{2}\right\rrbracket (called cartesian strong natural transformations), which only make sense for containers with the same index set [GK13, GH03, AM09].

A transducer from type $i_{1}\mathrel{\epsilon}\nu_{w_{1}^{\bot}}$ to type $i_{2}\mathrel{\epsilon}\nu_{w_{2}^{\bot}}$ works as follows: given an argument (input) in $i_{1}\mathrel{\epsilon}\nu_{w_{1}^{\bot}}$, morally of the form

[TABLE]

it must produce (output) an object of the form

[TABLE]

In other words, the transducer

• •

consumes $b$ (they are given by the environment when constructing the result) and $d$ (they may be produced internally by the input),

• •

produces $e$ (as part of the output) and $a$ (to be used internally by feeding them to the input).

Graphically, the transducer “plugs into” the input, producing the output:

[TABLE]

A very simple kind of transducer works as follows:

1. (1)

when given some $b_{0}$, 2. (2)

it produces an $a_{0}$ and feeds it to its argument, 3. (3)

it receives a $d_{0}$ from its argument, 4. (4)

and produces an $e_{0}$ for its result. 5. (5)

It starts again at step (1) possibly in a different internal state.

The resulting interface is of the form

[TABLE]

This intuition is captured by the following definition. {defi} Let $w_{1}=\textlangle A_{1},D_{1},n_{1}\textrangle$ and $w_{2}=\textlangle A_{2},D_{2},n_{2}\textrangle$ be indexed containers over $I_{1}$ and $I_{2}$ and let $R:\mathsf{Pow}(I_{1}\times I_{2})$ be a relation between states. We say that $R$ is a linear simulation from $w_{1}$ to $w_{2}$ if it comes with a proof:

[TABLE]

We write $(R,\rho):w_{1}\multimap w_{2}$, but usually leave the $\rho$ implicit and write $R:w_{1}\multimap w_{2}$.

We will not need this fact in the present paper, but this notion of simulation enjoys a strong universal property. It arises as the adjoint of a very natural tensor product [Hyv14a] (see also the discussion on page Internal Simulations).

To justify the fact that this can serve as a transducer, we need to “evaluate” a simulation on elements of $i\mathrel{\epsilon}\nu_{w_{1}^{\bot}}$.

Lemma 14**.**

Let $w_{1}=\textlangle A_{1},D_{1},n_{1}\textrangle$ and $w_{2}=\textlangle A_{2},D_{2},n_{2}\textrangle$ be indexed containers over $I_{1}$ and $I_{2}$, and $(R,\rho):w_{1}\multimap w_{2}$. We have a function

[TABLE]

Proof 4.1**.**

[Agda✓]* This amounts to unfolding the simulation as a linear transducer. The main point in the Agda proof is to show that the predicate $\nu_{w_{1}^{\bot}}\between R^{\sim}(i_{2})$ is a coalgebra for \left\llbracket w_{2}^{\bot}\right\rrbracket.*

The next lemma shows that this notion of simulation gives an appropriate notion of morphism between indexed containers.

Lemma 15**.**

We have:

• •

the identity type on $I$ is a linear simulation from any $w$ over $I$ to itself,

• •

if $R$ is a linear simulation from $w_{1}$ to $w_{2}$, and if $S$ is a linear simulation from $w_{2}$ to $w_{3}$, then $S\circ R$ is a linear simulation from $w_{1}$ to $w_{3}$, where $S\circ R$ is the relational composition of $R$ and $S$:

[TABLE]

Proof 4.2** (Proof).**

[Agda✓]* That the identity type is a linear simulation is straightforward. Composing simulation amounts to extracting the functions $a_{1}\mapsto a_{2}$ and $d_{2}\mapsto d_{1}$ from the simulations, and composing them.*

Note that composition of simulations is only associative up to associativity of relational composition (pullback of spans) so that a quotient is needed to turn indexed containers into a category [Hyv14a]. What is nice is that composition of simulations corresponds to composition of their evaluations, up to bisimilarity.

Lemma 16**.**

If $w_{1}$, $w_{2}$ and $w_{3}$ are containers indexed on $I_{1}$, $I_{2}$ and $I_{3}$, and if $R:w_{1}\multimap w_{2}$ and $S:w_{2}\multimap w_{3}$, then we have

[TABLE]

where

• •

$i_{1}:I_{1}$, $i_{2}:I_{2}$, $i_{3}:I_{3}$,

• •

$r:R(i_{1},i_{2})$* and $s:S(i_{2},i_{3})$,*

• •

and thus, $\textlangle i_{2},\textlangle r,s\textrangle\textrangle:(S\circ R)(i_{1},i_{3})$.

Recall that for functions, $f\approx g$ means that for every input $T$ (here of type $i_{1}\mathrel{\epsilon}\nu_{w_{1}^{\bot}}$), we have “$f\,T\approx g\,T$, i.e. $f\,T$ is bisimilar to $g\,T$”.

Proof 4.3**.**

[Agda✓]* This is one instance where the direct, type theoretic proof of bisimilarity is possible, and not (too) tedious. With the transducer intuition in mind, this result is natural: starting from some $a_{3}:A_{1}(i_{3})$, we can either*

• •

transform it to $a_{2}:A_{2}(i_{2})$ (with the simulation from $w_{2}$ to $w_{3}$) and then to $a_{1}:A_{1}(i_{1})$ (with the simulation from $w_{1}$ to $w_{2}$),

• •

or transform it directly to $a_{1}:A(i_{1})$ (with the composition of the two simulations).

Because composition is precisely defined by composing the functions making the simulations, the two transformations are obviously equal. (The Agda proof is messier than that but amounts to the same thing.)

Note that because of Lemma 11, the Agda proof only needs to show that $(\mathrm{eval}_{S}\circ\mathrm{eval}_{R})\,T$ is bisimilar to $\mathrm{eval}_{S\circ R}\,T$.

4.3. General Simulations

As far as representing functions from $i_{1}\mathrel{\epsilon}\nu_{w_{1}^{\bot}}$ to $i_{2}\mathrel{\epsilon}\nu_{w_{2}^{\bot}}$, linear simulation are not very powerful. For streams, the first $n$ elements of the result may depend at most on the first $n$ elements of the input! Here is a typical continuous function that cannot be represented by a linear simulation. Given a stream $s$ of natural numbers, look at the head of $s$:

• •

if it is [math], output [math] and start again with the tail of the stream,

• •

if it is $n>0$, remove the next $n$ element of the stream, output their sum, and start again.

For example, on the stream $[0,1,2,3,4,5,6,\dots]$, the function outputs

[TABLE]

We can generalize transducers by allowing them to work in the following manner.

1. (1)

When given some $b_{0}$, 2. (2)

they produce an $a_{0}$ and feed it to their argument, 3. (3)

they receive a $d_{0}$ from their argument, 4. (4)

and either go back to step (2) or produce an $e_{0}$ (output) for their result, 5. (5)

start again at step (1)…

In other words, steps (2) and (3) can occur several times in a row. We can even allow the transducer to go directly from step (1) to step (4), bypassing steps (2) and (3) entirely. Of course steps (3) and (4) should never happen infinitely many times consecutively. {defi} Let $w_{1}$ and $w_{2}$ be indexed containers over $I_{1}$ and $I_{2}$, let $R:\mathsf{Pow}(I_{1}\times I_{2})$ be a relation between states; we say that $R$ is a general simulation from $w_{1}$ to $w_{2}$ if it is a linear simulation from $w_{1}^{\ast}$ to $w_{2}$.

In other words, $\langle R,\rho\rangle$ is a general simulation from $\textlangle A_{1},D_{1},n_{1}\textrangle$ to $\textlangle A_{2},D_{2},n_{2}\textrangle$ if

[TABLE]

Thanks to Lemma 14, such a simulation automatically gives rise to a function from $\nu_{w_{1}^{\ast\bot}}$ to $\nu_{w_{2}^{\bot}}$. Fortunately, $\nu_{w_{1}^{\ast\bot}}$ is, up to bisimulation, isomorphic to $\nu_{w_{1}^{\bot}}$.

Lemma 17**.**

$\nu_{w^{\ast\bot}}$* is a weakly terminal coalgebra for \left\llbracket w^{\bot}\right\rrbracket.*

Proof 4.4**.**

[Agda✓]* From an element of $i\mathrel{\epsilon}\nu_{w^{\ast\bot}}$ we can use the elimination rule and extract a member of \left(\big{.}\Pi\,\alpha:A^{\ast}(i)\right)\,{}\left(\big{.}\Sigma\,\delta:D^{\ast}(i,\alpha)\right)\,{}i[\alpha/\delta]\nu_{w^{\ast\bot}}. Given some $a:A(i)$, we instantiate $\alpha$ to $\mathtt{Node}(a,(\lambda\,d:D(i,a))\,{}\mathtt{Leaf}):A^{\ast}(i)$ (a single $a$, followed by nothing), and its responses are just responses to $a$. This produces an element of \left(\big{.}\Pi\,a:A(i)\right)\,{}\left(\big{.}\Sigma\,d:D(i,a)\right)\,{}i[a/d]\mathrel{\epsilon}\nu_{w^{\ast\bot}}, i.e. an element of i\mathrel{\epsilon}\left\llbracket w^{\bot}\right\rrbracket(\nu_{w^{\ast\bot}}). We’ve just shown that \nu_{w^{\ast\bot}}\subset\left\llbracket w^{\bot}\right\rrbracket\nu_{w^{\ast\bot}}. We refer to the Agda code for the rest of the proof.*

Corollary 18**.**

$\nu_{w^{\ast\bot}}$* and $\nu_{w^{\bot}}$ are isomorphic up to bisimulation:*

[TABLE]

Proof 4.5**.**

This is a direct consequence of Lemma 5.

By composing the function $\nu_{w^{\bot}}\subset\nu_{w^{\ast\bot}}$ with the evaluation of linear simulations (Lemma 14), we get an evaluation function for general simulations.

Corollary 19**.**

Let $w_{1}=\textlangle A_{1},D_{1},n_{1}\textrangle$ and $w_{2}=\textlangle A_{2},D_{2},n_{2}\textrangle$ be indexed containers over $I$ and $I_{2}$, and $(R,\rho):w^{\ast}\multimap w_{2}$. We have a function

[TABLE]

Sidenote on formal topology

When evaluating a general simulation $R:w_{1}^{\ast}\multimap w_{2}$ directly (i.e. not relying on Corollary 18), we need to compute an element of $i_{2}\mathrel{\epsilon}\nu_{w_{2}^{\bot}}$ from

• •

a state $i_{1}:I_{1}$ and a state $i_{2}:I_{2}$,

• •

an element $r:R(i_{1},i_{2})$,

• •

an element $T_{1}:i_{1}\mathrel{\epsilon}\nu_{w_{1}^{\bot}}$.

We then need to find, for each branch $a_{2}:A_{2}(i_{2})$, a corresponding $d_{2}:D_{2}(i_{2},a_{2})$ and a way to continue the computation. Given $a_{2}$, by the general simulation property, we can compute an element of

[TABLE]

which can be rewritten as

[TABLE]

The crucial first step is matching the well-founded tree $\alpha_{1}$ with the infinite tree $T_{1}$. This can be done with

Lemma 20**.**

Let $I:\mathsf{Set}$, and $w$ an indexed container over $I$, and $X$ a predicate over $I$. The type $w^{\ast}(X)\between\nu_{w^{\bot}}\to X\between\nu_{w^{\bot}}$ is inhabited.

Proof 4.6**.**

[Agda✓]* By matching dual quantifiers coming from $i\mathrel{\epsilon}w^{\ast}(X)$ and $i\mathrel{\epsilon}\nu_{w^{\bot}}$, we get an alternating sequence of moves $a_{i}$ and counter moves $d_{i}$ reaching a final state $i_{f}$ in $X$, together with a infinite tree in $i_{f}\mathrel{\epsilon}\nu_{w^{\bot}}$. More formally, suppose $w^{\ast}(X)\between\nu_{w^{\bot}}$ is inhabited, i.e., that we have $i:I$, $\langle\alpha,f\rangle:i\mathrel{\epsilon}w^{\ast}(X)$ and a (non-well-founded) tree $T$ in $i\mathrel{\epsilon}\nu_{w^{\bot}}$. We examine $\alpha$:*

• •

$\alpha=\mathtt{Leaf}(i)$: we have $f\,\star:i\mathrel{\epsilon}X$, in which case $X\between\nu_{w^{\bot}}$ is inhabited.

• •

$\alpha=\mathtt{Node}(a,k)$: where k:\left(\big{.}\Pi\,d\right)\,{}i[a/d]\mathrel{\epsilon}w^{\ast}(X). We can apply $\nu_{\mathrm{elim}}$ to  $T:i\mathrel{\epsilon}\nu_{w^{\bot}}$ to obtain a function in \left(\big{.}\Pi\,a\right)\,{}\left(\big{.}\Sigma\,d\right)\,{}i[a/d]\mathrel{\epsilon}\nu_{w^{\bot}}. Applying that function to $a:A(i)$, we get $d:D(i,a)$ s.t.

• –

$i[a/d]\mathrel{\epsilon}\nu_{w^{\bot}}$,

• –

$k\,d:i[a/d]\mathrel{\epsilon}w^{\ast}(X)$.

This pair inhabits $w^{\ast}(X)\between\nu_{w^{\bot}}$, and by induction hypothesis, yields an inhabitant of $X\between\nu_{w^{\bot}}$.

This formula is at the heart of formal topology, where it is called “monotonicity” [CSSV03]. There, i\mathrel{\epsilon}\left\llbracket w^{\ast}\right\rrbracket(U) is read “the basic open $i$ is covered by $U$” (written $i\triangleleft U$), and $i\mathrel{\epsilon}\nu_{w^{\bot}}$ is read “the basic open $i$ contains a point” and is written $i\mathrel{\epsilon}\mathsf{Pos}$.

Applied to the present situation with X=(\lambda\,i:I_{1})\,{}\left(\big{.}\Sigma\,d_{2}:D_{2}(i_{2},a_{2})\right)\,{}R\big{(}i,i_{2}[a_{2}/d_{2}]\big{)}, we get an element of $X\between\nu_{w_{2}^{\bot}}$, which is precisely given by

• •

a state $i_{1}:I_{1}$,

• •

a pair $\langle d_{2},r\rangle$ with $d_{2}:D_{2}(i_{2},a_{2})$ and $r:R(i_{1},i_{2}[a_{2}/d_{2}])$,

• •

an element $T_{1}:\nu_{w_{1}^{\bot}}$.

In other words, we get the sought after $d_{2}$ (giving the first element of the $a_{2}$ branch), together with enough data to continue the computation.

4.4. The Free Monad Construction as a Comonad

Composition of general simulations does not follow directly from composition of linear simulations because there is a mismatch on the middle container: composing $R:w_{1}^{\ast}\multimap w_{2}$ and $S:w_{2}^{\ast}\multimap w_{3}$ to get a simulation from $w_{1}^{\ast}$ to $w_{3}$ is not obvious. Fortunately, the operation $w\mapsto w^{\ast}$ lifts to a comonad, and the composition corresponds to composition in its (co)Kleisli category.

Proposition 21**.**

Let $\mathbb{C}$ be a locally cartesian closed category. The operation $P\mapsto P^{\ast}$ lifts to a monad on the category of polynomial functors over $I$ with cartesian natural transformations between them.

Proof 4.7**.**

[Agda✗]* The operation $P\mapsto P^{\ast}$ goes from $\mathsf{End}(\mathbb{C}/I)$, the category of polynomial endofunctors on $\mathbb{C}/I$ to $\mathsf{Mnd}(\mathbb{C}/I)$, the category of (polynomial) monads over $\mathbb{C}/I$ [GH03, GK13]. We write $\mathsf{Nat}(F,G)$ for natural transformations from $F$ to $G$, and $\mathsf{Nat}_{\mathsf{Mnd}}(F,G)$ for those transformations that respect the monad structures of $F$ and $G$. Writing $F{\mathtt{-}}\mathsf{alg}$ for the category of $F$-algebras, and $F{\mathtt{-}}\mathsf{Alg}$ (when $F$ is a monad) for the category of $F$-algebras that respect the monad operations, we have*

[TABLE]

This shows that ${\texttt{\char 95\relax}}^{\ast}$ is left adjoint to the forgetful functor $\mathcal{U}:\mathsf{Mnd}(\mathbb{C}/I)\to\mathsf{End}(\mathbb{C}/I)$, and makes the composition $\mathcal{U}{\texttt{\char 95\relax}}^{\ast}$ a monad. It only remains to show that the monad operations are strong cartesian transformations.

Since strong natural transformations from \left\llbracket w_{1}\right\rrbracket to \left\llbracket w_{2}\right\rrbracket correspond exactly to linear simulations $(\equiv,\rho):w_{2}\multimap w_{1}$ [GK13, Hyv14b], it is enough to define the monad operations as simulations:

• •

$(\equiv,\varepsilon_{w}):w^{\ast}\multimap w$**

• •

and $(\equiv,\delta_{w}):w^{\ast}\multimap w^{\ast\ast}$

Those constructions are relatively straightforward in Agda: the first operation corresponds to embedding a single action $a:A(i)$ into $A^{\ast}(i)$ as $\mathtt{Node}(a,(\lambda\,d:D(i,a))\,{}\mathtt{Leaf})$. A direct definition of $\delta_{w}$ is done by induction and can be found in the Agda code. Semantically speaking, it can be derived from Lemma 9:

[TABLE]

What makes this lemma interesting is that the constructions themselves are easy to define in Agda without identity types. A purely type theoretic proof that the constructions satisfies the monad laws could not be completed in Agda, because the overhead of reasoning with equality on dependent structures is very tedious. The categorical proof guarantees that it holds in all models for extensional type theory which is good enough for us.

Because of the reversal (strong natural transformation from $w_{1}$ to $w_{2}$ are equivalent to identity linear simulations from $w_{2}$ to $w_{1}$), this translates to “$w\mapsto w^{\ast}$ lifts to a comonad in the category of indexed containers with linear simulations”.

Corollary 22**.**

The operation $w\mapsto w^{*}$ lifts to a comonad in the category of indexed containers over $I$ and linear simulations.

4.5. Composition of General Simulations

Recall that a comonad may be given in triple form with the following data:

• •

a natural transformation $\varepsilon_{w}:w^{\ast}\multimap w$,

• •

a “cobinding” operation taking $R:w_{1}^{\ast}\multimap w_{2}$ to $R^{\sharp}:w_{1}^{\ast}\multimap w_{2}^{\ast}$ (defined as $R^{\ast}\circ\delta_{w_{1}}$),

satisfying the following laws:

1. (1)

$\varepsilon_{w}^{\sharp}=\mathrm{id}_{w^{\ast}}$, 2. (2)

$\varepsilon_{w_{2}}\circ R^{\sharp}=R$ for $R:w_{1}^{\ast}\multimap w_{2}$, 3. (3)

$(S\circ R^{\sharp})^{\sharp}=S^{\sharp}\circ R^{\sharp}$ for $R:w_{1}\multimap w_{2}^{\ast}$ and $S:w_{2}^{\ast}\multimap w_{3}^{\ast}$.

We can now define {defi} If $R:w_{1}^{\ast}\multimap w_{2}$ and $S:w_{2}^{\ast}\multimap w_{3}$, define $S\bullet R$ with $S\circ R^{\sharp}$.

The comonad laws are then enough to prove that composition of general simulations corresponds to composition of their evaluations.

Proposition 23**.**

Let $w_{1},w_{2},w_{3}$ be containers indexed on $I_{1}$, $I_{2}$ and $I_{3}$, with $R:w_{1}^{\ast}\multimap w_{2}$ and $S:w_{2}^{\ast}\multimap w_{3}$, then we have

[TABLE]

where

• •

$i_{1}:I_{1}$, $i_{2}:I_{2}$, $i_{3}:I_{3}$,

• •

$s:S(i_{2},i_{3})$* and $t:T(i_{2},i_{3})$,*

• •

and thus, $\textlangle i_{2},\textlangle s,t\textrangle\textrangle:(T\bullet S)(i_{1},i_{3})$.

Proof 4.8**.**

[Agda✗]* Because $\nu_{w_{2}^{\ast\bot}}$ is a weakly terminal algebra for \left\llbracket w_{2}^{\bot}\right\rrbracket, by Lemma 5, we have a pair of morphisms $f_{2}:i_{2}\mathrel{\epsilon}\nu_{w_{2}^{\bot}}\to i_{2}\mathrel{\epsilon}\nu_{w_{2}^{\ast\bot}}$ and $g_{2}:i_{2}\mathrel{\epsilon}\nu_{w_{2}^{\ast\bot}}\to i_{2}\mathrel{\epsilon}\nu_{w_{2}^{\bot}}$ such that $f_{2}g_{2}\approx\mathrm{id}$ and $g_{2}f_{2}\approx\mathrm{id}$.*

Expanding the definitions (and omitting all non-essential parameters, except for the first and last lines), we have:

[TABLE]

The only missing part $(*)$ is showing that $\mathrm{eval}_{\varepsilon_{w_{2}}}\approx g_{2}$ where $g_{2}:i_{2}\mathrel{\epsilon}\nu_{w_{2}^{\ast\bot}}\to i_{2}\mathrel{\epsilon}\nu_{w_{2}^{\bot}}$ is the mediating morphism coming from the \left\llbracket w_{2}^{\bot}\right\rrbracket coalgebra structure of $i_{2}\mathrel{\epsilon}\nu_{w_{2}^{\ast\bot}}$. This was formally proved in Agda. (The reason is essentially that both morphisms are, up-to bisimilarity, the identity.)

Note that this proof is hybrid with a formal part proved in Agda, and a pen and paper proof.

5. Layering and Infinite Trees

General simulations allow to represent all computable (continuous) functions on streams: for a given piece of the output, we only need to look at finitely many elements of the stream. A general simulation does that by asking as many elements as it needs. However, for branching structures, general simulations are not enough: general simulations explore their arguments along a single branch $a_{1}/d_{1},a_{2}/d_{2},\dots$. For example, the function summing each layer of a binary tree to form a stream is not representable by a general simulation:

[TABLE]

We want a notion of “backtracking” transducer that can explore several branches. Describing such a transducer is difficult in type theory if we try to refrain from using equality.

5.1. Layering

To give a simulation access to several branches, we are going to replace a branching structure by the stream of its “layers”. Then, a simulation will be able to access as many layers as it needs to get information about as many branches as it needs.

{defi}

Given an indexed container $w=\textlangle A,D,n\textrangle$ over $I:\mathsf{Set}$ we define an indexed container $w^{\sharp}=\langle A^{\sharp},D^{\sharp},n^{\sharp}\rangle$ on $I$ by induction-recursion on $\mathsf{Fam}(I)$.

• •

given $i:I$, the index set $A^{\sharp}(i):\mathsf{Set}$ is defined with

[TABLE]

• •

for $\alpha:A^{\sharp}(i)$, the family \big{\langle}D^{\sharp}(i,\alpha):\mathsf{Set},n^{\sharp}\,i\,\alpha:D^{\sharp}(i,\alpha)\to I\big{\rangle} is defined with

• –

$D^{\sharp}(i,\mathtt{Leaf})={\bf 1}$ and D^{\sharp}(i,\alpha\triangleleft l)=\left(\big{.}\Sigma\,\beta:D^{\sharp}(i,\alpha)\right)\,{}D\big{(}n^{\sharp}\,i\,\alpha\,\beta,l\,\beta\big{)},

• –

$n^{\sharp}\,i\,\mathtt{Leaf}\,\star=i$ and $n^{\sharp}\,i\,(\alpha\triangleleft l)\,\textlangle\beta,d\textrangle=n\ (n^{\sharp}\,i\,\alpha\,\beta)\ (l\,\beta)\ d$.

The Agda definition looks like

mutual data A# : I → Set where Leaf : { i : I } → A# i $\triangleleft$ : {i : I} → (t : A# i) → ((b : D# i t) → A (n# t b)) → A# i

  D# : (i : I) → A# i → Set
  D# i Leaf = One
  D# i (t $\triangleleft$ l) = Σ (D# i t) (λ ds → D (n# t ds) (l ds))

  n# : {i : I} → (t : A# i) → D# i t → I
  n# {i} Leaf * = i
  n# {i} (t $\triangleleft$ l) ( ds , d ) = n {n# {i} t ds} (l ds) d

This definition is a direct extension of the operation appearing in previous work about continuous functions and (unindexed) containers [GHP09a]. It generalizes the example of complete binary trees as an inductive recursive definition from page 2.2 to arbitrary dependent $A$-labelled and $D$-branching trees. Given such a tree $\alpha:A^{\sharp}(i)$, $D^{\sharp}(i,\alpha)$ indexes the set of its terminal leaves. A new layer assigns a new element $a:A(\dots)$ at each leaf, and $\alpha\triangleleft l$ is the new, increased tree.

Of particular interest is the indexed container $w^{\bot\sharp}$. An element of $A^{\bot\sharp}(i)$ is a complete tree of finite depth where branching occurs at $A({\texttt{\char 95\relax}})$ and labels are chosen in $D({\texttt{\char 95\relax}},{\texttt{\char 95\relax}})$. In particular, an element of $D^{\bot\sharp}(i,\alpha)$ is a finite sequence of actions.

We can now construct a lopsided (angelic) indexed container from an arbitrary indexed container: {defi} Given $w$ a container indexed on $I$ and a fixed $i:I$, we define a new container $\langle\mskip-4.5mu\langle{w,i}\rangle\mskip-4.5mu\rangle$:

• •

$\langle\mskip-4.5mu\langle{w,i}\rangle\mskip-4.5mu\rangle$ is indexed on $A^{\sharp}(i)$,

• •

actions in state $\alpha:A^{\sharp}(i)$ are given by \left(\big{.}\Pi\,\beta:D^{\sharp}(i,\alpha)\right)\,{}A(n^{\sharp}\,i\,\alpha\,\beta), i.e., “layers” on top of $\alpha$,

• •

responses are trivial: there is only ever one possible response: $\star$,

• •

the next state after action $l$ in state $\alpha$ (and response $\star$) is $\alpha\triangleleft l$.

States of this new container record a complete tree of finite depth. Moreover, since it has trivial responses, an element of $\mathtt{Leaf}\mathrel{\epsilon}\nu_{\langle\mskip-4.5mu\langle{w,i}\rangle\mskip-4.5mu\rangle}$ is not very different from a (dependent) stream of layers, and so, from an infinite tree in $i\mathrel{\epsilon}\nu_{w}$. This is generalized and formalized in the next lemmas.

Lemma 24**.**

The predicate \left(\big{.}\Pi\,\beta:D^{\sharp}(i,\alpha)\right)\,{}(n^{\sharp}\,i\,\alpha\,\beta)\mathrel{\epsilon}\nu_{w},141414An element of \left(\big{.}\Pi\,\beta:D^{\sharp}(i,\alpha)\right)\,{}(n^{\sharp}\,i\,\alpha\,\beta)\mathrel{\epsilon}\nu_{w} is a way to extend the complete tree $\alpha$ of finite depth to a full infinite complete tree by appending an infinite tree at each leaf. depending on $\alpha:A^{\sharp}(i)$, is a weakly terminal coalgebra for \left\llbracket\langle\mskip-4.5mu\langle{w,i}\rangle\mskip-4.5mu\rangle\right\rrbracket.

Proof 5.1**.**

[Agda✓]* The proof corresponds to the above remark that an infinite tree is equivalently given by the infinite stream of its layers. It has been formalized in Agda.*

Corollary 25**.**

Given $\alpha:A^{\sharp}(i)$, there are functions

[TABLE]

that are, up to bisimulation, inverse to each other. In particular, there are functions

[TABLE]

such that $fg\approx\mathrm{id}$ and $gf\approx\mathrm{id}$.

Proof 5.2**.**

This is a direct consequence of Lemma 5.

As mentioned on page 3.3, lopsided containers are special because duality is essentially involutive, in the sense that $w$ and $w^{\bot\bot}$ are isomorphic:

• •

there are bijections $f_{i}$ between $A(i)$ and $A^{\bot\bot}(i)$,

• •

there is are bijections $g_{i,a}$ between $D(i,a)$ and $D^{\bot\bot}(i,f_{i}\,a)$,

• •

the next state functions are compatible with them: $n(i,a,d)\equiv n^{\bot\bot}(i,f_{i}\,a,g_{i,a}\,d)$.

Rather than developing this notion, we will only state and prove the only consequence we’ll need.

Lemma 26**.**

Suppose $w$ has trivial (singleton) reactions, then $\nu_{w}$ is a weakly terminal coalgebra for \left\llbracket w^{\bot\bot}\right\rrbracket.

Proof 5.3**.**

[Agda✓]**

Corollary 27**.**

There are function

[TABLE]

such that $\varphi\psi\approx\mathrm{id}$ and $\psi\varphi\approx\mathrm{id}$.

5.2. Continuous Functions

We now have everything we need. {defi} A layered simulation from $w_{1}$ to $w_{2}$ at states $i_{1}:I_{1}$ and $i_{2}:I_{2}$ is a simulation from $\langle\mskip-4.5mu\langle{w_{1}^{\bot},i_{1}}\rangle\mskip-4.5mu\rangle^{\bot}$ to $\langle\mskip-4.5mu\langle{w_{2}^{\bot},i_{2}}\rangle\mskip-4.5mu\rangle^{\bot}$. A general layered simulation is a simulation from $\langle\mskip-4.5mu\langle{w_{1}^{\bot},i_{1}}\rangle\mskip-4.5mu\rangle^{\bot\ast}$ to $\langle\mskip-4.5mu\langle{w_{2}^{\bot},i_{2}}\rangle\mskip-4.5mu\rangle^{\bot}$.

Theorem 28**.**

For every general layered simulation $R:\langle\mskip-4.5mu\langle{w_{1}^{\bot},i_{1}}\rangle\mskip-4.5mu\rangle^{\bot\ast}\multimap\langle\mskip-4.5mu\langle{w_{2}^{\bot},i_{2}}\rangle\mskip-4.5mu\rangle^{\bot}$ there is an evaluation function

[TABLE]

Proof 5.4**.**

Given $r:R(\mathtt{Leaf},\mathtt{Leaf})$, we have

[TABLE]

Theorem 29**.**

If composition of general layered simulations is defined as general composition of layered simulations, then evaluation of a composition is bisimilar to the composition of their evaluations.

Proof 5.5**.**

The composition of evaluations gives

[TABLE]

Since $f_{2}g_{2}\approx\mathrm{id}$ (Corollary 25) and $\varphi_{2}\psi_{2}\approx\mathrm{id}$ (Corollary 27), this whole composition is bisimilar to

[TABLE]

and thus, by Proposition 23, to

[TABLE]

This corresponds to evaluation of $S\bullet R:\langle\mskip-4.5mu\langle{w_{1}^{\bot},i_{1}}\rangle\mskip-4.5mu\rangle^{\bot\ast}\multimap\langle\mskip-4.5mu\langle{w_{2}^{\bot},i_{2}}\rangle\mskip-4.5mu\rangle^{\bot}$ as defined in Theorem 28.

Concluding Remarks

Internal Simulations

It is possible to internalize the notion of linear simulation by defining an indexed container $w_{1}\multimap w_{2}$ on $I_{1}\times I_{2}$ satisfying “$R$ is a linear simulation from $w_{1}$ to $w_{2}$ iff R\subset\left\llbracket w_{1}\multimap w_{2}\right\rrbracket(R)” [HH06, Hyv14a]. {defi} If $w_{1}$ and $w_{2}$ are containers indexed on $I_{1}$ and $I_{2}$, then the container $w_{1}\multimap w_{2}$, indexed on $I_{1}\times I_{2}$ is defined by

• •

\Big{.}A\big{(}\langle i_{1},i_{2}\rangle\big{)}=\left(\big{.}\Sigma\,f:A_{2}(i_{2})\to A_{1}(i_{1})\right)\,{}\left(\big{.}\Pi\,a_{2}:A_{2}(i_{2})\right)\,{}D_{1}\big{(}i_{1},f(a_{2})\big{)}\to D_{2}(i_{2},a_{2}),

• •

\Big{.}D\big{(}\langle i_{1},i_{2}\rangle,\langle f,\varphi\rangle\big{)}=\left(\big{.}\Sigma\,a_{2}:A_{2}(i_{2})\right)\,{}D_{1}\big{(}i_{1},{f(a_{2})}\big{)},

• •

\Big{.}n\,\langle i_{1},i_{2}\rangle\,\langle f,\varphi\rangle\,\langle a_{2},d_{1}\rangle=\big{\langle}i_{1}[f(a_{2})/d_{1}],i_{2}[a_{2}/\varphi(a_{2})(d_{1})]\big{\rangle}.

The resulting structure is nicer in the opposite category because then, $w_{1}\multimap w_{2}$ generalizes duality (definition 3.2) in the sense that $w^{\bot}$ is the same as $w\multimap\bot$, where $\bot$ is the trivial container (indexed on $I=\{\star\}$, with a single action and a single reaction). Moreover, this definition is universal in the following sense. Define the “synchronous tensor” $w_{1}\otimes w_{2}$ of containers, indexed with the cartesian product of states with

• •

\big{(}A_{1}\otimes A_{2}\big{)}\big{(}\langle i_{1},i_{2}\rangle\big{)}=A_{1}(i_{1})\times A_{2}(i_{2}),

• •

\big{(}D_{1}\otimes D_{2}\big{)}\big{(}\langle i_{1},i_{2}\rangle,\langle a_{1},a_{2}\rangle\big{)}=D_{1}(i_{1},a_{1})\times D_{2}(i_{2},a_{2}),

• •

\big{(}n_{1}\otimes n_{2}\big{)}\ \langle i_{1},i_{2}\rangle\ \langle a_{1},a_{2}\rangle\ \langle d_{1},d_{2}\rangle=\langle i_{1}[a_{1}/d_{1}],i_{2}[a_{2}/d_{2}]\rangle.

One can show [Hyv14a, Hyv14b] that $\multimap$ is right-adjoint to $\otimes$. Linear simulations thus give rise to a symmetric monoidal closed category.

That a simulation $R:w_{1}\multimap w_{2}$ is nothing more than a coalgebra for \left\llbracket w_{1}\multimap w_{2}\right\rrbracket means that, up to bisimilarity, they can be seen as elements of $\nu_{w_{1}\multimap w_{2}}$. However, even if $w_{1}$ and $w_{2}$ are finitary, $w_{1}^{\ast}$ or $\langle\mskip-4.5mu\langle{w_{1}^{\bot}}\rangle\mskip-4.5mu\rangle^{\ast}$ are not and we cannot iterate this construction to represent higher order continuous functions in this way.

Thoughts about Completeness

Stating and proving formally completeness of this representation is yet to be done. Even though all functions definable151515provided they pass the termination criterion in Agda are continuous (because they are computable), we need to define continuity as an Agda predicate. Looking at the simplest case of functions from streams to 2, we would need to transform some $f:\mathtt{stream}(X)\to{\bf 2}$ into a well-founded tree with branching given by $X$ and leaves in ${\bf 2}$. In order to do that, we need to know when a finite prefix of a stream gives enough information to decide what it maps to, that is, to know the “modulus of continuity” of the function, which is not definable in MLTT. To avoid a contradiction (the modulus is trivially computable from the tree representation), each continuous function needs to come with its modulus function.

The definition of “modulus of continuity” for elements of some $\nu_{w^{\bot}}(i)$ is not easy, and the simplest is probably to use the exact same ideas that were developed: see a (finitary branching) coinductive tree as the stream of its layer.

That’s a preliminary step to be able to state completeness of the representation in Agda. This path does look neither very enlightening nor very interesting.

On a meta-theoretical level, completeness of the representation is much simpler:

1. (1)

Semantically, when interpreting all the constructions in the category of sets and functions, every function that is continuous for the “wild” topology from Section 1.3 is representable as a general layered simulation.161616Let’s stress the point again: proving such theorems in Agda is not possible, as there can be non-computable continuous functions. This would be an analogous to Theorem 13 and the proof would go as follows

• •

we generalize Theorem 13 to dependent streams (i.e. consider indexed containers with trivial actions) and show that in this case, any continuous function from $\nu_{w_{1}^{\bot}}(i_{1})$ to $\nu_{w_{2}^{\bot}}(i_{2})$ is represented by an element of $\nu_{w_{1}^{\ast}\multimap w_{2}}(i_{1},i_{2})$.

• •

we use Corollary 27 showing that any $\nu_{w^{\bot}}(i)$ (without restriction) is isomorphic to some $\nu_{w^{\prime\bot}}(j)$ where $w^{\prime}$ has trivial actions. 2. (2)

In particular, every function continuous for the natural topology (Section 1.2) between greatest fixed points of finitary indexed containers171717An indexed container is finitary if its sets of actions are finite. is thus representable as a general layered simulation. 3. (3)

If only the codomain is finitary, all continuous functions between fixed points of non-finitary containers are representable by simulations of the form $\langle\mskip-4.5mu\langle{w_{1}^{\bot},i_{1}}\rangle\mskip-4.5mu\rangle^{\bot\ast}\multimap w_{2}$. This is for example the case of the naturally continuous but non-wildly continuous function from page • ‣ 1.3. However, we do not know how to compose such simulations.

Notes about Formalization

Some proofs have not been formalized in Agda, most notably:

• •

the proof of Lemma 11 or of Assumption 2.3,

• •

the proof of Corollary 22.

We think the second holds in intensional type theory with function extensionality but were unable to complete the proof. As it stands, we only know it holds semantically by categorical reasoning. (It thus holds in extensional type theory.)

The situation is subtle with Lemma 11. It is possible it can be bypassed entirely. A direct proof of Corollary 25 was in fact checked in Agda (with the --with-K flag), but its complexity convinced us to base similar proofs on Lemma 11.

Enriching the type theory with stronger forms of equality may well simplify the development. Preliminary investigation showed that cubical type theory [CCHM17] allows to prove that bisimulation and (path) equality are identical. For readers with some knowledge about cubical Agda [VMA19], here is one way of defining bisimulation:181818Note that states are written $s\in S$ to avoid clashing with cubical Agda’s interval called $I$.

record ≈ {s : S} (T₁ T₂ : ν w s) : Type₀ where coinductive field root≈ : root T₁ ≡ root T₂ branch≈ : (s’ : S) (d₁ : D s (root T₁)) (q₁ : n s (root T₁) d₁ ≡ s’) (d₂ : D s (root T₂)) (q₂ : n s (root T₂) d₂ ≡ s’) (Pd : PathP (λ i → D s (root≈ i)) d₁ d₂) → (PathP (λ i → n s (root≈ i) (Pd i) ≡ s’) q₁ q₂) → (subst (ν w) q₁ (branch T₁ d₁)) ≈ (subst (ν w) q₂ (branch T₂ d₂))

This is much more streamlined than the definition in plain Agda!

It is then possible to prove the following:

[TABLE]

which makes all the bisimilarity proofs unnecessary.191919To be honest, the difficult part of this proof is due to Anders Mortberg and is part of cubical Agda’s standard library: Cubical/Codata/M/Bisimilarity.agda

Recall however all this is only needed to prove properties about the objects that are defined in plain Martin-Löf type theory without identity.

Acknowledgements

I really want to thank Peter Hancock for all the discussions that led to this paper. His knowledge of type theory and inductive-recursive definitions, together with his reluctance to give in to the temptation of equality are at the bottom of this work.