Begin soundness proof.

2 files changed, 19 insertions, 0 deletions

diff --git a/src/Cfe/Type/Construct/Lift.agda b/src/Cfe/Type/Construct/Lift.agda
index 9f8e439..e26359f 100644
--- a/src/Cfe/Type/Construct/Lift.agda
+++ b/src/Cfe/Type/Construct/Lift.agda
@@ -7,6 +7,7 @@ module Cfe.Type.Construct.Lift
   where
 
 open import Cfe.Type over
+open import Cfe.Language over using (Language)
 open import Level as L hiding (Lift)
 open import Function
 
@@ -18,3 +19,12 @@ Lift fℓ₂ lℓ₂ τ = record
   }
   where
   module τ = Type τ
+
+⊨-liftʳ : ∀ {a fℓ₁ lℓ₁} {L : Language a} {τ : Type fℓ₁ lℓ₁} fℓ₂ lℓ₂ → L ⊨ τ → L ⊨ Lift fℓ₂ lℓ₂ τ
+⊨-liftʳ _ _ L⊨τ = record
+  { n⇒n = n⇒n
+  ; f⇒f = lift ∘ f⇒f
+  ; l⇒l = lift ∘ l⇒l
+  }
+  where
+  open _⊨_ L⊨τ
diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda
index e9ed634..2554ddd 100644
--- a/src/Cfe/Type/Properties.agda
+++ b/src/Cfe/Type/Properties.agda
@@ -67,6 +67,15 @@ L⊨τ+¬N⇒ε∉L {L = L} {τ} L⊨τ ¬n ε∈L = case ∃[ b ] ((null L →
   open _≤_ τ₁≤τ₂
   module A⊨τ₁ = _⊨_ A⊨τ₁
 
+⊨-liftˡ : ∀ {a fℓ lℓ} {L : Language a} {τ : Type fℓ lℓ} b → L ⊨ τ → Lift b L ⊨ τ
+⊨-liftˡ _ L⊨τ = record
+  { n⇒n = λ { ( L.lift ε∈L ) → n⇒n ε∈L }
+  ; f⇒f = λ { ( l , L.lift xl∈L ) → f⇒f (-, xl∈L)}
+  ; l⇒l = λ { ( l , l≢[] , L.lift l∈L , l′ , L.lift lxl′∈L ) → l⇒l (-, l≢[] , l∈L , -, lxl′∈L)}
+  }
+  where
+  open _⊨_ L⊨τ
+
 L⊨τ⊥⇒L≈∅ : ∀ {a} {L : Language a} → L ⊨ τ⊥ → L ≈ˡ ∅
 L⊨τ⊥⇒L≈∅ {L = L} L⊨τ⊥ = record
   { f = λ {l} → elim l