Constructive Sheaf Semantics
Erik Palmgren · Mathematical logic quarterly · 1997
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.