An Intuitionistic Theory of Types: Predicative Part