Sheaf models over sites, introduced by Grothendieck in algebraic geometry, are also important in the meta-theory of intuitionistic mathematics for showing that some properties are not valid constructively or for providing models of the notion of choice sequences. In this talk, I would like to explain another use of sheaf models in constructive mathematics, suggested by Joyal in 1975, which is to provide a way to build an algebraic closure of an arbitrary field.