Constructive mathematics and models of type theory