The paper develops a proof-theoretic semantics for belief reports by extending the constructive type-theoretical formalism presented in Więckowski (Stud Log 100:815–853, 2012) with a specific kind of set-forming operator suited for the representation of belief attitudes. The extended formalism allows us to interpret constructions which involve, e.g., iteration of belief, quantifying into belief contexts, and anaphora in belief reports. Moreover, constructive solutions to canonical instances of the problem of hyperintensionality are suggested. The paper includes a discussion of Ranta’s (Type-theoretical grammar, 1994) constructive account of belief reports.