Comment by marchdown

Oh no! I was following his work closely and had high hopes for him delivering on his vision: type theory and constructive notion of equality not getting in the way of doing mathematics with computer, but helping us along. It will hopefully will be picked up by his collaborators.