Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types"
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.
Except where otherwise noted, this item's licence is described as Attribution 4.0 International (CC BY 4.0)