this repo has no description

Lemma 41: strengthening to a quasi-inverse #3

merged opened by jonmsterling.com targeting main from push-sxlklnpmzkpy

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.

Labels

None yet.

assignee

None yet.

Participants 1
AT URI
at://did:plc:jjiv56ot7d6sgethto3jr3r5/sh.tangled.repo.pull/3mcrtyskrfp22
+45 -2
Diff #0
+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{ ··· 180 180 }{\Rx{\gA}{x}} 181 181 } 182 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} 224 + } 225 + \commentrow{by reflexivity} 183 226 \qedhere 184 227 } 185 228 }

History

1 round 0 comments
sign up or login to add to the discussion
jonmsterling.com submitted #0
1 commit
expand
Lemma 41: strengthening to a quasi-inverse
expand 0 comments
pull request successfully merged