I hadn't been aware of Tarau's work: http://www.cse.unt.edu/~tarau/ http://www.cse.unt.edu/~tarau/ The real treasure looks like being his theory of isomorphis

I hadn't been aware of Tarau's work: http://www.cse.unt.edu/~tarau/ http://www.cse.unt.edu/~tarau/ The real treasure looks like being his theory of isomorphisms: http://logic.csci.unt.edu/tarau/research/2010/ISO.pdf http://logic.csci.unt.edu/tarau/research/2010/ISO.pdf I haven't read it all yet, but it reminds me a bit of the isomorphic kernel described here: http://www.informatik.uni-marburg.de/~rendel/unparse/rendel10invertible.pdf http://www.informatik.uni-marburg.de/~rendel/unparse/rendel1... Discusion on LtU here: http://lambda-the-ultimate.org/node/4191 http://lambda-the-ultimate.org/node/4191 Sometimes wading through the noise on HN is worth it when gems like this turn up. Mik