We study a family of distributor-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We then restrict to a particular case of our construction and show that the interpretation of a program corresponds to the interpretation of its Böhm tree. We prove this result exploiting the proof-relevance of our model, which allows a fine-grained analysis of programs evaluation. We then obtain the characterization of the theory induced by the bicategorical model: two lambda-terms share the same interpretation exactly when their Bohm trees coincide.