Code supporting "Constructing Initial Algebras Using Inflationary Iteration"
Repository URI
Repository DOI
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
Sponsorship
EPSRC (2119809)
Steenkamp is funded by ERSRC Research Studentship 2119809 (institution reference RGS3370