The Davis complex is simply connected

A loop in either $X=\mathrm{\Sigma }$ or $X={\mathrm{\Sigma }}^2$ based at a vertex $v$ is homotopic rel $v$ in $X$ to an edge loop. Give $S^1$ the CW structure with one $0$-cell $\ast$ and one $1$-cell, and view the loop as a map of pairs $(S^1,\ast )\to (X,X^0)$. It is cellular on the $0$-skeleton because it sends $\ast$ to $v\in X^0={\mathrm{\Sigma }}^0$; the relative source $S^1\setminus \{\ast \}$ is one cell, so [F3] gives a cellular approximation rel $\ast$, whose image lies in $X^1={\mathrm{\Sigma }}^1$.

Suppose a loop $\beta$ in ${\mathrm{\Sigma }}^2$ based at a vertex $v$ is null-homotopic in $\mathrm{\Sigma }$, so it has a based homotopy $H\text{\hspace{0.17em}⁣}:I^2\to \mathrm{\Sigma }$ with $H(s,0)=\beta (s)$, $H(s,1)=v$, and $H(0,t)=H(1,t)=v$. Use [step 1.1] with $X={\mathrm{\Sigma }}^2$ to homotope $\beta$ rel endpoints to an edge loop ${\beta }^{\mathrm{\prime }}$ by $F\text{\hspace{0.17em}⁣}:I^2\to {\mathrm{\Sigma }}^2$, where $F(s,0)=\beta (s)$ and $F(s,1)={\beta }^{\mathrm{\prime }}(s)$. Define $H^{\mathrm{\prime }}(s,t)=F(s,1-2t)$ for $0\le t\le \frac{1}{2}$ and $H^{\mathrm{\prime }}(s,t)=H(s,2t-1)$ for $\frac{1}{2}\le t\le 1$; the two formulas agree at $t=\frac{1}{2}$, and $H^{\mathrm{\prime }}$ is a based null-homotopy of ${\beta }^{\mathrm{\prime }}$. Its boundary is cellular for $(I^2,\mathrm{\partial }{I}^2)\to (\mathrm{\Sigma },{\mathrm{\Sigma }}^2)$: the bottom edge maps into ${\mathrm{\Sigma }}^1$, and the other boundary edges and vertices map to $v\in {\mathrm{\Sigma }}^0$. The relative source has one open $2$-cell, so [F3] gives a cellular approximation rel boundary; because the source has dimension $2$, its image lies in ${\mathrm{\Sigma }}^2$. Thus ${\beta }^{\mathrm{\prime }}$ and then $\beta$ are null-homotopic in ${\mathrm{\Sigma }}^2$.

Every continuous loop in ${\mathrm{\Sigma }}^1$ based at $1$ is based-homotopic to a finite edge walk. Barycentrically subdivide the Cayley graph to an abstract simplicial graph: every original edge is split at its midpoint, so distinct original edges give distinct simplicial edges. Triangulate the circle with the basepoint as a vertex, and apply [F9] with the singleton basepoint as each distinguished subcomplex. The resulting map on a finite subdivided circle is a finite walk in the subdivided graph, with a homotopy fixing the basepoint. Delete stationary traversals and immediate reversals; at each midpoint the two incident half-edges either reverse or join to one full original edge, so compressing gives a finite based edge walk in the original graph. We now show that each such walk is null-homotopic in ${\mathrm{\Sigma }}^2$. Orient each traversal and record $s$ or $s^{-1}$ according to its direction, obtaining a word $w\in F(S)$ whose image in $W$ is $1$ by [F1]. By [F4], $w$ is a finite product $g_1{r}_1^{{ϵ}_1}{g}_1^{-1}\cdots g_k{r}_k^{{ϵ}_k}{g}_k^{-1}$ in $F(S)$, with $r_i\in R$ and ${ϵ}_i\in \{1,-1\}$; $k=0$ is allowed. The path for this product is a concatenation of conjugate relator loops, and [F5] turns equality in $F(S)$ into finitely many insertions or deletions of adjacent inverse letters. Since each Coxeter generator satisfies $s=s^{-1}$ in $W$, each such pair is an immediate backtrack in the undirected Cayley graph; [F8] ensures the $s$-edge has distinct endpoints. A relator $s^2$ traverses that edge out and back, while a relator $(st{)}^{m(s,t)}$ with distinct $s,t$ and finite label is the boundary of the corresponding $2m(s,t)$-gon in ${\mathrm{\Sigma }}^2$ by [F1]; inverse relators reverse these loops. Thus every conjugate relator loop contracts in ${\mathrm{\Sigma }}^2$ (conjugation preserves the identity class by [F6]), and the finite concatenation contracts by the group law [F6]. If $S=\mathrm{\varnothing }$, then $W=1$ and ${\mathrm{\Sigma }}^1$ is one vertex, so the only edge loop is constant; the same argument also allows the empty relator product $k=0$. If no finite rank-two label occurs, there are no polygon relators and the only relator loops are involution backtracks. Finally [step 1.1] reduces every loop in ${\mathrm{\Sigma }}^2$ at $1$ to an edge loop, proving ${\pi }_1({\mathrm{\Sigma }}^2,1)=1$.

For every vertex $v$, inclusion $j\text{\hspace{0.17em}⁣}:{\mathrm{\Sigma }}^2\hookrightarrow \mathrm{\Sigma }$ induces an isomorphism $j_{\ast }\text{\hspace{0.17em}⁣}:{\pi }_1({\mathrm{\Sigma }}^2,v)\to {\pi }_1(\mathrm{\Sigma },v)$. Every class represented by a loop in $\mathrm{\Sigma }$ has an edge-loop representative by [step 1.1], hence lies in the image. If a loop in ${\mathrm{\Sigma }}^2$ maps to the identity, [step 2.1] makes it null-homotopic in ${\mathrm{\Sigma }}^2$, so $j_{\ast }$ is injective. Its induced homomorphism is defined by [F6].

The graph ${\mathrm{\Sigma }}^1$ is connected because its vertices are $W$ and $S$ generates $W$ [F1, F7]. Every closed cell is a convex polytope containing its vertex $w{W}_{\mathrm{\varnothing }}=\{w\}$ as a face [F7], and each point of $\mathrm{\Sigma }$ lies in such a cell; a segment in that cell joins the point to a vertex of ${\mathrm{\Sigma }}^1$. Hence $\mathrm{\Sigma }$ is path-connected. For an arbitrary basepoint $x$, choose a path $p$ from $x$ to $1$ and a loop $\alpha$ at $x$. The loop $\bar{p}\ast \alpha \ast p$ at $1$ is homotopic rel basepoint to an edge loop by [step 1.1], then contracts by [step 2.2]. Prepending $p$ and appending $\bar{p}$ to that based null-homotopy gives a homotopy rel $x$ from $(p\ast \bar{p})\ast \alpha \ast (p\ast \bar{p})$ to $p\ast \bar{p}$, after reparameterizing concatenations. The loop $p\ast \bar{p}$ contracts rel $x$ by the homotopy $G(u,t)=p(2u(1-t))$ for $u\le \frac{1}{2}$ and $G(u,t)=p(2(1-u)(1-t))$ for $u\ge \frac{1}{2}$: the formulas agree at $u=\frac{1}{2}$, are continuous, and keep both endpoints at $x$. Hence $(p\ast \bar{p})\ast \alpha \ast (p\ast \bar{p})$ is null-homotopic and is also homotopic rel $x$ to $\alpha$ by contracting its two outer copies of $p\ast \bar{p}$. Thus $\alpha$ is null-homotopic, and every fundamental group of $\mathrm{\Sigma }$ is trivial.

The CW complex $\mathrm{\Sigma }$ is nonempty, path-connected and has trivial fundamental groups by [step 3.2], so it is simply connected; [step 3.1] then gives triviality of ${\pi }_1({\mathrm{\Sigma }}^2,v)$ and the asserted inclusion isomorphism for every vertex $v$, while [step 2.2] gives the explicit basepoint case ${\pi }_1({\mathrm{\Sigma }}^2,1)=1$. The cellular approximations use finite relative sources and [F3] is explicitly choice-free in that case; the normal-closure product and all word reductions are finite, and the path $p$ in [step 3.2] is chosen separately for one basepoint. No Axiom of Choice is used.