Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types" (v2)
Citation
Pitts, A., Fiore, M., & Steenkamp, S. (2022). Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types" (v2) [Dataset]. https://doi.org/10.17863/CAM.82943
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 of the dataset 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.
Format
Agda <https://github.com/agda/agda> version 2.6.2.1
Keywords
dependent type theory, higher inductive types, quotient types, topos theory, weakly initial set of covers,, well-founded relation
Relationships
Identifiers
This record's DOI: https://doi.org/10.17863/CAM.82943
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.
Recommended or similar items
The current recommendation prototype on the Apollo Repository will be turned off on 03 February 2023. Although the pilot has been fruitful for both parties, the service provider IKVA is focusing on horizon scanning products and so the recommender service can no longer be supported. We recognise the importance of recommender services in supporting research discovery and are evaluating offerings from other service providers. If you would like to offer feedback on this decision please contact us on: support@repository.cam.ac.uk