一句话：在 Setoid 模型中用依赖 W-类型构造 W-类型，证明 setoid 范畴有多项式自函子的初始代数，并给出 Coq 形式化。
该文研究外延 Martin-Löf 类型论的 setoid 模型是否支持 W-类型。作者在完全内涵的基础理论中，借助依赖 W-类型构造 setoid 模型里的 W-类型，等价地证明 setoid 的内部范畴对多项式自函子具有初始代数。关键构造将初始代数到给定代数的代数态射 setoid 表示为依赖 W-类型上的 setoid，并借此刻画该同态对象。文章进一步讨论自由 setoid 的情形：仅在讨论自由 setoid 时假设 identity types。由于使用依赖 W-类型，构造无需消去到类型宇宙。所有结果已在 Coq 中验证，形式化代码公开于作者 GitHub。
We present a construction of W-types in the setoid model of extensional Martin-L\"of type theory using dependent W-types in the underlying intensional theory. More precisely, we prove that the internal category of setoids has initial algebras for polynomial endofunctors. In particular, we characterise the setoid of algebra morphisms from the initial algebra to a given algebra as a setoid on a dependent W-type. We conclude by discussing the case of free setoids. We work in a fully intensional theory and, in fact, we assume identity types only when discussing free setoids. By using dependent W-types we can also avoid elimination into a type universe. The results have been verified in Coq and a formalisation is available on the author's GitHub page.