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?
Odpowiedzi:
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.