ERRATUM

In Section 4 we defined two kinds of categorical models called λc2η-models and monadic λc2η-models, where the latter is stronger notion than the former; and in Theorem 4 we stated that the λc2η-calculs is sound and complete for the λc2η-models. It turns out that this does not hold, and instead we have to assume monadic λc2η-models rather than λc2η-models; this is necessary in the sense that the calculus is also complete for the monadic λc2η-models, as the term model becomes a monadic λc2η-model. Thus a correct theorem instead of Theorem 4 is: