iBourbaki in constructive type theory? [Fwd: 1 Postdoc and 1 PhD vacancy in the MathWiki project]