From ab662afac4d660b279b48bb54d8a26d48da40258 Mon Sep 17 00:00:00 2001
From: Pierre-Evariste Dagand <pierre-evariste.dagand@lip6.fr>
Date: Fri, 7 Feb 2020 09:22:50 +0100
Subject: [PATCH] Add conversion rule(!)

---
 agda/00-agda/Warmup.lagda.rst | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/agda/00-agda/Warmup.lagda.rst b/agda/00-agda/Warmup.lagda.rst
index 23fcacc..c35b4fd 100644
--- a/agda/00-agda/Warmup.lagda.rst
+++ b/agda/00-agda/Warmup.lagda.rst
@@ -132,6 +132,17 @@ of ``(a : A) × B``. Again, a sequence of Σ-types is written ``(a₁ :
 A₁)(a₂ : A₂)...(aₙ : Aₙ) × B``, dispensing with the intermediate
 products.
 
+Since computation can occur at the type-level, we have to consider
+types up to conversion:
+
+.. code-block:: none
+
+   Γ ⊢ t ∈ S
+   S ≡ T        
+   ---------
+   Γ ⊢ t ∈ T
+
+
 ************************************************
 Motivating example: evolution of a type-checker
 ************************************************
-- 
GitLab