Dr. Harper spends a lot of time developing IPL and it's semantics both as Heyting Algebra and a Bi-Cartesian Closed Category in the first few weeks. I found it

Dr. Harper spends a lot of time developing IPL and it's semantics both as Heyting Algebra and a Bi-Cartesian Closed Category in the first few weeks. I found it easy to follow with a smattering of type theory and category theory background.