> 1. I would say the primary application is to proving that certain casts (function cast, etc.) are the primary result of the paper.

I think you accidentally a word.

Re 2: That makes sense to me. In Haskell any terms can contain exceptions but they can only be caught in IO.

I look forward to reading the paper this weekend! I started really appreciating profunctors when I first learned what an equipment was, they just seemed to make everything fall into place. One thing I find intriguing about your paper is that the equipment participates directly in the models of the type theory instead of being a way to relate different models ala formal category theory.

Perhaps the reason why profunctors aren't highlighted more often is the same prejudice that gives functions a more central place than relations.