A Calculus Of Definitions Formalization of Thierry Coquand's unpublished A Calculus of Definitions (June 13, 2017 draft) in Agda.