Agda2 tuples

[voidex]

Продолжаю ковырять. Вроде как всё, что я хотел бы от поддержки туплов, Агда умеет (туплы мои). По сути получается удобная работа с гетерогенным списком. Я, правда, не писал ещё всякие map/zip и прочие, но, надеюсь, там проблем не будет.
http://hpaste.org/68922