Dan Licata, abstract types with isomorphic types, wiki
OTT, observational type theory
Adam Chlipala, 2012, Certified programming with dependent types, web, chapter on heterogenous equality
Coq.Logic.JMeq in the standard Coq library
equality of pointed types