## Origin/Context * [[nLab:Conor McBride]] * [[nLab:Dan Licata]], abstract types with isomorphic types, [wiki](http://homotopytypetheory.org/2012/11/12/abstract-types-with-isomorphic-types/) * OTT, observational type theory * Adam Chlipala, 2012, Certified programming with dependent types, [web](http://adam.chlipala.net/cpdt/html/Intro.html), chapter on heterogenous equality * Coq.Logic.JMeq in the standard Coq library * equality of pointed types