This repository contains an Agda formalization of Section 2 of "Effects and Coeffects in Call-By-Push-Value".
Everything.agda indicates which files correspond to which subsections of the paper, the paper as well refers to specific theorems in this repository.
This code has been tested with Agda version 2.6.2.2 and standard library version 1.7.1.