[Agda] initial T-algebra for an endofunctor T, via sized types

[Andrew Pitts]

Recently I have been more or less forced into using Agda’s sized types to get a certain development to go through and it has set me thinking about the use of sized types with inductive definitions. The current documentation stub says

"Sizes help the termination checker by tracking the depth of data structures across definition boundaries”

and then goes on to give an extended example to do with coinduction; but of course sizes are useful for induction too. 

To get a better feel for what one can achieve, I tried using sizes to construct the (provably) initial algebra for a postulated strictly positive endofunctor on Set and eventually succeeded; but the construction was much more elaborate than I expected (and involved the use of quotient types). You can see it here:

<https://www.cl.cam.ac.uk/~amp12/agda/initial-T-algebras/ <https://www.cl.cam.ac.uk/~amp12/agda/initial-T-algebras/>>

Did I somehow over-complicate things? Am I re-inventing a construction that already exists?

Andy Pitts




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191107/307f2999/attachment.html>