An Agda Formalization of "On Recursion in Graded Modal Type Theory"

An Agda formalization related to the paper "On Recursion in Graded Modal Type Theory" by Oskar Eriksson, Andreas Abel and Nils Anders Danielsson. It builds on a formalization originally due to Andreas Abel, Joakim Öhman and Andrea Vezzosi, with additional contributions by Naïm Camille Favier, Eve Geng, Gaëtan Gilbert, Ondřej Kubánek, and Wojciech Nawrocki. The archive also includes html renderings of the included Agda code as well as parts of Agda's standard library (version 2.4) and Agda's builtin modules (version 2.8.0).