I probably phrased my suggestion wrong. Yes, it's not central to OP's enquiry. But I did find a basic understanding of CT to help a lot when reasoning about types, and that lecture series gives just that in a relatively simple way.