The logical framework has only two type formers: \(\Pi x {:} A. B\) (usually written \((x {:} A)B\) or \((x {:} A) \rightarrow B\) in the logical framework formulation) and \(\U\) (usually called \(\Set\)). The rules for \(\Pi x{:} A. B\) (\((x {:} A) \rightarrow B\)) are the same as given above (including \(\eta\)-conversion). The rules for \(\U\) (\(\Set\)) are also the same, except that the logical framework only stipulates closure under \(\Pi\)-type formation.