Oℕ
В зиво модулях - к инпуту внутри аутпута. Во фриструктурах - к образующему множеству/типу. В сортах таглесс файнал - к ограничениям на "символьный" параметр. В специальных языках для этого отдельная третья составляющая типа присутствует. Но всё это стоит рассматривать как договорённости, разные способы сообщить примерно одно и то же.