This repository contains all agda code for the formalisation of the boxed lambda calculus discussed in my bachelor's thesis