A work in progress of formal aspects, in Agda, of an equational calculus for ∞-categories, implementing the free model construction, normalization algorithm, and a decision procedure for equality of higher-categorical terms, based on the theory developed in the preprint 'Equational Reasoning in ∞-Categories.'