Deploying to gh-pages from @ a126e3f 🚀

Author: felixwellen

Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html

@@ -124,7 +124,7 @@
 
   <a id="DecIndec-BaseProperties.πₖ-id"></a><a id="4525" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4525" class="Function">πₖ-id</a> <a id="4531" class="Symbol">:</a> <a id="4533" class="Symbol">{</a><a id="4534" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4534" class="Bound">k</a> <a id="4536" class="Symbol">:</a> <a id="4538" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#3680" class="Bound">Idx</a><a id="4541" class="Symbol">}</a> <a id="4543" class="Symbol">→</a> <a id="4545" class="Symbol">(</a><a id="4546" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4546" class="Bound">a</a> <a id="4548" class="Symbol">:</a> <a id="4550" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#3724" class="Bound">G</a> <a id="4552" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4534" class="Bound">k</a><a id="4553" class="Symbol">)</a> <a id="4555" class="Symbol">→</a> <a id="4557" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#3845" class="Function">πₖ</a> <a id="4560" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4534" class="Bound">k</a> <a id="4562" class="Symbol">(</a><a id="4563" href="Cubical.Algebra.DirectSum.DirectSumHIT.Base.html#618" class="InductiveConstructor">base</a> <a id="4568" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4534" class="Bound">k</a> <a id="4570" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4546" class="Bound">a</a><a id="4571" class="Symbol">)</a> <a id="4573" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="4575" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4546" class="Bound">a</a>
   <a id="4579" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4525" class="Function">πₖ-id</a> <a id="4585" class="Symbol">{</a><a id="4586" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4586" class="Bound">k</a><a id="4587" class="Symbol">}</a> <a id="4589" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4589" class="Bound">a</a> <a id="4591" class="Keyword">with</a> <a id="4596" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#3698" class="Bound">decIdx</a> <a id="4603" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4586" class="Bound">k</a> <a id="4605" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4586" class="Bound">k</a>
-  <a id="4609" class="Symbol">...</a> <a id="4613" class="Symbol">|</a> <a id="4615" href="Cubical.Relation.Nullary.Base.html#478" class="InductiveConstructor">yes</a> <a id="4619" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4619" class="Bound">p</a> <a id="4621" class="Symbol">=</a> <a id="4623" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="4628" class="Symbol">(λ</a> <a id="4631" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4631" class="Bound">X</a> <a id="4633" class="Symbol">→</a> <a id="4635" href="Cubical.Foundations.Prelude.html#10228" class="Function">subst</a> <a id="4641" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#3724" class="Bound">G</a> <a id="4643" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4631" class="Bound">X</a> <a id="4645" class="Bound">a</a><a id="4646" class="Symbol">)</a> <a id="4648" class="Symbol">(</a><a id="4649" href="Cubical.Relation.Nullary.Properties.html#6986" class="Function">Discrete→isSet</a> <a id="4664" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#3698" class="Bound">decIdx</a> <a id="4671" class="Symbol">_</a> <a id="4673" class="Symbol">_</a> <a id="4675" class="Symbol">_</a> <a id="4677" class="Symbol">_)</a> <a id="4680" href="Cubical.Foundations.Prelude.html#5207" class="Function Operator">∙</a> <a id="4682" href="Cubical.Foundations.Prelude.html#9918" class="Function">transportRefl</a> <a id="4696" class="Symbol">_</a>
+  <a id="4609" class="Symbol">...</a> <a id="4613" class="Symbol">|</a> <a id="4615" href="Cubical.Relation.Nullary.Base.html#478" class="InductiveConstructor">yes</a> <a id="4619" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4619" class="Bound">p</a> <a id="4621" class="Symbol">=</a> <a id="4623" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="4628" class="Symbol">(λ</a> <a id="4631" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4631" class="Bound">X</a> <a id="4633" class="Symbol">→</a> <a id="4635" href="Cubical.Foundations.Prelude.html#10228" class="Function">subst</a> <a id="4641" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#3724" class="Bound">G</a> <a id="4643" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4631" class="Bound">X</a> <a id="4645" class="Bound">a</a><a id="4646" class="Symbol">)</a> <a id="4648" class="Symbol">(</a><a id="4649" href="Cubical.Relation.Nullary.Properties.html#7256" class="Function">Discrete→isSet</a> <a id="4664" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#3698" class="Bound">decIdx</a> <a id="4671" class="Symbol">_</a> <a id="4673" class="Symbol">_</a> <a id="4675" class="Symbol">_</a> <a id="4677" class="Symbol">_)</a> <a id="4680" href="Cubical.Foundations.Prelude.html#5207" class="Function Operator">∙</a> <a id="4682" href="Cubical.Foundations.Prelude.html#9918" class="Function">transportRefl</a> <a id="4696" class="Symbol">_</a>
   <a id="4700" class="Symbol">...</a> <a id="4704" class="Symbol">|</a> <a id="4706" href="Cubical.Relation.Nullary.Base.html#505" class="InductiveConstructor">no</a> <a id="4709" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4709" class="Bound">¬p</a> <a id="4712" class="Symbol">=</a> <a id="4714" href="Cubical.Data.Empty.Base.html#187" class="Function">rec</a> <a id="4718" class="Symbol">(</a><a id="4719" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4709" class="Bound">¬p</a> <a id="4722" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a><a id="4726" class="Symbol">)</a>
 
   <a id="DecIndec-BaseProperties.πₖ-0g"></a><a id="4731" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4731" class="Function">πₖ-0g</a> <a id="4737" class="Symbol">:</a> <a id="4739" class="Symbol">{</a><a id="4740" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4740" class="Bound">k</a> <a id="4742" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4742" class="Bound">l</a> <a id="4744" class="Symbol">:</a> <a id="4746" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#3680" class="Bound">Idx</a><a id="4749" class="Symbol">}</a> <a id="4751" class="Symbol">→</a> <a id="4753" class="Symbol">(</a><a id="4754" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4754" class="Bound">a</a> <a id="4756" class="Symbol">:</a> <a id="4758" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#3724" class="Bound">G</a> <a id="4760" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4742" class="Bound">l</a><a id="4761" class="Symbol">)</a> <a id="4763" class="Symbol">→</a> <a id="4765" class="Symbol">(</a><a id="4766" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4766" class="Bound">p</a> <a id="4768" class="Symbol">:</a> <a id="4770" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4740" class="Bound">k</a> <a id="4772" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="4774" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4742" class="Bound">l</a> <a id="4776" class="Symbol">→</a> <a id="4778" href="Cubical.Data.Empty.Base.html#145" class="Datatype">⊥</a><a id="4779" class="Symbol">)</a> <a id="4781" class="Symbol">→</a> <a id="4783" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#3845" class="Function">πₖ</a> <a id="4786" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4740" class="Bound">k</a> <a id="4788" class="Symbol">(</a><a id="4789" href="Cubical.Algebra.DirectSum.DirectSumHIT.Base.html#618" class="InductiveConstructor">base</a> <a id="4794" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4742" class="Bound">l</a> <a id="4796" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4754" class="Bound">a</a><a id="4797" class="Symbol">)</a> <a id="4799" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="4801" href="Cubical.Algebra.AbGroup.Base.html#1616" class="Field">0g</a> <a id="4804" class="Symbol">(</a><a id="4805" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#3749" class="Bound">Gstr</a> <a id="4810" href="Cubical.Algebra.DirectSum.DirectSumHIT.Properties.html#4740" class="Bound">k</a><a id="4811" class="Symbol">)</a>

Cubical.Algebra.Field.Base.html

@@ -183,7 +183,7 @@
              <a id="6232" class="Symbol">→</a> <a id="6234" href="Cubical.Foundations.Prelude.html#15547" class="Function">isProp</a> <a id="6241" class="Symbol">(</a><a id="6242" href="Cubical.Algebra.Field.Base.html#1350" class="Record">IsField</a> <a id="6250" href="Cubical.Algebra.Field.Base.html#6173" class="Bound">0r</a> <a id="6253" href="Cubical.Algebra.Field.Base.html#6176" class="Bound">1r</a> <a id="6256" href="Cubical.Algebra.Field.Base.html#6185" class="Bound Operator">_+_</a> <a id="6260" href="Cubical.Algebra.Field.Base.html#6189" class="Bound Operator">_·_</a> <a id="6264" href="Cubical.Algebra.Field.Base.html#6207" class="Bound Operator">-_</a><a id="6266" class="Symbol">)</a>
 <a id="6268" href="Cubical.Algebra.Field.Base.html#6143" class="Function">isPropIsField</a> <a id="6282" class="Symbol">{</a><a id="6283" class="Argument">R</a> <a id="6285" class="Symbol">=</a> <a id="6287" href="Cubical.Algebra.Field.Base.html#6287" class="Bound">R</a><a id="6288" class="Symbol">}</a> <a id="6290" href="Cubical.Algebra.Field.Base.html#6290" class="Bound">0r</a> <a id="6293" href="Cubical.Algebra.Field.Base.html#6293" class="Bound">1r</a> <a id="6296" href="Cubical.Algebra.Field.Base.html#6296" class="Bound Operator">_+_</a> <a id="6300" href="Cubical.Algebra.Field.Base.html#6300" class="Bound Operator">_·_</a> <a id="6304" href="Cubical.Algebra.Field.Base.html#6304" class="Bound Operator">-_</a> <a id="6307" href="Cubical.Algebra.Field.Base.html#6307" class="Bound">H</a><a id="6308" class="Symbol">@(</a><a id="6310" href="Cubical.Algebra.Field.Base.html#1466" class="InductiveConstructor">isfield</a> <a id="6318" href="Cubical.Algebra.Field.Base.html#6318" class="Bound">RR</a> <a id="6321" href="Cubical.Algebra.Field.Base.html#6321" class="Bound">RC</a> <a id="6324" href="Cubical.Algebra.Field.Base.html#6324" class="Bound">RD</a><a id="6326" class="Symbol">)</a> <a id="6328" class="Symbol">(</a><a id="6329" href="Cubical.Algebra.Field.Base.html#1466" class="InductiveConstructor">isfield</a> <a id="6337" href="Cubical.Algebra.Field.Base.html#6337" class="Bound">SR</a> <a id="6340" href="Cubical.Algebra.Field.Base.html#6340" class="Bound">SC</a> <a id="6343" href="Cubical.Algebra.Field.Base.html#6343" class="Bound">SD</a><a id="6345" class="Symbol">)</a> <a id="6347" class="Symbol">=</a>
   <a id="6351" class="Symbol">λ</a> <a id="6353" href="Cubical.Algebra.Field.Base.html#6353" class="Bound">i</a> <a id="6355" class="Symbol">→</a> <a id="6357" href="Cubical.Algebra.Field.Base.html#1466" class="InductiveConstructor">isfield</a> <a id="6365" class="Symbol">(</a><a id="6366" href="Cubical.Algebra.CommRing.Base.html#4736" class="Function">isPropIsCommRing</a> <a id="6383" class="Symbol">_</a> <a id="6385" class="Symbol">_</a> <a id="6387" class="Symbol">_</a> <a id="6389" class="Symbol">_</a> <a id="6391" class="Symbol">_</a> <a id="6393" href="Cubical.Algebra.Field.Base.html#6318" class="Bound">RR</a> <a id="6396" href="Cubical.Algebra.Field.Base.html#6337" class="Bound">SR</a> <a id="6399" href="Cubical.Algebra.Field.Base.html#6353" class="Bound">i</a><a id="6400" class="Symbol">)</a>
-                   <a id="6421" class="Symbol">(</a><a id="6422" href="Cubical.Algebra.Field.Base.html#6471" class="Function">isPropInv</a> <a id="6432" href="Cubical.Algebra.Field.Base.html#6321" class="Bound">RC</a> <a id="6435" href="Cubical.Algebra.Field.Base.html#6340" class="Bound">SC</a> <a id="6438" href="Cubical.Algebra.Field.Base.html#6353" class="Bound">i</a><a id="6439" class="Symbol">)</a> <a id="6441" class="Symbol">(</a><a id="6442" href="Cubical.Relation.Nullary.Properties.html#1361" class="Function">isProp¬</a> <a id="6450" class="Symbol">_</a> <a id="6452" href="Cubical.Algebra.Field.Base.html#6324" class="Bound">RD</a> <a id="6455" href="Cubical.Algebra.Field.Base.html#6343" class="Bound">SD</a> <a id="6458" href="Cubical.Algebra.Field.Base.html#6353" class="Bound">i</a><a id="6459" class="Symbol">)</a>
+                   <a id="6421" class="Symbol">(</a><a id="6422" href="Cubical.Algebra.Field.Base.html#6471" class="Function">isPropInv</a> <a id="6432" href="Cubical.Algebra.Field.Base.html#6321" class="Bound">RC</a> <a id="6435" href="Cubical.Algebra.Field.Base.html#6340" class="Bound">SC</a> <a id="6438" href="Cubical.Algebra.Field.Base.html#6353" class="Bound">i</a><a id="6439" class="Symbol">)</a> <a id="6441" class="Symbol">(</a><a id="6442" href="Cubical.Relation.Nullary.Properties.html#1364" class="Function">isProp¬</a> <a id="6450" class="Symbol">_</a> <a id="6452" href="Cubical.Algebra.Field.Base.html#6324" class="Bound">RD</a> <a id="6455" href="Cubical.Algebra.Field.Base.html#6343" class="Bound">SD</a> <a id="6458" href="Cubical.Algebra.Field.Base.html#6353" class="Bound">i</a><a id="6459" class="Symbol">)</a>
   <a id="6463" class="Keyword">where</a>
   <a id="6471" href="Cubical.Algebra.Field.Base.html#6471" class="Function">isPropInv</a> <a id="6481" class="Symbol">:</a> <a id="6483" href="Cubical.Foundations.Prelude.html#15547" class="Function">isProp</a> <a id="6490" class="Symbol">((</a><a id="6492" href="Cubical.Algebra.Field.Base.html#6492" class="Bound">x</a> <a id="6494" class="Symbol">:</a> <a id="6496" class="Symbol">_)</a> <a id="6499" class="Symbol">→</a> <a id="6501" href="Cubical.Relation.Nullary.Base.html#355" class="Function Operator">¬</a> <a id="6503" href="Cubical.Algebra.Field.Base.html#6492" class="Bound">x</a> <a id="6505" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="6507" href="Cubical.Algebra.Field.Base.html#6290" class="Bound">0r</a> <a id="6510" class="Symbol">→</a> <a id="6512" href="Cubical.Core.Primitives.html#6268" class="Function">Σ[</a> <a id="6515" href="Cubical.Algebra.Field.Base.html#6515" class="Bound">y</a> <a id="6517" href="Cubical.Core.Primitives.html#6268" class="Function">∈</a> <a id="6519" href="Cubical.Algebra.Field.Base.html#6287" class="Bound">R</a> <a id="6521" href="Cubical.Core.Primitives.html#6268" class="Function">]</a> <a id="6523" href="Cubical.Algebra.Field.Base.html#6492" class="Bound">x</a> <a id="6525" href="Cubical.Algebra.Field.Base.html#6300" class="Bound Operator">·</a> <a id="6527" href="Cubical.Algebra.Field.Base.html#6515" class="Bound">y</a> <a id="6529" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="6531" href="Cubical.Algebra.Field.Base.html#6293" class="Bound">1r</a><a id="6533" class="Symbol">)</a>
   <a id="6537" href="Cubical.Algebra.Field.Base.html#6471" class="Function">isPropInv</a> <a id="6547" class="Symbol">=</a> <a id="6549" href="Cubical.Foundations.HLevels.html#16995" class="Function">isPropΠ2</a> <a id="6558" class="Symbol">(λ</a> <a id="6561" href="Cubical.Algebra.Field.Base.html#6561" class="Bound">x</a> <a id="6563" href="Cubical.Algebra.Field.Base.html#6563" class="Bound">_</a> <a id="6565" class="Symbol">→</a> <a id="6567" href="Cubical.Algebra.CommRing.Properties.html#1307" class="Function">Units.inverseUniqueness</a> <a id="6591" class="Symbol">(</a><a id="6592" href="Cubical.Algebra.Field.Base.html#4865" class="Function">Field→CommRing</a> <a id="6607" class="Symbol">(_</a> <a id="6610" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="6612" href="Cubical.Algebra.Field.Base.html#1895" class="InductiveConstructor">fieldstr</a> <a id="6621" class="Symbol">_</a> <a id="6623" class="Symbol">_</a> <a id="6625" class="Symbol">_</a> <a id="6627" class="Symbol">_</a> <a id="6629" class="Symbol">_</a> <a id="6631" href="Cubical.Algebra.Field.Base.html#6307" class="Bound">H</a><a id="6632" class="Symbol">))</a> <a id="6635" href="Cubical.Algebra.Field.Base.html#6561" class="Bound">x</a><a id="6636" class="Symbol">)</a>