1078 \nn{...}

  1078 $\cl{\cC}(W)$ is a colimit of a diagram of sets, and each of the arrows in the diagram is

  1079 injective.

  1080 Concretely, the colimit is the disjoint union of the sets (one for each decomposition of $W$),

  1081 modulo the relation which identifies the domain of each of the injective maps

  1082 with it's image.

  1083 

  1084 To save ink and electrons we will simplify notation and write $\psi(x)$ for $\psi_{\cC;W}(x)$.

  1085 

  1086 Suppose $a, \hat{a}\in \psi(x)$ have the same image in $\cl{\cC}(W)$ but $a\ne \hat{a}$.

  1087 Then there exist

  1088 \begin{itemize}

  1089 \item decompositions $x = x_0, x_1, \ldots , x_{k-1}, x_k = x$ and $v_1,\ldots, v_k$ of $W$;

  1090 \item anti-refinements $v_i\to x_i$ and $v_i\to x_{i-1}$; and

  1091 \item elements $a_i\in \psi(x_i)$ and $b_i\in \psi(v_i)$, with $a_0 = a$ and $a_k = \hat{a}$, 

  1092 such that $b_i$ and $b_{i+1}$both map to (glue up to) $a_i$.

  1093 \end{itemize}

  1094 In other words, we have a zig-zag of equivalences starting at $a$ and ending at $\hat{a}$.

  1095 The idea of the proof is to produce a similar zig-zag where everything antirefines to the same

  1096 disjoint union of balls, and then invoke the associativity axiom \ref{nca-assoc}.

  1097 \nn{hmmm... it would be nicer if this were ``7.xx" instead of ``4"}

  1098 

  1099 Let $z$ be a decomposition of $W$ which is in general position with respect to all of the 

  1100 $x_i$'s and $v_i$'s.

  1101 There there decompositions $x'_i$ and $v'_i$ (for all $i$) such that

  1102 \begin{itemize}

  1103 \item $x'_i$ antirefines to $x_i$ and $z$;

  1104 \item $v'_i$ antirefines to $x'_i$, $x'_{i-1}$ and $v_i$;

  1105 \item $b_i$ is the image of some $b'_i\in \psi(v'_i)$; and

  1106 \item $a_i$ is the image of some $a'_i\in \psi(x'_i)$, which in turn is the image

  1107 of $b'_i$ and $b'_{i+1}$.

  1108 \end{itemize}

  1109 Now consider the diagrams

  1110 \[ \xymatrix{

  1111 	& \psi(x'_{i-1}) \ar[rd] & \\

  1112 	\psi(v'_i) \ar[ru] \ar[rd] & & \psi(z) \\

  1113 	& \psi(x'_i) \ar[ru] &

  1114 } \]

  1115 The associativity axiom applied to this diagram implies that $a'_{i-1}$ and $a'_i$

  1116 map to the same element $c\in \psi(z)$.

  1117 Therefore $a'_0$ and $a'_k$ both map to $c$.

  1118 But $a'_0$ and $a'_k$ are both elements of $\psi(x'_0)$ (because $x'_k = x'_0$).

  1119 So by the injectivity clause of the composition axiom, we must have that $a'_0 = a'_k$.

  1120 But this implies that $a = a_0 = a_k = \hat{a}$, contrary to our assumption that $a\ne \hat{a}$.