Errata of CATEGORICAL MODEL CONSTRUCTION FOR PROVING SYNTACTIC PROPERTIES^{1}

Takafumi SAKURAI

1 Revised version We list up errors of our paper^{1} here, but we would like you to read the revised full version of this paper:

    http://www.math.s.chiba-u.ac.jp/~sakurai/papers/cms.dvi.gz

2 Section 4, p.190 The condition (P1) if P (M[x := N]) and P (N), then P (λx.M) should be replaced by the conditions (P1a) If P (M[x := z]) where z is a variable, then P (M). (P1b) If P (M), then P (λx.M). and some proofs should be modified accordingly.

3 Section 5, p.195 The paragraph after (4) in the Definition 5.3 and the paragraph above the Definition 5.4 should be replaced by the following paragraphs.

In the following, we will abbreviate 𝔼//T as 𝔼̃. For F : l ⟶ k and h : D ⟶ E where D, E ∈ _{k}T^{∗}, there is an arrow h ∘ \overline{F} D : F^{∗}D ⟶ E. By (4), there is a unique arrow g : F^{∗}D ⟶ F^{∗}E. We write F^{∗}h for the arrow g. For f : E′ ⟶ E, we define a reindexing functor f^{∗} : 𝔼̃_{E} ⟶ 𝔼̃_{E′} as follows. We take an arrow f′ such that f = \overline{pf}E ∘ f′ and pf′ = id (f′ uniquely exists because p is a fibration) and define f^{∗}(E; X) =^{def} E′; (pf)^{∗}X

and f^{∗}[id_{E}, g] =^{def} [id_{E′}, (pf)^{∗}g ∘ (f′ × id_{(pf)^{∗}X})].

An arrow ⋯

We introduce some notations. Let E ∈ _{k}T^{∗}, A ∈ _{k}T , and E′ ∈ _{l}T^{∗}. We

define ↓(E; A) =^{def} π|_{1}^{E,A} : E × A ⟶ E, ^{+}E =^{def} (π|_{1}^{k,1})^{∗}E, ⇓(E) =^{def} \overline{π|_{1}^{k,1}}E :

+E ⟶ E. For f : E′ ⟶ E in 𝔼, we define ^{+}f as follows. We take an arrow f′

such that f = \overline{pf}E ∘ f′ and pf′ = id and define ^{+}f =^{def} \overline{pf × id_{1}}^{+}E ∘ (π|_{1}^{l,1})^{∗}f′.

4 Section 6, p.199 The condition (P1) if P (M[x := N]) for some P -value or type N, then P (πx.M) should be replaced by the conditions (P1a) If P (M[x := N]) where N is a variable or a type, then P (M). (P1b) If P (M), then P (πx.M). and some proofs should be modified accordingly. References

1. T. Sakurai, Categorical Model Construction for Proving Syntactic Properties, In Proceedings of Third Fuji International Symposium on Functional and Logic Programming, 187–206, 1998.