Skip to content

Commit

Permalink
Deploying to gh-pages from @ e2cf0ab 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@mortberg
mortberg committed Sep 2, 2024
1 parent b955479 commit 32951fb
Show file tree
Hide file tree
Showing 58 changed files with 5,845 additions and 3,695 deletions.
8 changes: 4 additions & 4 deletions Cubical.CW.Approximation.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -147,7 +147,7 @@
<a id="5013" href="Cubical.Foundations.Equiv.html#3136" class="Function">invEq</a> <a id="5019" href="Cubical.HITs.Truncation.Properties.html#13091" class="Function">propTrunc≃Trunc1</a>
<a id="5043" class="Symbol">(</a><a id="5044" href="Cubical.Foundations.Equiv.html#3136" class="Function">invEq</a> <a id="5050" class="Symbol">(_</a> <a id="5053" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="5055" href="Cubical.Axiom.Choice.html#3903" class="Function">InductiveFinSatAC</a> <a id="5073" class="Number">1</a> <a id="5075" class="Symbol">(</a><a id="5076" href="Cubical.CW.Base.html#1366" class="Function">CWskel-fields.card</a> <a id="5095" href="Cubical.CW.Approximation.html#3039" class="Bound">C</a> <a id="5097" class="Symbol">(</a><a id="5098" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="5102" href="Cubical.CW.Approximation.html#4346" class="Bound">m</a><a id="5103" class="Symbol">))</a> <a id="5106" class="Symbol">_)</a>
<a id="5117" class="Symbol">λ</a> <a id="5119" href="Cubical.CW.Approximation.html#5119" class="Bound">a</a> <a id="5121" class="Symbol">→</a> <a id="5123" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="5127" href="Cubical.HITs.Truncation.Properties.html#13091" class="Function">propTrunc≃Trunc1</a>
<a id="5155" class="Symbol">(</a><a id="5156" href="Cubical.HITs.Sn.Properties.html#16495" class="Function">sphereToTrunc</a> <a id="5170" href="Cubical.CW.Approximation.html#4346" class="Bound">m</a> <a id="5172" class="Symbol">λ</a> <a id="5174" href="Cubical.CW.Approximation.html#5174" class="Bound">y</a> <a id="5176" class="Symbol">→</a>
<a id="5155" class="Symbol">(</a><a id="5156" href="Cubical.HITs.Sn.Properties.html#16912" class="Function">sphereToTrunc</a> <a id="5170" href="Cubical.CW.Approximation.html#4346" class="Bound">m</a> <a id="5172" class="Symbol">λ</a> <a id="5174" href="Cubical.CW.Approximation.html#5174" class="Bound">y</a> <a id="5176" class="Symbol">→</a>
<a id="5191" href="Cubical.HITs.Truncation.Properties.html#11512" class="Function">TR.map</a> <a id="5198" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="5202" class="Symbol">(</a><a id="5203" href="Cubical.Homotopy.Connected.html#13736" class="Function">isConnectedCong</a> <a id="5219" class="Symbol">_</a> <a id="5221" class="Symbol">_</a> <a id="5223" class="Symbol">(</a><a id="5224" href="Cubical.CW.Properties.html#8874" class="Function">isConnected-CW↪∞</a> <a id="5241" class="Symbol">(</a><a id="5242" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="5246" class="Symbol">(</a><a id="5247" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="5251" href="Cubical.CW.Approximation.html#4346" class="Bound">m</a><a id="5252" class="Symbol">))</a> <a id="5255" href="Cubical.CW.Approximation.html#3054" class="Bound">D</a><a id="5256" class="Symbol">)</a>
<a id="5279" class="Symbol">(</a><a id="5280" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="5284" class="Symbol">(</a><a id="5285" href="Cubical.HITs.SequentialColimit.Base.html#455" class="InductiveConstructor">push</a> <a id="5290" class="Symbol">_)</a>
<a id="5314" href="Cubical.Foundations.Prelude.html#4776" class="Function Operator">∙</a> <a id="5316" class="Symbol">(</a><a id="5317" href="Cubical.CW.Approximation.html#5002" class="Bound">fh</a> <a id="5320" class="Symbol">(</a><a id="5321" href="Cubical.CW.Base.html#1404" class="Function">CWskel-fields.α</a> <a id="5337" href="Cubical.CW.Approximation.html#3039" class="Bound">C</a> <a id="5339" class="Symbol">(</a><a id="5340" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="5344" href="Cubical.CW.Approximation.html#4346" class="Bound">m</a><a id="5345" class="Symbol">)</a> <a id="5347" class="Symbol">(</a><a id="5348" href="Cubical.CW.Approximation.html#5119" class="Bound">a</a> <a id="5350" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="5352" href="Cubical.CW.Approximation.html#5174" class="Bound">y</a><a id="5353" class="Symbol">))</a>
Expand Down Expand Up @@ -191,8 +191,8 @@
<a id="7200" class="Symbol">(</a><a id="7201" href="Cubical.CW.Approximation.html#6341" class="Function">fib-f-r</a> <a id="7209" href="Cubical.CW.Approximation.html#7029" class="Bound">x</a><a id="7210" class="Symbol">))</a> <a id="7213" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥₁</a>
<a id="7224" href="Cubical.CW.Approximation.html#7008" class="Function">mere-fib-f-coh</a> <a id="7239" class="Symbol">=</a> <a id="7241" href="Cubical.Foundations.Equiv.html#3136" class="Function">invEq</a> <a id="7247" href="Cubical.HITs.Truncation.Properties.html#13091" class="Function">propTrunc≃Trunc1</a>
<a id="7274" class="Symbol">(</a><a id="7275" href="Cubical.Foundations.Equiv.html#3136" class="Function">invEq</a> <a id="7281" class="Symbol">(_</a> <a id="7284" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="7286" href="Cubical.Axiom.Choice.html#3903" class="Function">InductiveFinSatAC</a> <a id="7304" class="Number">1</a> <a id="7306" class="Symbol">(</a><a id="7307" href="Cubical.CW.Base.html#1366" class="Function">card</a> <a id="7312" class="Symbol">(</a><a id="7313" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="7317" href="Cubical.CW.Approximation.html#4346" class="Bound">m</a><a id="7318" class="Symbol">))</a> <a id="7321" class="Symbol">_)</a>
<a id="7336" class="Symbol">λ</a> <a id="7338" href="Cubical.CW.Approximation.html#7338" class="Bound">a</a> <a id="7340" class="Symbol">→</a> <a id="7342" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="7346" href="Cubical.HITs.Truncation.Properties.html#13091" class="Function">propTrunc≃Trunc1</a> <a id="7363" class="Symbol">(</a><a id="7364" href="Cubical.HITs.Sn.Properties.html#16495" class="Function">sphereToTrunc</a> <a id="7378" href="Cubical.CW.Approximation.html#4346" class="Bound">m</a>
<a id="7394" class="Symbol">(</a><a id="7395" href="Cubical.HITs.Sn.Properties.html#3503" class="Function">sphereElim&#39;</a> <a id="7407" href="Cubical.CW.Approximation.html#4346" class="Bound">m</a>
<a id="7336" class="Symbol">λ</a> <a id="7338" href="Cubical.CW.Approximation.html#7338" class="Bound">a</a> <a id="7340" class="Symbol">→</a> <a id="7342" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="7346" href="Cubical.HITs.Truncation.Properties.html#13091" class="Function">propTrunc≃Trunc1</a> <a id="7363" class="Symbol">(</a><a id="7364" href="Cubical.HITs.Sn.Properties.html#16912" class="Function">sphereToTrunc</a> <a id="7378" href="Cubical.CW.Approximation.html#4346" class="Bound">m</a>
<a id="7394" class="Symbol">(</a><a id="7395" href="Cubical.HITs.Sn.Properties.html#3920" class="Function">sphereElim&#39;</a> <a id="7407" href="Cubical.CW.Approximation.html#4346" class="Bound">m</a>
<a id="7425" class="Symbol">(λ</a> <a id="7428" href="Cubical.CW.Approximation.html#7428" class="Bound">x</a> <a id="7430" class="Symbol">→</a> <a id="7432" href="Cubical.Foundations.HLevels.html#9402" class="Function">isOfHLevelRetractFromIso</a> <a id="7457" href="Cubical.CW.Approximation.html#4346" class="Bound">m</a>
<a id="7475" class="Symbol">(</a><a id="7476" href="Cubical.Foundations.Isomorphism.html#3376" class="Function">invIso</a> <a id="7483" class="Symbol">(</a><a id="7484" href="Cubical.HITs.Truncation.Properties.html#20536" class="Function">PathPIdTruncIso</a> <a id="7500" class="Symbol">(</a><a id="7501" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="7505" href="Cubical.CW.Approximation.html#4346" class="Bound">m</a><a id="7506" class="Symbol">)))</a>
<a id="7526" class="Symbol">(</a><a id="7527" href="Cubical.Foundations.HLevels.html#10084" class="Function">isOfHLevelPathP&#39;</a> <a id="7544" href="Cubical.CW.Approximation.html#4346" class="Bound">m</a> <a id="7546" class="Symbol">(</a><a id="7547" href="Cubical.Foundations.HLevels.html#2962" class="Function">isProp→isOfHLevelSuc</a> <a id="7568" href="Cubical.CW.Approximation.html#4346" class="Bound">m</a>
Expand Down Expand Up @@ -521,7 +521,7 @@
<a id="21451" href="Cubical.Foundations.Isomorphism.html#895" class="Field">Iso.inv</a> <a id="21459" href="Cubical.HITs.Truncation.Properties.html#12736" class="Function">propTruncTrunc1Iso</a>
<a id="21486" class="Symbol">(</a><a id="21487" href="Cubical.Foundations.Equiv.html#3136" class="Function">invEq</a> <a id="21493" class="Symbol">(_</a> <a id="21496" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="21498" href="Cubical.Axiom.Choice.html#3903" class="Function">InductiveFinSatAC</a> <a id="21516" class="Number">1</a> <a id="21518" class="Symbol">_</a> <a id="21520" class="Symbol">_)</a>
<a id="21531" class="Symbol">λ</a> <a id="21533" href="Cubical.CW.Approximation.html#21533" class="Bound">x</a> <a id="21535" class="Symbol">→</a> <a id="21537" href="Cubical.Foundations.Isomorphism.html#879" class="Field">Iso.fun</a> <a id="21545" href="Cubical.HITs.Truncation.Properties.html#12736" class="Function">propTruncTrunc1Iso</a>
<a id="21580" class="Symbol">(</a><a id="21581" href="Cubical.HITs.Sn.Properties.html#16495" class="Function">sphereToTrunc</a> <a id="21595" href="Cubical.CW.Approximation.html#14378" class="Bound">n&#39;</a> <a id="21598" class="Symbol">(</a><a id="21599" href="Cubical.CW.Approximation.html#19148" class="Function">fiber-cong²-hₙ₊₁-push∞</a> <a id="21622" href="Cubical.CW.Approximation.html#21533" class="Bound">x</a><a id="21623" class="Symbol">)))</a>
<a id="21580" class="Symbol">(</a><a id="21581" href="Cubical.HITs.Sn.Properties.html#16912" class="Function">sphereToTrunc</a> <a id="21595" href="Cubical.CW.Approximation.html#14378" class="Bound">n&#39;</a> <a id="21598" class="Symbol">(</a><a id="21599" href="Cubical.CW.Approximation.html#19148" class="Function">fiber-cong²-hₙ₊₁-push∞</a> <a id="21622" href="Cubical.CW.Approximation.html#21533" class="Bound">x</a><a id="21623" class="Symbol">)))</a>

<a id="21632" class="Keyword">module</a> <a id="21639" href="Cubical.CW.Approximation.html#21639" class="Module">_</a> <a id="21641" class="Symbol">(</a><a id="21642" href="Cubical.CW.Approximation.html#21642" class="Bound">q</a> <a id="21644" class="Symbol">:</a> <a id="21646" class="Symbol">(</a><a id="21647" href="Cubical.CW.Approximation.html#21647" class="Bound">x</a> <a id="21649" class="Symbol">:</a> <a id="21651" href="Cubical.Data.Fin.Inductive.Base.html#453" class="Function">Fin</a> <a id="21655" class="Symbol">(</a><a id="21656" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="21660" class="Symbol">(</a><a id="21661" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="21665" href="Cubical.CW.Approximation.html#11743" class="Bound">C</a><a id="21666" class="Symbol">)</a> <a id="21668" class="Symbol">(</a><a id="21669" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="21673" href="Cubical.CW.Approximation.html#14378" class="Bound">n&#39;</a><a id="21675" class="Symbol">)))</a> <a id="21679" class="Symbol">(</a><a id="21680" href="Cubical.CW.Approximation.html#21680" class="Bound">y</a> <a id="21682" class="Symbol">:</a> <a id="21684" href="Cubical.HITs.Sn.Base.html#389" class="Function">S₊</a> <a id="21687" href="Cubical.CW.Approximation.html#14378" class="Bound">n&#39;</a><a id="21689" class="Symbol">)</a>
<a id="21707" class="Symbol">→</a> <a id="21709" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="21715" class="Symbol">(</a><a id="21716" href="Cubical.CW.Approximation.html#17823" class="Function">cong²</a> <a id="21722" href="Cubical.CW.Approximation.html#21647" class="Bound">x</a> <a id="21724" href="Cubical.CW.Approximation.html#21680" class="Bound">y</a><a id="21725" class="Symbol">)</a> <a id="21727" class="Symbol">(</a><a id="21728" href="Cubical.CW.Approximation.html#18272" class="Function">hₙ₊₁-push∞</a> <a id="21739" href="Cubical.CW.Approximation.html#21647" class="Bound">x</a> <a id="21741" href="Cubical.CW.Approximation.html#21680" class="Bound">y</a><a id="21742" class="Symbol">))</a> <a id="21745" class="Keyword">where</a>
Expand Down
2 changes: 1 addition & 1 deletion Cubical.CW.Properties.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -240,7 +240,7 @@

<a id="8617" href="Cubical.CW.Properties.html#8617" class="Function">inPushoutConnected</a> <a id="8636" class="Symbol">:</a> <a id="8638" href="Cubical.Homotopy.Connected.html#1532" class="Function">isConnectedFun</a> <a id="8653" class="Symbol">(</a><a id="8654" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="8658" href="Cubical.CW.Properties.html#8191" class="Bound">n</a><a id="8659" class="Symbol">)</a> <a id="8661" href="Cubical.CW.Properties.html#8401" class="Function">inPushout</a>
<a id="8675" href="Cubical.CW.Properties.html#8617" class="Function">inPushoutConnected</a> <a id="8694" class="Symbol">=</a> <a id="8696" href="Cubical.Homotopy.Connected.html#25305" class="Function">inlConnected</a> <a id="8709" class="Symbol">(</a><a id="8710" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="8714" href="Cubical.CW.Properties.html#8191" class="Bound">n</a><a id="8715" class="Symbol">)</a> <a id="8717" class="Symbol">(</a><a id="8718" href="Cubical.CW.Properties.html#8346" class="Function">α</a> <a id="8720" class="Symbol">(</a><a id="8721" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="8725" href="Cubical.CW.Properties.html#8191" class="Bound">n</a><a id="8726" class="Symbol">))</a> <a id="8729" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a>
<a id="8739" class="Symbol">λ</a> <a id="8741" href="Cubical.CW.Properties.html#8741" class="Bound">b</a> <a id="8743" class="Symbol">→</a> <a id="8745" href="Cubical.Foundations.Prelude.html#9797" class="Function">subst</a> <a id="8751" class="Symbol">(</a><a id="8752" href="Cubical.Homotopy.Connected.html#1432" class="Function">isConnected</a> <a id="8764" class="Symbol">(</a><a id="8765" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="8769" href="Cubical.CW.Properties.html#8191" class="Bound">n</a><a id="8770" class="Symbol">))</a> <a id="8773" class="Symbol">(</a><a id="8774" href="Cubical.CW.Properties.html#8482" class="Function">fstProjPath</a> <a id="8786" href="Cubical.CW.Properties.html#8741" class="Bound">b</a><a id="8787" class="Symbol">)</a> <a id="8789" class="Symbol">(</a><a id="8790" href="Cubical.HITs.Sn.Properties.html#16251" class="Function">sphereConnected</a> <a id="8806" href="Cubical.CW.Properties.html#8191" class="Bound">n</a><a id="8807" class="Symbol">)</a>
<a id="8739" class="Symbol">λ</a> <a id="8741" href="Cubical.CW.Properties.html#8741" class="Bound">b</a> <a id="8743" class="Symbol">→</a> <a id="8745" href="Cubical.Foundations.Prelude.html#9797" class="Function">subst</a> <a id="8751" class="Symbol">(</a><a id="8752" href="Cubical.Homotopy.Connected.html#1432" class="Function">isConnected</a> <a id="8764" class="Symbol">(</a><a id="8765" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="8769" href="Cubical.CW.Properties.html#8191" class="Bound">n</a><a id="8770" class="Symbol">))</a> <a id="8773" class="Symbol">(</a><a id="8774" href="Cubical.CW.Properties.html#8482" class="Function">fstProjPath</a> <a id="8786" href="Cubical.CW.Properties.html#8741" class="Bound">b</a><a id="8787" class="Symbol">)</a> <a id="8789" class="Symbol">(</a><a id="8790" href="Cubical.HITs.Sn.Properties.html#16668" class="Function">sphereConnected</a> <a id="8806" href="Cubical.CW.Properties.html#8191" class="Bound">n</a><a id="8807" class="Symbol">)</a>

<a id="8810" class="Comment">-- The embedding of stage n into the colimit is (n+1)-connected</a>
<a id="isConnected-CW↪∞"></a><a id="8874" href="Cubical.CW.Properties.html#8874" class="Function">isConnected-CW↪∞</a> <a id="8891" class="Symbol">:</a> <a id="8893" class="Symbol">(</a><a id="8894" href="Cubical.CW.Properties.html#8894" class="Bound">n</a> <a id="8896" class="Symbol">:</a> <a id="8898" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a><a id="8899" class="Symbol">)</a> <a id="8901" class="Symbol">(</a><a id="8902" href="Cubical.CW.Properties.html#8902" class="Bound">C</a> <a id="8904" class="Symbol">:</a> <a id="8906" href="Cubical.CW.Base.html#1233" class="Function">CWskel</a> <a id="8913" href="Cubical.CW.Properties.html#1413" class="Generalizable">ℓ</a><a id="8914" class="Symbol">)</a> <a id="8916" class="Symbol">→</a> <a id="8918" href="Cubical.Homotopy.Connected.html#1532" class="Function">isConnectedFun</a> <a id="8933" href="Cubical.CW.Properties.html#8894" class="Bound">n</a> <a id="8935" class="Symbol">(</a><a id="8936" href="Cubical.CW.Base.html#4318" class="Function">CW↪∞</a> <a id="8941" href="Cubical.CW.Properties.html#8902" class="Bound">C</a> <a id="8943" href="Cubical.CW.Properties.html#8894" class="Bound">n</a><a id="8944" class="Symbol">)</a>
Expand Down
Loading

0 comments on commit 32951fb

Please sign in to comment.