There is a wealth of metatheoretical or philosophical considerations behind the technicalities of constructive type theory. The purpose of this chapter is to cast at least some light on at least a few of those considerations and to draw attention to the philosophical underpinnings and intricacies of type theory. These issues have been selected for consideration: the philosophical evergreen called identity (Sect. i), one of the few main pillars of any logic, namely the notion of judgement, which is also elucidated by means of the theory of knowledge (Sect. ii), the great tradition of metalogic with its principal targets: consistency, completeness and decidability (Sect. iii), and last but not least the positioning of constructive type theory within the philosophy or foundations of mathematics (Sect. iv). Needless to write, the real bulk of metatheoretical or philosophical consideration remains still to be carried out — the following is but an initiation.