Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types"
Repository URI
Repository DOI
No Thumbnail Available
Type
Dataset
Change log
Authors
Steenkamp, Shaun
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
Version
Software / Usage instructions
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
