Repository logo
 

Code supporting "Constructing Infinitary Quotient-Inductive Types"

Repository URI

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

Repository DOI

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

Files

coniqi.zip (793.72 KB)

Type

Dataset

Change log

Authors

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

Description

Agda code (source and html) supporting the paper "Constructing Infinitary Quotient-Inductive Types" in 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2020), Dublin, Ireland 2020. See README file for more information.

Version

Software / Usage instructions

Checks with Agda <https://wiki.portal.chalmers.se/agda/agda.php> version 2.6.0.1. Root file is README.agda

Keywords

dependent type theory, higher inductive types, inductive-inductive definitions, quotient types, sized types, category 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

Supplements:
https://www.repository.cam.ac.uk/handle/1810/302210
https://doi.org/10.1007/978-3-030-45231-5_14

Collections

Research Data - Computer Science and Technology