Deploying to gh-pages from @ 6dc0886 🚀

Author: felixwellen

Cubical.Algebra.AbGroup.Base.html

@@ -277,7 +277,7 @@
 <a id="9012" href="Cubical.Algebra.AbGroup.Base.html#1611" class="Field Operator">_+_</a> <a id="9016" class="Symbol">(</a><a id="9017" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="9021" href="Cubical.Algebra.AbGroup.Base.html#8920" class="Function">trivialAbGroup</a><a id="9035" class="Symbol">)</a> <a id="9037" class="Symbol">_</a> <a id="9039" class="Symbol">_</a> <a id="9041" class="Symbol">=</a> <a id="9043" href="Cubical.Data.Unit.Base.html#245" class="InductiveConstructor">tt*</a>
 <a id="9047" class="Symbol">(</a><a id="9048" href="Cubical.Algebra.AbGroup.Base.html#1637" class="Field Operator">-</a> <a id="9050" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="9054" href="Cubical.Algebra.AbGroup.Base.html#8920" class="Function">trivialAbGroup</a><a id="9068" class="Symbol">)</a> <a id="9070" class="Symbol">_</a> <a id="9072" class="Symbol">=</a> <a id="9074" href="Cubical.Data.Unit.Base.html#245" class="InductiveConstructor">tt*</a>
 <a id="9078" href="Cubical.Algebra.AbGroup.Base.html#1659" class="Field">isAbGroup</a> <a id="9088" class="Symbol">(</a><a id="9089" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="9093" href="Cubical.Algebra.AbGroup.Base.html#8920" class="Function">trivialAbGroup</a><a id="9107" class="Symbol">)</a> <a id="9109" class="Symbol">=</a> <a id="9111" href="Cubical.Algebra.AbGroup.Base.html#2130" class="Function">makeIsAbGroup</a>
-                                 <a id="9158" class="Symbol">(</a><a id="9159" href="Cubical.Foundations.Prelude.html#19832" class="Function">isProp→isSet</a> <a id="9172" href="Cubical.Data.Unit.Properties.html#2723" class="Function">isPropUnit*</a><a id="9183" class="Symbol">)</a>
+                                 <a id="9158" class="Symbol">(</a><a id="9159" href="Cubical.Foundations.Prelude.html#20297" class="Function">isProp→isSet</a> <a id="9172" href="Cubical.Data.Unit.Properties.html#2723" class="Function">isPropUnit*</a><a id="9183" class="Symbol">)</a>
                                  <a id="9218" class="Symbol">(λ</a> <a id="9221" href="Cubical.Algebra.AbGroup.Base.html#9221" class="Bound">_</a> <a id="9223" href="Cubical.Algebra.AbGroup.Base.html#9223" class="Bound">_</a> <a id="9225" href="Cubical.Algebra.AbGroup.Base.html#9225" class="Bound">_</a> <a id="9227" class="Symbol">→</a> <a id="9229" href="Cubical.Foundations.Prelude.html#892" class="Function">refl</a><a id="9233" class="Symbol">)</a>
                                  <a id="9268" class="Symbol">(λ</a> <a id="9271" href="Cubical.Algebra.AbGroup.Base.html#9271" class="Bound">_</a> <a id="9273" class="Symbol">→</a> <a id="9275" href="Cubical.Foundations.Prelude.html#892" class="Function">refl</a><a id="9279" class="Symbol">)</a>
                                  <a id="9314" class="Symbol">(λ</a> <a id="9317" href="Cubical.Algebra.AbGroup.Base.html#9317" class="Bound">_</a> <a id="9319" class="Symbol">→</a> <a id="9321" href="Cubical.Foundations.Prelude.html#892" class="Function">refl</a><a id="9325" class="Symbol">)</a>

Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html

@@ -112,7 +112,7 @@
     <a id="3115" href="Cubical.Foundations.HLevels.html#26149" class="Function">isOfHLevel→isOfHLevelDep</a> <a id="3140" class="Number">1</a> <a id="3142" class="Symbol">{</a><a id="3143" class="Argument">B</a> <a id="3145" class="Symbol">=</a> <a id="3147" href="Cubical.Algebra.AbGroup.TensorProduct.html#3081" class="Bound">C</a><a id="3148" class="Symbol">}</a> <a id="3150" href="Cubical.Algebra.AbGroup.TensorProduct.html#3084" class="Bound">p</a>
       <a id="3158" class="Symbol">(</a><a id="3159" href="Cubical.Algebra.AbGroup.TensorProduct.html#3086" class="Bound">f</a> <a id="3161" class="Symbol">(</a><a id="3162" href="Cubical.Algebra.AbGroup.TensorProduct.html#3100" class="Bound">x</a> <a id="3164" href="Cubical.Algebra.AbGroup.TensorProduct.html#1789" class="Function Operator">+A</a> <a id="3167" href="Cubical.Algebra.AbGroup.TensorProduct.html#3102" class="Bound">y</a><a id="3168" class="Symbol">)</a> <a id="3170" href="Cubical.Algebra.AbGroup.TensorProduct.html#3104" class="Bound">z</a><a id="3171" class="Symbol">)</a> <a id="3173" class="Symbol">(</a><a id="3174" href="Cubical.Algebra.AbGroup.TensorProduct.html#3088" class="Bound">g</a> <a id="3176" class="Symbol">(</a><a id="3177" href="Cubical.Algebra.AbGroup.TensorProduct.html#3100" class="Bound">x</a> <a id="3179" href="Cubical.Algebra.AbGroup.TensorProduct.html#1170" class="InductiveConstructor Operator">⊗</a> <a id="3181" href="Cubical.Algebra.AbGroup.TensorProduct.html#3104" class="Bound">z</a><a id="3182" class="Symbol">)</a> <a id="3184" class="Symbol">(</a><a id="3185" href="Cubical.Algebra.AbGroup.TensorProduct.html#3102" class="Bound">y</a> <a id="3187" href="Cubical.Algebra.AbGroup.TensorProduct.html#1170" class="InductiveConstructor Operator">⊗</a> <a id="3189" href="Cubical.Algebra.AbGroup.TensorProduct.html#3104" class="Bound">z</a><a id="3190" class="Symbol">)</a> <a id="3192" class="Symbol">(</a><a id="3193" href="Cubical.Algebra.AbGroup.TensorProduct.html#3086" class="Bound">f</a> <a id="3195" href="Cubical.Algebra.AbGroup.TensorProduct.html#3100" class="Bound">x</a> <a id="3197" href="Cubical.Algebra.AbGroup.TensorProduct.html#3104" class="Bound">z</a><a id="3198" class="Symbol">)</a> <a id="3200" class="Symbol">(</a><a id="3201" href="Cubical.Algebra.AbGroup.TensorProduct.html#3086" class="Bound">f</a> <a id="3203" href="Cubical.Algebra.AbGroup.TensorProduct.html#3102" class="Bound">y</a> <a id="3205" href="Cubical.Algebra.AbGroup.TensorProduct.html#3104" class="Bound">z</a><a id="3206" class="Symbol">))</a> <a id="3209" class="Symbol">(</a><a id="3210" href="Cubical.Algebra.AbGroup.TensorProduct.html#1467" class="InductiveConstructor">⊗DistL+⊗</a> <a id="3219" href="Cubical.Algebra.AbGroup.TensorProduct.html#3100" class="Bound">x</a> <a id="3221" href="Cubical.Algebra.AbGroup.TensorProduct.html#3102" class="Bound">y</a> <a id="3223" href="Cubical.Algebra.AbGroup.TensorProduct.html#3104" class="Bound">z</a><a id="3224" class="Symbol">)</a> <a id="3226" href="Cubical.Algebra.AbGroup.TensorProduct.html#3106" class="Bound">i</a>
   <a id="3230" href="Cubical.Algebra.AbGroup.TensorProduct.html#1889" class="Function">⊗elimProp</a> <a id="3240" class="Symbol">{</a><a id="3241" class="Argument">C</a> <a id="3243" class="Symbol">=</a> <a id="3245" href="Cubical.Algebra.AbGroup.TensorProduct.html#3245" class="Bound">C</a><a id="3246" class="Symbol">}</a> <a id="3248" href="Cubical.Algebra.AbGroup.TensorProduct.html#3248" class="Bound">p</a> <a id="3250" href="Cubical.Algebra.AbGroup.TensorProduct.html#3250" class="Bound">f</a> <a id="3252" href="Cubical.Algebra.AbGroup.TensorProduct.html#3252" class="Bound">g</a> <a id="3254" class="Symbol">(</a><a id="3255" href="Cubical.Algebra.AbGroup.TensorProduct.html#1538" class="InductiveConstructor">⊗squash</a> <a id="3263" href="Cubical.Algebra.AbGroup.TensorProduct.html#3263" class="Bound">x</a> <a id="3265" href="Cubical.Algebra.AbGroup.TensorProduct.html#3265" class="Bound">y</a> <a id="3267" href="Cubical.Algebra.AbGroup.TensorProduct.html#3267" class="Bound">q</a> <a id="3269" href="Cubical.Algebra.AbGroup.TensorProduct.html#3269" class="Bound">r</a> <a id="3271" href="Cubical.Algebra.AbGroup.TensorProduct.html#3271" class="Bound">i</a> <a id="3273" href="Cubical.Algebra.AbGroup.TensorProduct.html#3273" class="Bound">j</a><a id="3274" class="Symbol">)</a> <a id="3276" class="Symbol">=</a>
-    <a id="3282" href="Cubical.Foundations.HLevels.html#26149" class="Function">isOfHLevel→isOfHLevelDep</a> <a id="3307" class="Number">2</a> <a id="3309" class="Symbol">{</a><a id="3310" class="Argument">B</a> <a id="3312" class="Symbol">=</a> <a id="3314" href="Cubical.Algebra.AbGroup.TensorProduct.html#3245" class="Bound">C</a><a id="3315" class="Symbol">}</a> <a id="3317" class="Symbol">(λ</a> <a id="3320" href="Cubical.Algebra.AbGroup.TensorProduct.html#3320" class="Bound">x</a> <a id="3322" class="Symbol">→</a> <a id="3324" href="Cubical.Foundations.Prelude.html#19832" class="Function">isProp→isSet</a> <a id="3337" class="Symbol">(</a><a id="3338" href="Cubical.Algebra.AbGroup.TensorProduct.html#3248" class="Bound">p</a> <a id="3340" href="Cubical.Algebra.AbGroup.TensorProduct.html#3320" class="Bound">x</a><a id="3341" class="Symbol">))</a>
+    <a id="3282" href="Cubical.Foundations.HLevels.html#26149" class="Function">isOfHLevel→isOfHLevelDep</a> <a id="3307" class="Number">2</a> <a id="3309" class="Symbol">{</a><a id="3310" class="Argument">B</a> <a id="3312" class="Symbol">=</a> <a id="3314" href="Cubical.Algebra.AbGroup.TensorProduct.html#3245" class="Bound">C</a><a id="3315" class="Symbol">}</a> <a id="3317" class="Symbol">(λ</a> <a id="3320" href="Cubical.Algebra.AbGroup.TensorProduct.html#3320" class="Bound">x</a> <a id="3322" class="Symbol">→</a> <a id="3324" href="Cubical.Foundations.Prelude.html#20297" class="Function">isProp→isSet</a> <a id="3337" class="Symbol">(</a><a id="3338" href="Cubical.Algebra.AbGroup.TensorProduct.html#3248" class="Bound">p</a> <a id="3340" href="Cubical.Algebra.AbGroup.TensorProduct.html#3320" class="Bound">x</a><a id="3341" class="Symbol">))</a>
       <a id="3350" class="Symbol">_</a> <a id="3352" class="Symbol">_</a> <a id="3354" class="Symbol">(λ</a> <a id="3357" href="Cubical.Algebra.AbGroup.TensorProduct.html#3357" class="Bound">j</a> <a id="3359" class="Symbol">→</a> <a id="3361" href="Cubical.Algebra.AbGroup.TensorProduct.html#1889" class="Function">⊗elimProp</a> <a id="3371" href="Cubical.Algebra.AbGroup.TensorProduct.html#3248" class="Bound">p</a> <a id="3373" href="Cubical.Algebra.AbGroup.TensorProduct.html#3250" class="Bound">f</a> <a id="3375" href="Cubical.Algebra.AbGroup.TensorProduct.html#3252" class="Bound">g</a> <a id="3377" class="Symbol">(</a><a id="3378" href="Cubical.Algebra.AbGroup.TensorProduct.html#3267" class="Bound">q</a> <a id="3380" href="Cubical.Algebra.AbGroup.TensorProduct.html#3357" class="Bound">j</a><a id="3381" class="Symbol">))</a> <a id="3384" class="Symbol">(λ</a> <a id="3387" href="Cubical.Algebra.AbGroup.TensorProduct.html#3387" class="Bound">j</a> <a id="3389" class="Symbol">→</a> <a id="3391" href="Cubical.Algebra.AbGroup.TensorProduct.html#1889" class="Function">⊗elimProp</a> <a id="3401" href="Cubical.Algebra.AbGroup.TensorProduct.html#3248" class="Bound">p</a> <a id="3403" href="Cubical.Algebra.AbGroup.TensorProduct.html#3250" class="Bound">f</a> <a id="3405" href="Cubical.Algebra.AbGroup.TensorProduct.html#3252" class="Bound">g</a> <a id="3407" class="Symbol">(</a><a id="3408" href="Cubical.Algebra.AbGroup.TensorProduct.html#3269" class="Bound">r</a> <a id="3410" href="Cubical.Algebra.AbGroup.TensorProduct.html#3387" class="Bound">j</a><a id="3411" class="Symbol">))</a>
           <a id="3424" class="Symbol">(</a><a id="3425" href="Cubical.Algebra.AbGroup.TensorProduct.html#1538" class="InductiveConstructor">⊗squash</a> <a id="3433" href="Cubical.Algebra.AbGroup.TensorProduct.html#3263" class="Bound">x</a> <a id="3435" href="Cubical.Algebra.AbGroup.TensorProduct.html#3265" class="Bound">y</a> <a id="3437" href="Cubical.Algebra.AbGroup.TensorProduct.html#3267" class="Bound">q</a> <a id="3439" href="Cubical.Algebra.AbGroup.TensorProduct.html#3269" class="Bound">r</a><a id="3440" class="Symbol">)</a> <a id="3442" href="Cubical.Algebra.AbGroup.TensorProduct.html#3271" class="Bound">i</a> <a id="3444" href="Cubical.Algebra.AbGroup.TensorProduct.html#3273" class="Bound">j</a>
 

Cubical.Algebra.AbGroup.Instances.IntMod.html

@@ -218,15 +218,15 @@
 <a id="isSetAlgebraHom"></a><a id="7664" href="Cubical.Algebra.Algebra.Base.html#7664" class="Function">isSetAlgebraHom</a> <a id="7680" class="Symbol">:</a> <a id="7682" class="Symbol">(</a><a id="7683" href="Cubical.Algebra.Algebra.Base.html#7683" class="Bound">M</a> <a id="7685" class="Symbol">:</a> <a id="7687" href="Cubical.Algebra.Algebra.Base.html#2086" class="Function">Algebra</a> <a id="7695" href="Cubical.Algebra.Algebra.Base.html#5884" class="Generalizable">R</a> <a id="7697" href="Cubical.Algebra.Algebra.Base.html#667" class="Generalizable">ℓ&#39;</a><a id="7699" class="Symbol">)</a> <a id="7701" class="Symbol">(</a><a id="7702" href="Cubical.Algebra.Algebra.Base.html#7702" class="Bound">N</a> <a id="7704" class="Symbol">:</a> <a id="7706" href="Cubical.Algebra.Algebra.Base.html#2086" class="Function">Algebra</a> <a id="7714" href="Cubical.Algebra.Algebra.Base.html#5884" class="Generalizable">R</a> <a id="7716" href="Cubical.Algebra.Algebra.Base.html#670" class="Generalizable">ℓ&#39;&#39;</a><a id="7719" class="Symbol">)</a>
                 <a id="7737" class="Symbol">→</a> <a id="7739" href="Cubical.Foundations.Prelude.html#15579" class="Function">isSet</a> <a id="7745" class="Symbol">(</a><a id="7746" href="Cubical.Algebra.Algebra.Base.html#5918" class="Function">AlgebraHom</a> <a id="7757" href="Cubical.Algebra.Algebra.Base.html#7683" class="Bound">M</a> <a id="7759" href="Cubical.Algebra.Algebra.Base.html#7702" class="Bound">N</a><a id="7760" class="Symbol">)</a>
 <a id="7762" href="Cubical.Algebra.Algebra.Base.html#7664" class="Function">isSetAlgebraHom</a> <a id="7778" class="Symbol">_</a> <a id="7780" href="Cubical.Algebra.Algebra.Base.html#7780" class="Bound">N</a> <a id="7782" class="Symbol">=</a> <a id="7784" href="Cubical.Foundations.HLevels.html#13368" class="Function">isSetΣ</a> <a id="7791" class="Symbol">(</a><a id="7792" href="Cubical.Foundations.HLevels.html#18870" class="Function">isSetΠ</a> <a id="7799" class="Symbol">(λ</a> <a id="7802" href="Cubical.Algebra.Algebra.Base.html#7802" class="Bound">_</a> <a id="7804" class="Symbol">→</a> <a id="7806" href="Cubical.Algebra.Semigroup.Base.html#987" class="Function">is-set</a><a id="7812" class="Symbol">))</a>
-                        <a id="7839" class="Symbol">λ</a> <a id="7841" href="Cubical.Algebra.Algebra.Base.html#7841" class="Bound">_</a> <a id="7843" class="Symbol">→</a> <a id="7845" href="Cubical.Foundations.Prelude.html#19832" class="Function">isProp→isSet</a> <a id="7858" class="Symbol">(</a><a id="7859" href="Cubical.Algebra.Algebra.Base.html#7134" class="Function">isPropIsAlgebraHom</a> <a id="7878" class="Symbol">_</a> <a id="7880" class="Symbol">_</a> <a id="7882" class="Symbol">_</a> <a id="7884" class="Symbol">_)</a>
+                        <a id="7839" class="Symbol">λ</a> <a id="7841" href="Cubical.Algebra.Algebra.Base.html#7841" class="Bound">_</a> <a id="7843" class="Symbol">→</a> <a id="7845" href="Cubical.Foundations.Prelude.html#20297" class="Function">isProp→isSet</a> <a id="7858" class="Symbol">(</a><a id="7859" href="Cubical.Algebra.Algebra.Base.html#7134" class="Function">isPropIsAlgebraHom</a> <a id="7878" class="Symbol">_</a> <a id="7880" class="Symbol">_</a> <a id="7882" class="Symbol">_</a> <a id="7884" class="Symbol">_)</a>
   <a id="7889" class="Keyword">where</a>
   <a id="7897" class="Keyword">open</a> <a id="7902" href="Cubical.Algebra.Algebra.Base.html#1671" class="Module">AlgebraStr</a> <a id="7913" class="Symbol">(</a><a id="7914" href="Cubical.Foundations.Structure.html#1051" class="Function">str</a> <a id="7918" href="Cubical.Algebra.Algebra.Base.html#7780" class="Bound">N</a><a id="7919" class="Symbol">)</a>
 
 
 <a id="isSetAlgebraEquiv"></a><a id="7923" href="Cubical.Algebra.Algebra.Base.html#7923" class="Function">isSetAlgebraEquiv</a> <a id="7941" class="Symbol">:</a> <a id="7943" class="Symbol">(</a><a id="7944" href="Cubical.Algebra.Algebra.Base.html#7944" class="Bound">M</a> <a id="7946" class="Symbol">:</a> <a id="7948" href="Cubical.Algebra.Algebra.Base.html#2086" class="Function">Algebra</a> <a id="7956" href="Cubical.Algebra.Algebra.Base.html#5884" class="Generalizable">R</a> <a id="7958" href="Cubical.Algebra.Algebra.Base.html#667" class="Generalizable">ℓ&#39;</a><a id="7960" class="Symbol">)</a> <a id="7962" class="Symbol">(</a><a id="7963" href="Cubical.Algebra.Algebra.Base.html#7963" class="Bound">N</a> <a id="7965" class="Symbol">:</a> <a id="7967" href="Cubical.Algebra.Algebra.Base.html#2086" class="Function">Algebra</a> <a id="7975" href="Cubical.Algebra.Algebra.Base.html#5884" class="Generalizable">R</a> <a id="7977" href="Cubical.Algebra.Algebra.Base.html#670" class="Generalizable">ℓ&#39;&#39;</a><a id="7980" class="Symbol">)</a>
                   <a id="8000" class="Symbol">→</a> <a id="8002" href="Cubical.Foundations.Prelude.html#15579" class="Function">isSet</a> <a id="8008" class="Symbol">(</a><a id="8009" href="Cubical.Algebra.Algebra.Base.html#6218" class="Function">AlgebraEquiv</a> <a id="8022" href="Cubical.Algebra.Algebra.Base.html#7944" class="Bound">M</a> <a id="8024" href="Cubical.Algebra.Algebra.Base.html#7963" class="Bound">N</a><a id="8025" class="Symbol">)</a>
 <a id="8027" href="Cubical.Algebra.Algebra.Base.html#7923" class="Function">isSetAlgebraEquiv</a> <a id="8045" href="Cubical.Algebra.Algebra.Base.html#8045" class="Bound">M</a> <a id="8047" href="Cubical.Algebra.Algebra.Base.html#8047" class="Bound">N</a> <a id="8049" class="Symbol">=</a> <a id="8051" href="Cubical.Foundations.HLevels.html#13368" class="Function">isSetΣ</a> <a id="8058" class="Symbol">(</a><a id="8059" href="Cubical.Foundations.HLevels.html#21294" class="Function">isOfHLevel≃</a> <a id="8071" class="Number">2</a> <a id="8073" href="Cubical.Algebra.Semigroup.Base.html#987" class="Function">M.is-set</a> <a id="8082" href="Cubical.Algebra.Semigroup.Base.html#987" class="Function">N.is-set</a><a id="8090" class="Symbol">)</a>
-                          <a id="8118" class="Symbol">λ</a> <a id="8120" href="Cubical.Algebra.Algebra.Base.html#8120" class="Bound">_</a> <a id="8122" class="Symbol">→</a> <a id="8124" href="Cubical.Foundations.Prelude.html#19832" class="Function">isProp→isSet</a> <a id="8137" class="Symbol">(</a><a id="8138" href="Cubical.Algebra.Algebra.Base.html#7134" class="Function">isPropIsAlgebraHom</a> <a id="8157" class="Symbol">_</a> <a id="8159" class="Symbol">_</a> <a id="8161" class="Symbol">_</a> <a id="8163" class="Symbol">_)</a>
+                          <a id="8118" class="Symbol">λ</a> <a id="8120" href="Cubical.Algebra.Algebra.Base.html#8120" class="Bound">_</a> <a id="8122" class="Symbol">→</a> <a id="8124" href="Cubical.Foundations.Prelude.html#20297" class="Function">isProp→isSet</a> <a id="8137" class="Symbol">(</a><a id="8138" href="Cubical.Algebra.Algebra.Base.html#7134" class="Function">isPropIsAlgebraHom</a> <a id="8157" class="Symbol">_</a> <a id="8159" class="Symbol">_</a> <a id="8161" class="Symbol">_</a> <a id="8163" class="Symbol">_)</a>
   <a id="8168" class="Keyword">where</a>
   <a id="8176" class="Keyword">module</a> <a id="8183" href="Cubical.Algebra.Algebra.Base.html#8183" class="Module">M</a> <a id="8185" class="Symbol">=</a> <a id="8187" href="Cubical.Algebra.Algebra.Base.html#1671" class="Module">AlgebraStr</a> <a id="8198" class="Symbol">(</a><a id="8199" href="Cubical.Foundations.Structure.html#1051" class="Function">str</a> <a id="8203" href="Cubical.Algebra.Algebra.Base.html#8045" class="Bound">M</a><a id="8204" class="Symbol">)</a>
   <a id="8208" class="Keyword">module</a> <a id="8215" href="Cubical.Algebra.Algebra.Base.html#8215" class="Module">N</a> <a id="8217" class="Symbol">=</a> <a id="8219" href="Cubical.Algebra.Algebra.Base.html#1671" class="Module">AlgebraStr</a> <a id="8230" class="Symbol">(</a><a id="8231" href="Cubical.Foundations.Structure.html#1051" class="Function">str</a> <a id="8235" href="Cubical.Algebra.Algebra.Base.html#8047" class="Bound">N</a><a id="8236" class="Symbol">)</a>