Part I indicates that typed-calculi are a formulation of higher-order logic, and cartesian closed categories are essentially the same. Part …
