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
Created on November 29, 2012 at 13:52:09. See the history of this page for a list of all contributions to it.