 Curry and Feys (1958) extended the correspondence idea to one between type theory and Gentzen’s sequent calculus. In the paper already cited, circulated in 1969, but only published in a volume in a Festschrift for Curry in 1980, W.A. Howard (1969) deepened the CH correspondence by demonstrating a correspondence between intuitionistic sequent form natural deduction and type theory in \(\lambda\)-calculus format, generalising to encompass intuitionist arithmetic- ‘Heyting arithmetic’ (HA)- (thus requiring an extension from all of propositional to predicate logic), all as part of a project of investigation of the constructivist notion of a construction. Howard deepened the results by making clear not only a correspondence between provable formulae in the sequent calculus and type ascriptions, but also between the terms in the type ascriptions and proofs of the corresponding  formulae.[2]  For example, (to the horror of relevantists) A \(\rightarrow\) (B \(\rightarrow\) A) is provable in T\(_{\rightarrow}\). The corresponding type is \(\alpha \Rightarrow(\beta \Rightarrow \alpha)\), the type of the basic operator K, whose action is 