Вы не найдёте литературы, обучающей логике на основе теории типов, или учебников по математике, которые опираются на теорию типов, а не на теорию множеств. И ученик так же, как в этой теме, будет блуждать в потёмках. А так да, теория типов хороша, как чужая жена.

Ну я ж не про теорию типов, интерпретация BHK на то и неформальная.