(∃, ∀) とそれぞれ「仲がいい」命題結合子が (∨, ∧) だったり (∧, →) だったりするのは型理論特有ではなくもっといろんな場面で出てくると思うけどこの関係は面白いと思う