Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types" (v2)

Thumbnail
View / Open Files
Authors
  Pitts, Andrew
  Fiore, Marcelo
Steenkamp, SC
Publication Date
2022-03-30
Previous Version(s)
Type
Dataset
Metadata
Show full item record
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
Related Item: https://elements.admin.cam.ac.uk/viewobject.html?cid=1&id=1330147
Publication Reference: https://doi.org/10.46298/lmcs-18(2:15)2022https://www.repository.cam.ac.uk/handle/1810/343176
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.

Attribution 4.0 International (CC BY 4.0)
Except where otherwise noted, this item's licence is described as Attribution 4.0 International (CC BY 4.0)