Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types"
Citation
Pitts, A., Steenkamp, S. C., & Fiore, M. (2021). Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types" [Dataset]. https://doi.org/10.17863/CAM.77483
Description
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 2.6.2.1 to check the code. See https://doi.org/10.17863/CAM.82943 for Version 2
Format
Agda <https://github.com/agda/agda> version 2.6.2
Keywords
dependent type theory, higher inductive types, quotient types, well-founded relation, weakly initial set of covers, topos theory
Identifiers
This record's DOI: https://doi.org/10.17863/CAM.77483
Rights
Attribution 4.0 International (CC BY 4.0)
Licence URL: https://creativecommons.org/licenses/by/4.0/
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.