Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types"
Formal proofs for the results in the paper "Quotients, Inductive Types and Quotient Inductive Types" constructed with the Agda theorem proving system, version 2.6.2.
Important note: There is an updated version of this dataset. Version 2 updates some links to agree with the published version of the accompanying journal paper and uses Agda version 22.214.171.124 to check the code. See https://doi.org/10.17863/CAM.82943 for Version 2