Lambda Calculi and Categories

Stream: Is there code for X?

[Chris Henson]

Are there any formaizations in Lean of the connection between lambda calculi and categories? For instance the simply-typed lambda calculus and cartesian closed categories, dependent types and locally cartesian closed categories, etc. I'm working on this myself (for my PhD's candidacy paper) and would like to be able to compare approaches.