In the paper Knowledge Representation in Bicategories of Relations there is a short remark on p47 that makes a distinction that seems quite far ranging regarding the Curry-Howard Correspondence. The paper is is interested in "types with logic" not "types as logic", where the first is sometimes called "two-level type theory", or "logic-enriched type theory".
It cites Nicola Gambino and Peter Aczel 2006 paper The generalised type-theoretic interpretation of constructive set theory, which is difficult to read.
Is there a nice intuitive explanation of this distinction? (Something that would allow me to understand the gist of it, and know at what point I would need to dig into the details?)
You might try these two posts by Mike Shulman, Propositions as Some Types and Algebraic Nonalgebraicity and Freedom From Logic.