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

Thumbnail
View / Open Files
Authors
  Pitts, Andrew
Steenkamp, Shaun
  Fiore, Marcelo
Publication Date
2021-11-01
Type
Dataset
Metadata
Show full item record
Citation
Pitts, A., Steenkamp, S., & Fiore, M. (2021). Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types" [Dataset]. https://doi.org/10.17863/CAM.77483
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.
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/

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)