Thanks, Joe Niederberger, for drawing our attention to 'Homotopy Type Theory' (HOTT) and the BIG book on it: "Homotopy Type Theory: Univalent Foundations of Mathematics".
I have since re-read, quite carefully, the Introduction to the book - No, I've not yet done any modeling there, because I believe this will be possible only when I've at least started studying 'Foundations'. I've made a fair start on "Foundations" - Type Theory; Type Theory Vs. Set Theory; Function Types; etc. I've also read (and listened to) the talk on "Univalent Foundations" by Vladimir Voevodsky.
As noted in an earlier post, some of it is pretty hairy stuff (in particular when I look at some of the 'exercises' in the book) - and I'm sure I'll not succeed in 'studying' (with modeling) the book as a whole UNLESS I am guided by someone who's reasonably expert with HOTT. Let's see how it goes.
However, I DO believe that the 'structures' (the 'higher-level models') within OPMS would help clarify several of the issues in HOTT. Hopefully, I shall be able to convince someone accordingly at 'The Univalent Foundations Program'. As note