On https://ncatlab.org/nlab/show/sum+type the following $\eta$-reduction rule is given for sum types: $$\mbox{match}(p,x.c[\mbox{inl}(x)/z],y.c[\mbox{inr}(y)/z]) \rightarrow_{\eta} c[p/z]$$ This rule makes a lot of sense to me. But doesn't it break the Church Rosser property? Let $c$ be the term $$D \ \mbox{match}(z, u.A, v.B)$$ (Assume that $z$ is not free in $A$, $B$ or $D$). Then consider the term
$$\mbox{match}(p,x.c[\mbox{inl}(x)/z],y.c[\mbox{inr}(y)/z]) \hskip 1 cm (1)$$ We have $c[\mbox{inl}(x)/z]$ $\beta$-reduces to $D A[x/u]$ and $c[\mbox{inr}(y)/z]$ $\beta$-reduces to $D B[y/v]$. So ($1$) $\beta$-reduces to $$\mbox{match}(p,x.D A[x/u],y.D B[y/v]) \hskip 1 cm (2)$$ or renaming bound variables $$\mbox{match}(p,u.D A,v.D B) \hskip 1 cm (3)$$ That is, $(1) \rightarrow_{\beta} (3)$. But we also have that (1) $\eta$-reduces to $D \ \mbox{match}(z, u.A, v.B)[p/z]$, i.e., $$D \ \mbox{match}(p,u.A,v.B) \hskip 1 cm (4)$$ So $(1) \rightarrow_{\beta \eta} (3)$ and $(1) \rightarrow_{\beta \eta} (4)$. But I don't see how any sequence of $\beta$ or $\eta$ reductions will bring (3) and (4) together again; surely we can choose $A$, $B$ and $D$ so that (3) and (4) are in fact in $\beta \eta$ normal form.