diff options
Diffstat (limited to 'src/Cfe/Type')
| -rw-r--r-- | src/Cfe/Type/Construct/Lift.agda | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Cfe/Type/Construct/Lift.agda b/src/Cfe/Type/Construct/Lift.agda new file mode 100644 index 0000000..9f8e439 --- /dev/null +++ b/src/Cfe/Type/Construct/Lift.agda @@ -0,0 +1,20 @@ +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary using (Setoid) + +module Cfe.Type.Construct.Lift + {c ℓ} (over : Setoid c ℓ) + where + +open import Cfe.Type over +open import Level as L hiding (Lift) +open import Function + +Lift : ∀ {fℓ₁ lℓ₁} fℓ₂ lℓ₂ → Type fℓ₁ lℓ₁ → Type (fℓ₁ ⊔ fℓ₂) (lℓ₁ ⊔ lℓ₂) +Lift fℓ₂ lℓ₂ τ = record + { Null = τ.Null + ; First = L.Lift fℓ₂ ∘ τ.First + ; Flast = L.Lift lℓ₂ ∘ τ.Flast + } + where + module τ = Type τ |