Czy system F z parami ma silne właściwości normalizacyjne i redukujące podmiot?

W wielu podręcznikach łatwo jest przejrzeć dowody redukcji podmiotu i silnej normalizacji dla Systemu F, czasem też istnieją definicje Systemu F z parami, gdzie (t, r) jest terminem, a nie tylko kodowaniem. Pytanie brzmi: jakie byłoby odniesienie dla tego systemu?

Traktowanie par podanych przez kodowanie, takich jak w Dowodach i Typach , nie jest tym, czego zwykle chcesz, ponieważ nie są one „parami przymiotników”, tzn. Nie ma zasady eta. Nazwijmy parami przejmującymi, produktami.

Rozszerzenie systemu F o produkty i jednostkę podano w: Di Cosmo, 1995, Izomorfizmy typów: od rachunku lambda do wyszukiwania informacji i projektowania języka , Birkhauser: Bazylea.

Możesz dodać dowolne (dodatnie) typy indukcyjne do układu F i pokazać, że układ z odpowiednimi eliminatorami to SN. Zajmuje się to tutaj teza Mendlera .