Summary edit

Licensing edit

I, the copyright holder of this work, release this work into the public domain. This applies worldwide. In some countries this may not be legally possible; if so: I grant anyone the right to use this work for any purpose, without any conditions, unless such conditions are required by law.

LaTeX source edit

\begin{diagram}
\N                                     & \rDashto^{\tt upFrom} & {\tt Stream}_\N \\
\dTo^{\langle 1_\N, {\tt succ}\rangle} &                       & \dTo_{\langle{\tt head}, {\tt tail}\rangle} \\
\N \times \N                           & \rTo                  & \N \times {\tt Stream}_\N
\end{diagram}