Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types" (v2)
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, well-founded relation, weakly initial set of covers,, topos theory
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.
Except where otherwise noted, this item's licence is described as Attribution 4.0 International (CC BY 4.0)