Code supporting "Constructing Infinitary Quotient-Inductive Types"
Repository URI
Repository DOI
Change log
Authors
Steenkamp, Shaun
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
