Abstract. Sheaf semantics is developed within a constructive and predicative framework, Martin-Löf's type theory. We prove strong completeness of many sorted, first order intuitionistic logic with respect to this semantics, by using sites of provably functional relations.
Erik Palmgren, March 9, 1999.