[Agda] Termination proof in partiality monad

[Dan Doel]

On Wednesday 19 November 2008 7:15:46 pm Dan Doel wrote:
> And there you have it. A genuine proof of convergence for factorial that
> passes the type checker. Proof for a version of fix that actually works
> correctly is left as an exercise to the reader. :)

I just realized that some of this thread has been cross posted to coq-club, 
but I've only been following up to the Agda list. If anyone wishes to forward 
my code to the former list to spur discussion there (I'm not sure how helpful 
the Agda will be to finding an analogous Coq solution, as I've not learned 
Coq), they have my permission.

-- Dan