I'm not familiar with Agda, but it's entirely possible its syntax is just not good. It doesn't contradict pg's point.