I have retitled my manuscript Isomorphism within Naive Type Theory. This is a treatment of isomorphism within a formulation of dependent type theory where expressions are assigned their obvious (naive) compositional meaning. This simplification is made possible by an up-front commitment to a classical set-theoretic foundation of mathematics

I have also written several blog posts on the subjects including this most recent one.