Agda formalisation of the results of the paper "Non-wellfounded trees in Homotopy Type Theory" by Benedikt Ahrens, Paolo Capriotti and Régis Spadotti. The code is commented with theorem, definition, and lemma numbers from the paper for side-by-side reading.
The Agda library compiles with Agda 2.4.2.2, which can be downloaded here. We refer to the Agda wiki for installation instructions for Agda.