From 4df09d9b05c6734c591cdebf061bad333c658e44 Mon Sep 17 00:00:00 2001 From: wadler Date: Wed, 31 Jan 2018 21:26:08 -0200 Subject: [PATCH] code for Lists --- src/Isomorphism.lagda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Isomorphism.lagda b/src/Isomorphism.lagda index a03f43d2..b64b4c76 100644 --- a/src/Isomorphism.lagda +++ b/src/Isomorphism.lagda @@ -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 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. \begin{code}