<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">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<br class=""><br class="">"Sizes help the termination checker by tracking the depth of data structures across definition boundaries”<div class=""><br class=""></div><div class="">and then goes on to give an extended example to do with coinduction; but of course sizes are useful for induction too. </div><div class=""><br class=""></div><div class="">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:</div><div class=""><div class=""><br class=""></div><div class=""><<a href="https://www.cl.cam.ac.uk/~amp12/agda/initial-T-algebras/" class="">https://www.cl.cam.ac.uk/~amp12/agda/initial-T-algebras/</a>><br class=""><div class=""><br class=""></div><div class="">Did I somehow over-complicate things? Am I re-inventing a construction that already exists?</div><div class=""><br class=""></div><div class="">Andy Pitts</div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div></div></div></body></html>