Proof theoretical issues in Martin-Löf Type Theory and Homotopy Type Theory