(no subject)

Ых, как же на категорном языке сформулировать, что аргумент функции будет использоваться только параметрически, т.е. его значение анализироваться не будет (т.е. будет возможна runtime erasure)?..

Может это какая-то особенная squash-операция над типом?.., но не propositional truncation и не двойное отрицание.