is anyone out there extremely familiar with asher-style type logics for lexical semantics? trying to understand how type presuppositions propagate across the curry-howard isomorphic boundary (ie: if I presuppose an argument of type A in the lexical content (LHS), is that reflected on the type side?)