Curry-Howard style correspondences establish a tight conection between various logics on the one hand and explicitly computational calculi on the other. The canonical example is the correspondence between simple type theory (with arrow types) and natural deduction in the implicational fragment of propositional intuitionistic/minimal logic.
I understand that adding dependent types to the underlying type theory corresponds to the addition of quantifiers in the paired logic. Likewise, one can think of the passage from simple type theory to system F as corresponding to the addition of universal quantification over propositional variables. But I'm a bit unclear on what the addition of proper type operators corresponds to.
I'm sure this question has a relatively simple answer.