jonmsterling.com
this repo has no description
Lemma 41: strengthening to a quasi-inverse
The previous version of this claimed a retraction, but in fact only
constructed a section. I will just construct both a section and a
retraction.
From Ian Ray.
+45
-2
+45
-2
nodes/path-objects.tex
+45
-2
nodes/path-objects.tex
···
87
87
\end{construction}
88
88
89
89
\begin{lemma}[From edges to identifications via propositional fans]\label[lemma]{lem:edge-to-id}
90
-
Suppose that each fan $\Fan{\gA}{x}$ of a reflexive graph $\gA$ is a proposition. Then each $\IdToEdge{\gA}[x,y]{-}$ has a retraction $\EdgeToId{\gA}[x,y]{-} \colon x\Edge{\gA}y\to \Id{\vrt{\gA}}{x}{y}$.
90
+
Suppose that each fan $\Fan{\gA}{x}$ of a reflexive graph $\gA$ is a proposition. Then each $\IdToEdge{\gA}[x,y]{-}$ has a quasi-inverse $\EdgeToId{\gA}[x,y]{-} \colon x\Edge{\gA}y\to \Id{\vrt{\gA}}{x}{y}$.
91
91
\end{lemma}
92
92
\begin{proof}
93
93
Let $\Phi_x$ be the proof that a given fan $\Fan{\gA}{x}$ is a proposition. Rather than defining $\EdgeToId{\gA}[x,y]{-} : x\Edge{\gA}y\to \Id{\vrt{\gA}}{x}{y}$ directly, we construct a slightly more general function that anticipates the contractibility of $\Fan{\gA}{x}$.
···
127
127
}
128
128
}
129
129
130
-
Next we exhibit the witness of retraction.
130
+
Next we prove that $\EdgeToId{\gA}[x,y]{-}$ is a section of $\IdToEdge{\gA}[x,y]{-}$.
131
131
132
132
\iblock{
133
133
\mhang{
···
178
178
\Id{x\Edge{\gA}x}{
179
179
\Rx{\gA}{x}
180
180
}{\Rx{\gA}{x}}
181
+
}
182
+
\commentrow{by reflexivity}
183
+
}
184
+
}
185
+
186
+
Finally, we prove that $\EdgeToId{\gA}[x,y]{-}$ is a retraction of $\IdToEdge{\gA}[x,y]{-}$.
187
+
188
+
\iblock{
189
+
\mhang{
190
+
x,y:\vrt{\gA}; p : \Id{\vrt{\gA}}{x}{y}
191
+
\vdash \Id{\Id{\vrt{A}}{x}{y}}{\EdgeToId{\gA}[x,y]{\IdToEdge{\gA}[x,y]{p}}}{p}
192
+
}{
193
+
\commentrow{by identification induction}
194
+
\mrow{
195
+
x:\vrt{\gA} \vdash
196
+
\Id{\Id{\vrt{A}}{x}{x}}{\EdgeToId{\gA}[x,x]{\IdToEdge{\gA}[x,x]{\Refl}}}{\Refl}
197
+
}
198
+
\commentrow{by definition}
199
+
\mrow{
200
+
x:\vrt{\gA} \vdash
201
+
\Id{\Id{\vrt{A}}{x}{x}}{
202
+
\EdgeToIdGen{\gA}[x,x]{
203
+
\Rx{\gA}x
204
+
}{
205
+
\Phi_x\,(x,\Rx{\gA}x)\,(x,\Rx{\gA}x)
206
+
}
207
+
}{\Refl}
208
+
}
209
+
\commentrow{because $\Fan{\gA}{x}$ is a set}
210
+
\mrow{
211
+
x:\vrt{\gA} \vdash
212
+
\Id{\Id{\vrt{A}}{x}{x}}{
213
+
\EdgeToIdGen{\gA}[x,x]{
214
+
\Rx{\gA}x
215
+
}{
216
+
\Refl
217
+
}
218
+
}{\Refl}
219
+
}
220
+
\commentrow{by definition}
221
+
\mrow{
222
+
x:\vrt{\gA} \vdash
223
+
\Id{\Id{\vrt{A}}{x}{x}}{\Refl}{\Refl}
181
224
}
182
225
\commentrow{by reflexivity}
183
226
\qedhere