Abstract: "Writing an evaluator for the simply typed lambda calculus is a classic example of a dependently typed program that appears in numerous tutorials. The central idea is to represent the well-typed lambda terms over some universe U using an inductive family. Before writing the evaluator for such terms, we need to define a type of environments, capturing the values associated with the free variables in a term.