M-types

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.

Installation

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.