Comment by mietek

Author of the mechanization here. Feel free to suggest materials from the history of intuitionistic mathematics and type theory that ought to be mechanized and made available to a wider audience — the less well-known, the better.