Apakah Sistem F dengan pasangan memiliki sifat normalisasi dan reduksi subjek yang kuat?

Sangat mudah untuk melihat di banyak buku teks bukti pengurangan subjek dan normalisasi yang kuat untuk Sistem F, juga, kadang-kadang ada definisi Sistem F dengan pasangan, di mana (t, r) adalah istilah, bukan hanya pengkodean. Pertanyaannya adalah, apa yang akan menjadi referensi untuk sistem ini?

Perlakuan pasangan yang diberikan oleh pengkodean, seperti dalam Bukti dan Jenis , bukan apa yang biasanya Anda inginkan karena mereka bukan "pasangan surjektif", yaitu, tidak ada aturan eta. Mari kita sebut pasangan surjective, produk.

Perpanjangan sistem F dengan produk dan unit diberikan dalam: Di Cosmo, 1995, Isomorfisme jenis: dari lambda-calculus ke pencarian informasi dan desain bahasa , Birkhauser: Basel.

Anda dapat menambahkan tipe induktif yang berubah-ubah (positif) ke sistem F, dan menunjukkan bahwa sistem dengan eliminator yang sesuai adalah SN. Ini dibahas dalam tesis Mendler di sini .