Deploying to gh-pages from @ 952b058 🚀

Author: github-merge-queue[bot]

master/Algebra.Apartness.Bundles.html

@@ -11,7 +11,7 @@
 
 <a id="307" class="Keyword">open</a> <a id="312" class="Keyword">import</a> <a id="319" href="Level.html" class="Module">Level</a> <a id="325" class="Keyword">using</a> <a id="331" class="Symbol">(</a><a id="332" href="Agda.Primitive.html#961" class="Primitive Operator">_⊔_</a><a id="335" class="Symbol">;</a> <a id="337" href="Agda.Primitive.html#931" class="Primitive">suc</a><a id="340" class="Symbol">)</a>
 <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#10991" class="Record">ApartnessRelation</a><a id="447" 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="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>
@@ -37,8 +37,8 @@
   <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.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#10991" 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#11193" 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>
+  <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>
 
 
 <a id="1494" class="Keyword">record</a> <a id="HeytingField"></a><a id="1501" href="Algebra.Apartness.Bundles.html#1501" class="Record">HeytingField</a> <a id="1514" href="Algebra.Apartness.Bundles.html#1514" class="Bound">c</a> <a id="1516" href="Algebra.Apartness.Bundles.html#1516" class="Bound">ℓ₁</a> <a id="1519" href="Algebra.Apartness.Bundles.html#1519" class="Bound">ℓ₂</a> <a id="1522" class="Symbol">:</a> <a id="1524" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="1528" class="Symbol">(</a><a id="1529" href="Agda.Primitive.html#931" class="Primitive">suc</a> <a id="1533" class="Symbol">(</a><a id="1534" href="Algebra.Apartness.Bundles.html#1514" class="Bound">c</a> <a id="1536" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1538" href="Algebra.Apartness.Bundles.html#1516" class="Bound">ℓ₁</a> <a id="1541" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1543" href="Algebra.Apartness.Bundles.html#1519" class="Bound">ℓ₂</a><a id="1545" class="Symbol">))</a> <a id="1548" class="Keyword">where</a>
@@ -62,6 +62,6 @@
   <a id="HeytingField.heytingCommutativeRing"></a><a id="1990" href="Algebra.Apartness.Bundles.html#1990" class="Function">heytingCommutativeRing</a> <a id="2013" class="Symbol">:</a> <a id="2015" href="Algebra.Apartness.Bundles.html#641" class="Record">HeytingCommutativeRing</a> <a id="2038" href="Algebra.Apartness.Bundles.html#1514" class="Bound">c</a> <a id="2040" href="Algebra.Apartness.Bundles.html#1516" class="Bound">ℓ₁</a> <a id="2043" href="Algebra.Apartness.Bundles.html#1519" class="Bound">ℓ₂</a>
   <a id="2048" href="Algebra.Apartness.Bundles.html#1990" class="Function">heytingCommutativeRing</a> <a id="2071" class="Symbol">=</a> <a id="2073" class="Keyword">record</a> <a id="2080" class="Symbol">{</a> <a id="2082" href="Algebra.Apartness.Bundles.html#1115" class="Field">isHeytingCommutativeRing</a> <a id="2107" class="Symbol">=</a> <a id="2109" href="Algebra.Apartness.Structures.html#1707" class="Function">isHeytingCommutativeRing</a> <a id="2134" class="Symbol">}</a>
 
-  <a id="HeytingField.apartnessRelation"></a><a id="2139" href="Algebra.Apartness.Bundles.html#2139" class="Function">apartnessRelation</a> <a id="2157" class="Symbol">:</a> <a id="2159" href="Relation.Binary.Bundles.html#10991" class="Record">ApartnessRelation</a> <a id="2177" href="Algebra.Apartness.Bundles.html#1514" class="Bound">c</a> <a id="2179" href="Algebra.Apartness.Bundles.html#1516" class="Bound">ℓ₁</a> <a id="2182" href="Algebra.Apartness.Bundles.html#1519" class="Bound">ℓ₂</a>
-  <a id="2187" href="Algebra.Apartness.Bundles.html#2139" class="Function">apartnessRelation</a> <a id="2205" class="Symbol">=</a> <a id="2207" class="Keyword">record</a> <a id="2214" class="Symbol">{</a> <a id="2216" href="Relation.Binary.Bundles.html#11193" class="Field">isApartnessRelation</a> <a id="2236" class="Symbol">=</a> <a id="2238" href="Algebra.Apartness.Structures.html#1144" class="Function">isApartnessRelation</a> <a id="2258" class="Symbol">}</a>
+  <a id="HeytingField.apartnessRelation"></a><a id="2139" href="Algebra.Apartness.Bundles.html#2139" class="Function">apartnessRelation</a> <a id="2157" class="Symbol">:</a> <a id="2159" href="Relation.Binary.Bundles.html#11022" class="Record">ApartnessRelation</a> <a id="2177" href="Algebra.Apartness.Bundles.html#1514" class="Bound">c</a> <a id="2179" href="Algebra.Apartness.Bundles.html#1516" class="Bound">ℓ₁</a> <a id="2182" href="Algebra.Apartness.Bundles.html#1519" class="Bound">ℓ₂</a>
+  <a id="2187" href="Algebra.Apartness.Bundles.html#2139" class="Function">apartnessRelation</a> <a id="2205" class="Symbol">=</a> <a id="2207" class="Keyword">record</a> <a id="2214" class="Symbol">{</a> <a id="2216" href="Relation.Binary.Bundles.html#11224" class="Field">isApartnessRelation</a> <a id="2236" class="Symbol">=</a> <a id="2238" href="Algebra.Apartness.Structures.html#1144" class="Function">isApartnessRelation</a> <a id="2258" class="Symbol">}</a>
 </pre></body></html>