Walk away now.
Type Theory derailed my PhD studies.
Seduced by constructivism, Curry-Howard, Martin-Löf and especially Girard's Proofs and Types, I wasted two years and subsequently abandoned my postgraduate studies.
It's comp. sci. flavoured esoteric nonsense.
is there anything in the world that is non-nonsense? so it is better to study pure-nonsense, just because it is pure