diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-24 17:01:29 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-24 17:01:29 +0000 |
| commit | abe9461e0dc194c160d97fee23a1646097a0c264 (patch) | |
| tree | 5ef1f5929e5ab037ac2c6880210517f05e90b7ca /src/Cfe/Language/Properties.agda | |
| parent | 11dddff1955a696538afbc1cfb604bbc640242a6 (diff) | |
Prove lemma 3.5 (7).
Diffstat (limited to 'src/Cfe/Language/Properties.agda')
| -rw-r--r-- | src/Cfe/Language/Properties.agda | 8 |
1 files changed, 7 insertions, 1 deletions
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 + } |