For the purpose of illustration we consider meaning explanations only for three type formers: \(\N, \Pi x {:} A.B\), and \(\U\). The context free grammar for the terms of this fragment of Intuitionistic Type Theory is as follows: