code for Lists

This commit is contained in:
wadler 2018-01-31 21:26:08 -02:00
parent 650610600f
commit 4df09d9b05

View file

@ -238,9 +238,9 @@ last combines the left inverse of `B ≲ A` with the equivalences of
the `to` and `fro` components from the two embeddings to obtain the `to` and `fro` components from the two embeddings to obtain
the right inverse of the isomorphism. the right inverse of the isomorphism.
## Tabular reasoning for encoding ## Tabular reasoning for embedding
We can also support tabular reasoning for encoding, We can also support tabular reasoning for embedding,
analogous to that used for isomorphism. analogous to that used for isomorphism.
\begin{code} \begin{code}