From 650610600fbe2b465868dcb3a3858a51c1979b85 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Wed, 31 Jan 2018 16:57:11 -0200
Subject: [PATCH] added tabular reasoning for embedding

---
 src/Isomorphism.lagda | 28 ++++++++++++++++++++++++++--
 src/Logic.lagda       |  2 +-
 2 files changed, 27 insertions(+), 3 deletions(-)

diff --git a/src/Isomorphism.lagda b/src/Isomorphism.lagda
index c1cc26ca..a03f43d2 100644
--- a/src/Isomorphism.lagda
+++ b/src/Isomorphism.lagda
@@ -195,8 +195,8 @@ right inverses.
     ; invˡ = λ x → refl
     } 
 
-≲-tran : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
-≲-tran A≲B B≲C =
+≲-trans : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
+≲-trans A≲B B≲C =
   record
     { to = λ x → to B≲C (to A≲B x)
     ; fro = λ y → fro A≲B (fro B≲C y)
@@ -238,5 +238,29 @@ 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
+
+We can also support tabular reasoning for encoding,
+analogous to that used for isomorphism.
+
+\begin{code}
+module ≲-Reasoning where
+
+  infix  1 ≲-begin_
+  infixr 2 _≲⟨_⟩_
+  infix  3 _≲-∎
+
+  ≲-begin_ : ∀ {A B : Set} → A ≲ B → A ≲ B
+  ≲-begin A≲B = A≲B
+
+  _≲⟨_⟩_ : ∀ (A : Set) {B C : Set} → A ≲ B → B ≲ C → A ≲ C
+  A ≲⟨ A≲B ⟩ B≲C = ≲-trans A≲B B≲C
+
+  _≲-∎ : ∀ (A : Set) → A ≲ A
+  A ≲-∎ = ≲-refl
+
+open ≲-Reasoning
+\end{code}
+
 
 
diff --git a/src/Logic.lagda b/src/Logic.lagda
index 779bb5b5..21bc32bb 100644
--- a/src/Logic.lagda
+++ b/src/Logic.lagda
@@ -503,7 +503,7 @@ commutativity of sum and left identity.
   ≃-∎
 \end{code}
 Here we have used tabular reasoning for isomorphism,
-analogous to than used for equivalence.
+analogous to that used for equivalence.
 
 
 ## Implication is function