Имеет ли система F с парами сильные свойства нормализации и сокращения объекта?

Во многих учебниках легко найти доказательства сокращения предмета и строгой нормализации для Системы F, а также иногда есть определения Системы F с парами, где (t, r) - это термин, а не только кодировка. Вопрос в том, что будет ссылкой на эту систему?

Обработка пар, задаваемых кодированием, например, в Proofs и Types , не является тем, что вы обычно хотите, поскольку они не являются «сюръективными парами», т. Е. Нет правила eta. Назовем сюръективные пары, продукты.

Расширение системы F с продуктами и единицами дано в: Di Cosmo, 1995, Изоморфизмы типов: от лямбда-исчисления до информационного поиска и языкового дизайна , Birkhauser: Basel.

Вы можете добавить произвольные (положительные) индуктивные типы к системе F и показать, что системой с соответствующими элиминаторами является SN. Это рассматривается в диссертации Мендлера здесь .