Repository logo
 

Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types"

Repository URI

https://www.repository.cam.ac.uk/handle/1810/330136

Repository DOI

https://doi.org/10.17863/CAM.77483
Thumbnail Image

Files

Quotients-InductiveTypes-And-QuotientInductiveTypes-Code.zip (401.53 KB)

Type

Dataset

Change log

Authors

Pitts, Andrew  ORCID logo  https://orcid.org/0000-0001-7775-3471
Fiore, Marcelo  ORCID logo  https://orcid.org/0000-0001-8558-3492

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

Publisher

Rights and licensing

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

Relationships

Is previous version of:
https://doi.org/10.17863/CAM.82943

Collections

Research Data - Computer Science and Technology