W-types in homotopy-type theory – CORRIGENDUM. (5th April 2016) - VAN DEN BERG, BENNO; MOERDIJK, IEKE
Abstract : In the article below, Theorem 3.4 requires the additional assumption that A is Kan as well. Indeed, the inductive proof as given only shows that if W ( f )<α is a Kan complex, then W ( f )<α+1 → A is a Kan fibration.