Some observations about μν

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:
munu
/Thorsten

Leave a Reply