July 10th, 2009 by Nils Anders Danielsson
Today Thorsten and I talked about nested fixpoints of the form μX.νY.F X Y. It turns out that such fixpoints cannot be represented directly in Agda. More details are available in a post to the Agda mailing list.
Additionally here is the whiteboard from the meeting: