Skip to content

Commit 2b473a0

Browse files
ecavalloecavallo
committed
Deploying to gh-pages from @ 35d2919 🚀
1 parent d4289d1 commit 2b473a0

File tree

87 files changed

+6121
-5387
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

87 files changed

+6121
-5387
lines changed

‎Cubical.CW.ChainComplex.html‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -142,17 +142,17 @@
142142
<a id="6117" class="Keyword">where</a>
143143
<a id="6131" href="Cubical.CW.ChainComplex.html#6131" class="Function">cofibCW-exactness↑</a> <a id="6150" class="Symbol">:</a> <a id="6152" href="Cubical.HITs.Susp.Base.html#682" class="Function">suspFun</a> <a id="6160" class="Symbol">(</a><a id="6161" href="Cubical.CW.Base.html#4274" class="Function">δ</a> <a id="6163" class="Symbol">(</a><a id="6164" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="6168" href="Cubical.CW.ChainComplex.html#4350" class="Bound">n</a><a id="6169" class="Symbol">)</a> <a id="6171" href="Cubical.CW.ChainComplex.html#1441" class="Bound">C</a><a id="6172" class="Symbol">)</a> <a id="6174" href="Cubical.Foundations.Function.html#665" class="Function Operator">∘</a> <a id="6176" href="Cubical.HITs.Susp.Base.html#682" class="Function">suspFun</a> <a id="6184" class="Symbol">(</a><a id="6185" href="Cubical.CW.Base.html#3970" class="Function Operator">to_cofibCW</a> <a id="6196" class="Symbol">(</a><a id="6197" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="6201" href="Cubical.CW.ChainComplex.html#4350" class="Bound">n</a><a id="6202" class="Symbol">)</a> <a id="6204" href="Cubical.CW.ChainComplex.html#1441" class="Bound">C</a><a id="6205" class="Symbol">)</a>
144144
<a id="6236" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="6238" class="Symbol">λ</a> <a id="6240" href="Cubical.CW.ChainComplex.html#6240" class="Bound">x</a> <a id="6242" class="Symbol">→</a> <a id="6244" href="Cubical.HITs.Susp.Base.html#536" class="InductiveConstructor">north</a>
145-
<a id="6258" href="Cubical.CW.ChainComplex.html#6131" class="Function">cofibCW-exactness↑</a> <a id="6277" class="Symbol">=</a> <a id="6279" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="6283" class="Symbol">(</a><a id="6284" href="Cubical.HITs.Susp.Properties.html#675" class="Function">suspFunComp</a> <a id="6296" class="Symbol">_</a> <a id="6298" class="Symbol">_)</a>
145+
<a id="6258" href="Cubical.CW.ChainComplex.html#6131" class="Function">cofibCW-exactness↑</a> <a id="6277" class="Symbol">=</a> <a id="6279" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="6283" class="Symbol">(</a><a id="6284" href="Cubical.HITs.Susp.Properties.html#781" class="Function">suspFunComp</a> <a id="6296" class="Symbol">_</a> <a id="6298" class="Symbol">_)</a>
146146
<a id="6330" href="Cubical.Foundations.Prelude.html#4007" class="Function Operator">∙∙</a> <a id="6333" href="Cubical.Foundations.Prelude.html#1697" class="Function">congS</a> <a id="6339" href="Cubical.HITs.Susp.Base.html#682" class="Function">suspFun</a> <a id="6347" href="Cubical.CW.ChainComplex.html#4644" class="Function">cofibCW-exactness</a>
147-
<a id="6394" href="Cubical.Foundations.Prelude.html#4007" class="Function Operator">∙∙</a> <a id="6397" href="Cubical.HITs.Susp.Properties.html#891" class="Function">suspFunConst</a> <a id="6410" href="Cubical.HITs.Susp.Base.html#536" class="InductiveConstructor">north</a>
147+
<a id="6394" href="Cubical.Foundations.Prelude.html#4007" class="Function Operator">∙∙</a> <a id="6397" href="Cubical.HITs.Susp.Properties.html#997" class="Function">suspFunConst</a> <a id="6410" href="Cubical.HITs.Susp.Base.html#536" class="InductiveConstructor">north</a>
148148

149149
<a id="6425" href="Cubical.CW.ChainComplex.html#6425" class="Function">iso-cancel-1</a> <a id="6438" class="Symbol">:</a> <a id="6440" href="Cubical.HITs.Susp.Base.html#682" class="Function">suspFun</a> <a id="6448" class="Symbol">(</a><a id="6449" href="Cubical.CW.ChainComplex.html#2805" class="Function">isoCofBouquetInv↑</a> <a id="6467" href="Cubical.CW.ChainComplex.html#4350" class="Bound">n</a><a id="6468" class="Symbol">)</a> <a id="6470" href="Cubical.Foundations.Function.html#665" class="Function Operator">∘</a> <a id="6472" href="Cubical.HITs.Susp.Base.html#682" class="Function">suspFun</a> <a id="6480" class="Symbol">(</a><a id="6481" href="Cubical.CW.ChainComplex.html#2523" class="Function">isoCofBouquet</a> <a id="6495" class="Symbol">(</a><a id="6496" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="6500" href="Cubical.CW.ChainComplex.html#4350" class="Bound">n</a><a id="6501" class="Symbol">))</a>
150150
<a id="6527" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="6529" class="Symbol">λ</a> <a id="6531" href="Cubical.CW.ChainComplex.html#6531" class="Bound">x</a> <a id="6533" class="Symbol">→</a> <a id="6535" href="Cubical.CW.ChainComplex.html#6531" class="Bound">x</a>
151-
<a id="6545" href="Cubical.CW.ChainComplex.html#6425" class="Function">iso-cancel-1</a> <a id="6558" class="Symbol">=</a> <a id="6560" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="6564" class="Symbol">(</a><a id="6565" href="Cubical.HITs.Susp.Properties.html#675" class="Function">suspFunComp</a> <a id="6577" class="Symbol">_</a> <a id="6579" class="Symbol">_)</a>
151+
<a id="6545" href="Cubical.CW.ChainComplex.html#6425" class="Function">iso-cancel-1</a> <a id="6558" class="Symbol">=</a> <a id="6560" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="6564" class="Symbol">(</a><a id="6565" href="Cubical.HITs.Susp.Properties.html#781" class="Function">suspFunComp</a> <a id="6577" class="Symbol">_</a> <a id="6579" class="Symbol">_)</a>
152152
<a id="6605" href="Cubical.Foundations.Prelude.html#4007" class="Function Operator">∙∙</a> <a id="6608" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="6613" href="Cubical.HITs.Susp.Base.html#682" class="Function">suspFun</a> <a id="6621" class="Symbol">(λ</a> <a id="6624" href="Cubical.CW.ChainComplex.html#6624" class="Bound">i</a> <a id="6626" href="Cubical.CW.ChainComplex.html#6626" class="Bound">x</a> <a id="6628" class="Symbol">→</a> <a id="6630" href="Cubical.Foundations.Isomorphism.html#942" class="Field">Iso.leftInv</a>
153153
<a id="6670" class="Symbol">(</a><a id="6671" href="Cubical.HITs.SphereBouquet.Properties.html#15990" class="Function">BouquetIso-gen</a> <a id="6686" class="Symbol">(</a><a id="6687" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="6691" href="Cubical.CW.ChainComplex.html#4350" class="Bound">n</a><a id="6692" class="Symbol">)</a> <a id="6694" class="Symbol">(</a><a id="6695" href="Cubical.CW.ChainComplex.html#1743" class="Function">An+1</a> <a id="6700" href="Cubical.CW.ChainComplex.html#4350" class="Bound">n</a><a id="6701" class="Symbol">)</a> <a id="6703" class="Symbol">(</a><a id="6704" href="Cubical.CW.ChainComplex.html#1804" class="Function">αn+1</a> <a id="6709" href="Cubical.CW.ChainComplex.html#4350" class="Bound">n</a><a id="6710" class="Symbol">)</a>
154154
<a id="6756" class="Symbol">(</a><a id="6757" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="6761" href="Cubical.CW.ChainComplex.html#1441" class="Bound">C</a> <a id="6763" class="Symbol">.</a><a id="6764" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="6768" class="Symbol">.</a><a id="6769" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="6773" class="Symbol">.</a><a id="6774" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="6778" class="Symbol">(</a><a id="6779" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="6783" href="Cubical.CW.ChainComplex.html#4350" class="Bound">n</a><a id="6784" class="Symbol">)))</a> <a id="6788" href="Cubical.CW.ChainComplex.html#6626" class="Bound">x</a> <a id="6790" href="Cubical.CW.ChainComplex.html#6624" class="Bound">i</a><a id="6791" class="Symbol">)</a>
155-
<a id="6816" href="Cubical.Foundations.Prelude.html#4007" class="Function Operator">∙∙</a> <a id="6819" href="Cubical.HITs.Susp.Properties.html#1074" class="Function">suspFunIdFun</a>
155+
<a id="6816" href="Cubical.Foundations.Prelude.html#4007" class="Function Operator">∙∙</a> <a id="6819" href="Cubical.HITs.Susp.Properties.html#1180" class="Function">suspFunIdFun</a>
156156
<a id="6840" href="Cubical.CW.ChainComplex.html#6840" class="Function">iso-cancel-2</a> <a id="6853" class="Symbol">:</a> <a id="6855" class="Symbol">(</a><a id="6856" href="Cubical.CW.ChainComplex.html#2337" class="Function">isoSuspBouquetInv↑</a> <a id="6875" href="Cubical.CW.ChainComplex.html#4350" class="Bound">n</a><a id="6876" class="Symbol">)</a> <a id="6878" href="Cubical.Foundations.Function.html#665" class="Function Operator">∘</a> <a id="6880" class="Symbol">(</a><a id="6881" href="Cubical.CW.ChainComplex.html#1842" class="Function">isoSuspBouquet</a> <a id="6896" class="Symbol">(</a><a id="6897" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="6901" href="Cubical.CW.ChainComplex.html#4350" class="Bound">n</a><a id="6902" class="Symbol">))</a> <a id="6905" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="6907" class="Symbol">λ</a> <a id="6909" href="Cubical.CW.ChainComplex.html#6909" class="Bound">x</a> <a id="6911" class="Symbol">→</a> <a id="6913" href="Cubical.CW.ChainComplex.html#6909" class="Bound">x</a>
157157
<a id="6923" href="Cubical.CW.ChainComplex.html#6840" class="Function">iso-cancel-2</a> <a id="6936" href="Cubical.CW.ChainComplex.html#6936" class="Bound">i</a> <a id="6938" href="Cubical.CW.ChainComplex.html#6938" class="Bound">x</a> <a id="6940" class="Symbol">=</a> <a id="6942" href="Cubical.Foundations.Isomorphism.html#942" class="Field">Iso.leftInv</a> <a id="6954" href="Cubical.HITs.SphereBouquet.Properties.html#4545" class="Function">sphereBouquetSuspIso</a> <a id="6975" href="Cubical.CW.ChainComplex.html#6938" class="Bound">x</a> <a id="6977" href="Cubical.CW.ChainComplex.html#6936" class="Bound">i</a>
158158

0 commit comments

Comments
 (0)