I once did an introductory talk to Agda that was structured around solving the MU problem, i.e. proving that MU is not derivable in MIU: https://unsafePerform.I

I once did an introductory talk to Agda that was structured around solving the MU problem, i.e. proving that MU is not derivable in MIU: https://unsafePerform.IO/projects/agda/sg-meetup/SGMeetup.pdf https://unsafePerform.IO/projects/agda/sg-meetup/SGMeetup.pd... (the MIU bit starts in Part III, slide 46)