Deploying to gh-pages from @ dfa5b89 🚀

Author: github-merge-queue[bot]

master/Algebra.Apartness.Bundles.html

@@ -13,7 +13,7 @@
 <a id="342" class="Keyword">open</a> <a id="347" class="Keyword">import</a> <a id="354" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a> <a id="375" class="Keyword">using</a> <a id="381" class="Symbol">(</a><a id="382" href="Relation.Binary.Core.html#896" class="Function">Rel</a><a id="385" class="Symbol">)</a>
 <a id="387" class="Keyword">open</a> <a id="392" class="Keyword">import</a> <a id="399" href="Relation.Binary.Bundles.html" class="Module">Relation.Binary.Bundles</a> <a id="423" class="Keyword">using</a> <a id="429" class="Symbol">(</a><a id="430" href="Relation.Binary.Bundles.html#11022" class="Record">ApartnessRelation</a><a id="447" class="Symbol">)</a>
 <a id="449" class="Keyword">open</a> <a id="454" class="Keyword">import</a> <a id="461" href="Algebra.Core.html" class="Module">Algebra.Core</a> <a id="474" class="Keyword">using</a> <a id="480" class="Symbol">(</a><a id="481" href="Algebra.Core.html#484" class="Function">Op₁</a><a id="484" class="Symbol">;</a> <a id="486" href="Algebra.Core.html#527" class="Function">Op₂</a><a id="489" class="Symbol">)</a>
-<a id="491" class="Keyword">open</a> <a id="496" class="Keyword">import</a> <a id="503" href="Algebra.Bundles.html" class="Module">Algebra.Bundles</a> <a id="519" class="Keyword">using</a> <a id="525" class="Symbol">(</a><a id="526" href="Algebra.Bundles.html#30337" class="Record">CommutativeRing</a><a id="541" class="Symbol">)</a>
+<a id="491" class="Keyword">open</a> <a id="496" class="Keyword">import</a> <a id="503" href="Algebra.Bundles.html" class="Module">Algebra.Bundles</a> <a id="519" class="Keyword">using</a> <a id="525" class="Symbol">(</a><a id="526" href="Algebra.Bundles.html#31426" class="Record">CommutativeRing</a><a id="541" class="Symbol">)</a>
 <a id="543" class="Keyword">open</a> <a id="548" class="Keyword">import</a> <a id="555" href="Algebra.Apartness.Structures.html" class="Module">Algebra.Apartness.Structures</a> <a id="584" class="Keyword">using</a> <a id="590" class="Symbol">(</a><a id="591" href="Algebra.Apartness.Structures.html#1019" class="Record">IsHeytingCommutativeRing</a><a id="615" class="Symbol">;</a> <a id="617" href="Algebra.Apartness.Structures.html#1653" class="Record">IsHeytingField</a><a id="631" class="Symbol">)</a>
 
 <a id="634" class="Keyword">record</a> <a id="HeytingCommutativeRing"></a><a id="641" href="Algebra.Apartness.Bundles.html#641" class="Record">HeytingCommutativeRing</a> <a id="664" href="Algebra.Apartness.Bundles.html#664" class="Bound">c</a> <a id="666" href="Algebra.Apartness.Bundles.html#666" class="Bound">ℓ₁</a> <a id="669" href="Algebra.Apartness.Bundles.html#669" class="Bound">ℓ₂</a> <a id="672" class="Symbol">:</a> <a id="674" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="678" class="Symbol">(</a><a id="679" href="Agda.Primitive.html#931" class="Primitive">suc</a> <a id="683" class="Symbol">(</a><a id="684" href="Algebra.Apartness.Bundles.html#664" class="Bound">c</a> <a id="686" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="688" href="Algebra.Apartness.Bundles.html#666" class="Bound">ℓ₁</a> <a id="691" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="693" href="Algebra.Apartness.Bundles.html#669" class="Bound">ℓ₂</a><a id="695" class="Symbol">))</a> <a id="698" class="Keyword">where</a>
@@ -34,8 +34,8 @@
 
   <a id="1195" class="Keyword">open</a> <a id="1200" href="Algebra.Apartness.Structures.html#1019" class="Module">IsHeytingCommutativeRing</a> <a id="1225" href="Algebra.Apartness.Bundles.html#1115" class="Field">isHeytingCommutativeRing</a> <a id="1250" class="Keyword">public</a>
 
-  <a id="HeytingCommutativeRing.commutativeRing"></a><a id="1260" href="Algebra.Apartness.Bundles.html#1260" class="Function">commutativeRing</a> <a id="1276" class="Symbol">:</a> <a id="1278" href="Algebra.Bundles.html#30337" class="Record">CommutativeRing</a> <a id="1294" href="Algebra.Apartness.Bundles.html#664" class="Bound">c</a> <a id="1296" href="Algebra.Apartness.Bundles.html#666" class="Bound">ℓ₁</a>
-  <a id="1301" href="Algebra.Apartness.Bundles.html#1260" class="Function">commutativeRing</a> <a id="1317" class="Symbol">=</a> <a id="1319" class="Keyword">record</a> <a id="1326" class="Symbol">{</a> <a id="1328" href="Algebra.Bundles.html#30694" class="Field">isCommutativeRing</a> <a id="1346" class="Symbol">=</a> <a id="1348" href="Algebra.Apartness.Structures.html#1083" class="Function">isCommutativeRing</a> <a id="1366" class="Symbol">}</a>
+  <a id="HeytingCommutativeRing.commutativeRing"></a><a id="1260" href="Algebra.Apartness.Bundles.html#1260" class="Function">commutativeRing</a> <a id="1276" class="Symbol">:</a> <a id="1278" href="Algebra.Bundles.html#31426" class="Record">CommutativeRing</a> <a id="1294" href="Algebra.Apartness.Bundles.html#664" class="Bound">c</a> <a id="1296" href="Algebra.Apartness.Bundles.html#666" class="Bound">ℓ₁</a>
+  <a id="1301" href="Algebra.Apartness.Bundles.html#1260" class="Function">commutativeRing</a> <a id="1317" class="Symbol">=</a> <a id="1319" class="Keyword">record</a> <a id="1326" class="Symbol">{</a> <a id="1328" href="Algebra.Bundles.html#31783" class="Field">isCommutativeRing</a> <a id="1346" class="Symbol">=</a> <a id="1348" href="Algebra.Apartness.Structures.html#1083" class="Function">isCommutativeRing</a> <a id="1366" class="Symbol">}</a>
 
   <a id="HeytingCommutativeRing.apartnessRelation"></a><a id="1371" href="Algebra.Apartness.Bundles.html#1371" class="Function">apartnessRelation</a> <a id="1389" class="Symbol">:</a> <a id="1391" href="Relation.Binary.Bundles.html#11022" class="Record">ApartnessRelation</a> <a id="1409" href="Algebra.Apartness.Bundles.html#664" class="Bound">c</a> <a id="1411" href="Algebra.Apartness.Bundles.html#666" class="Bound">ℓ₁</a> <a id="1414" href="Algebra.Apartness.Bundles.html#669" class="Bound">ℓ₂</a>
   <a id="1419" href="Algebra.Apartness.Bundles.html#1371" class="Function">apartnessRelation</a> <a id="1437" class="Symbol">=</a> <a id="1439" class="Keyword">record</a> <a id="1446" class="Symbol">{</a> <a id="1448" href="Relation.Binary.Bundles.html#11224" class="Field">isApartnessRelation</a> <a id="1468" class="Symbol">=</a> <a id="1470" href="Algebra.Apartness.Structures.html#1144" class="Function">isApartnessRelation</a> <a id="1490" class="Symbol">}</a>