I keep reworking my manuscript Isomorphism within Set-Theoretic Type Theory. This is a treatment of isomorphism within a formulation of dependent type theory where expressions are assigned their obvious (naive) set-thereotic compositional meaning. For example the type "group" denotes (literally) the class of tuples of a carrier set (the group elements) and the group operations satisfying the group properties. Of course an Abelian group is also a group. The semantic value of a proposition is either true or false (a Boolean). These simple naive statements are not true of constructive type theory or homotopy type theory (HoTT).
I have also written several blog posts on the subject including a post on formalism, Platonism and mentalese.