Ed Kellett edk0

This article is now published on my website: Prefer Subshells for Context.

	{-# OPTIONS --no-import-sorts --erasure #-}
	open import Agda.Primitive renaming (Set to Type)
	open import Data.Nat
	open import Data.Bool
	open import Data.Product
	open import Relation.Binary.PropositionalEquality

	-- An element of `Remember a` is a witness that `a` exists at runtime.
	data Remember {ℓ} {@0 A : Type ℓ} : (@0 a : A) → Type ℓ where
	instance remember : {a : A} → Remember a