証明論と型理論の対応

あのハスケル・カリーと、ウィリアム・アルヴィン・ハワードが見つけた

これ対応関係ってどうやって示すの？

対応することは直感的に理解できるけど、実際なんで対応してるのかみたいな部分を何も知らない。

なんもわからんけど、圏論とか使うんですかね