Code supporting "Constructing Initial Algebras Using Inflationary Iteration"

Repository URI
https://www.repository.cam.ac.uk/handle/1810/330134
Repository DOI
https://doi.org/10.17863/CAM.73911
No Thumbnail Available
Files
coniau-code.zip (221.76 KB)
Type
Dataset
Change log
Authors
Steenkamp, Shaun 
Description

Formalization of definitions, theorems and proofs from the paper

A. M. Pitts and S. C. Steenkamp, Constructing Initial Algebras Using Inflationary Iteration. In K. Kishida (ed), Fourth International Conference on Applied Category Theory (ACT 2021), EPTCS 2012, to appear.

using the Agda theorem-proving system

Version
Software / Usage instructions
Checked with Agda version 2.6.2 Root file: index.html (source-code/index.agda)
Keywords
constructive logic, initial algebra of endofunctor, Type theory, WISC axiom
Publisher
Rights
Attribution 4.0 International (CC BY 4.0) Repository logo
Sponsorship
EPSRC (2119809)
Steenkamp is funded by ERSRC Research Studentship 2119809 (institution reference RGS3370
Relationships
https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACT2021:16
 https://www.repository.cam.ac.uk/handle/1810/328263
Supplements:
https://www.repository.cam.ac.uk/handle/1810/328263
https://doi.org/10.4204/EPTCS.372.7
 https://doi.org/10.48550/arXiv.2105.03252
Collections
Research Data - Computer Science and Technology