From abe9461e0dc194c160d97fee23a1646097a0c264 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 24 Mar 2021 17:01:29 +0000
Subject: Prove lemma 3.5 (7).

---
 src/Cfe/Language/Properties.agda | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'src/Cfe/Language/Properties.agda')

diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda
index b2630ce..756877c 100644
--- a/src/Cfe/Language/Properties.agda
+++ b/src/Cfe/Language/Properties.agda
@@ -13,7 +13,7 @@ open import Cfe.Language.Base over
 open import Data.List
 open import Data.List.Relation.Binary.Equality.Setoid over
 open import Function
-open import Level
+open import Level hiding (Lift)
 
 ≈-refl : ∀ {a} → Reflexive (_≈_ {a})
 ≈-refl {x = A} = record
@@ -94,3 +94,9 @@ setoid a = record { isEquivalence = ≈-isEquivalence {a} }
 
 poset : ∀ a → Poset (c ⊔ ℓ ⊔ suc a) (c ⊔ ℓ ⊔ a) (c ⊔ a)
 poset a = record { isPartialOrder = ≤-isPartialOrder a }
+
+lift-cong : ∀ {a} b (L : Language a) → Lift b L ≈ L
+lift-cong b L = record
+  { f = lower
+  ; f⁻¹ = lift
+  }
-- 
cgit v1.2.3