darinmorrison/multisetoids — pull request #7 by jonsterling (2014-11-28 20:30:48+00:00)
Title: --type-in-type

Pretty much inevitable, given the unusable state of universes in Agda.