------------------------------------------------------------------------ -- The type constructor Erased, defined using weak Ξ£ and unit types ------------------------------------------------------------------------ open import Graded.Modality module Graded.Derived.Erased.NoEta.Untyped {a} {M : Set a} (π : Modality M) where open Modality π open import Definition.Untyped M open import Definition.Untyped.Sigma π open import Tools.Fin open import Tools.Nat open import Tools.PropositionalEquality private variable n : Nat Ο : Subst _ _ -- The "projection" erased. erased : Term n β Term n β Term n erased = fstΚ· π opaque -- A substitution lemma for erased. erased-[] : (A t : Term n) β erased A t [ Ο ] β‘ erased (A [ Ο ]) (t [ Ο ]) erased-[] = fstΚ·-[]