The current version is described in MathZero, the Classification Problem, and 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.

I have also written several blog posts on the subject including a post on formalism, Platonism and mentalese.