Seminormal rings (following Thierry Coquand)

The Traverso–Swan theorem says that a reduced ring is seminormal if and only if the natural homomorphism is an isomorphism [C. Traverso, Seminormality and the Picard group, Ann. Sc. Norm. Sup. Pisa 24 (1970) 585–595; R.G. Swan, On seminormality, J. Algebra 67 (1980) 210–229]. We give here all the details needed to understand the elementary constructive proof for this result given by Coquand in [T. Coquand, On seminormality, J. Algebra 305 (2006) 577–584].This example is typical of a new constructive method. The final proof is simpler than the initial classical one. More important: the classical argument by absurdum using “an abstract ideal object” is deciphered with a general technique based on the following idea: purely ideal objects constructed using TEM and Choice may be replaced by concrete objects that are “finite approximations” of these ideal objects.