The Traverso-Swan theorem says that a reduced ring A is seminormal if and only if the natural homomorphism Pic A → Pic A [X] 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. © 2007 Elsevier Ltd. All rights reserved.
Lombardi, H., & Quitté, C. (2008). Seminormal rings (following Thierry Coquand). Theoretical Computer Science, 392(1–3), 113–127. https://doi.org/10.1016/j.tcs.2007.10.007