I mean the Curry-Howard-Lambek correspondance is that lambda calculus, proofs/logic and category theory are all just different ways of talking about the same thing for the most part