In this note we shall assume acquaintance with [T4] and the parts of [T1] which deal with intuitionistic arithmetic in all finite types. The bibliography just continues the bibliography of [T4].The principal purpose of this note is the discussion of two models for intuitionistic finite type arithmetic with fan functional. The first model is needed to correct an oversight in the proof of Theorem 6 [T4, §5]: the model ECF+as defined there cannot be shown to have the required properties inEL+ (...) QF-AC, the reason being that a change in the definition ofW12alone does not suffice—if one wishes to establish closure under the operations of HAωthe definitions ofW1σfor other σ have to be adopted as well. It is difficult to see how to do this directly in a uniform way — but we succeed via a detour, which is described in §2.For a proper understanding, we should perhaps note already here thaton the assumption of the fan theorem, ECF+as defined in [T4] and the new model of this note coincide ; but inELit is impossible to prove this. (shrink)