Skip to content

Commit

Permalink
Deploying to gh-pages from @ 6078b64 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@github-merge-queue
github-merge-queue[bot] committed Oct 7, 2024
1 parent c1ef807 commit 29e72d6
Show file tree
Hide file tree
Showing 123 changed files with 2,335 additions and 2,294 deletions.
10 changes: 5 additions & 5 deletions master/Algebra.Apartness.Bundles.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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#9918" 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#10630" 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#29926" 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>
Expand All @@ -37,8 +37,8 @@
<a id="HeytingCommutativeRing.commutativeRing"></a><a id="1211" href="Algebra.Apartness.Bundles.html#1211" class="Function">commutativeRing</a> <a id="1227" class="Symbol">:</a> <a id="1229" href="Algebra.Bundles.html#29926" class="Record">CommutativeRing</a> <a id="1245" href="Algebra.Apartness.Bundles.html#615" class="Bound">c</a> <a id="1247" href="Algebra.Apartness.Bundles.html#617" class="Bound">ℓ₁</a>
<a id="1252" href="Algebra.Apartness.Bundles.html#1211" class="Function">commutativeRing</a> <a id="1268" class="Symbol">=</a> <a id="1270" class="Keyword">record</a> <a id="1277" class="Symbol">{</a> <a id="1279" href="Algebra.Bundles.html#30283" class="Field">isCommutativeRing</a> <a id="1297" class="Symbol">=</a> <a id="1299" href="Algebra.Apartness.Structures.html#1083" class="Function">isCommutativeRing</a> <a id="1317" class="Symbol">}</a>

<a id="HeytingCommutativeRing.apartnessRelation"></a><a id="1322" href="Algebra.Apartness.Bundles.html#1322" class="Function">apartnessRelation</a> <a id="1340" class="Symbol">:</a> <a id="1342" href="Relation.Binary.Bundles.html#9918" class="Record">ApartnessRelation</a> <a id="1360" href="Algebra.Apartness.Bundles.html#615" class="Bound">c</a> <a id="1362" href="Algebra.Apartness.Bundles.html#617" class="Bound">ℓ₁</a> <a id="1365" href="Algebra.Apartness.Bundles.html#620" class="Bound">ℓ₂</a>
<a id="1370" href="Algebra.Apartness.Bundles.html#1322" class="Function">apartnessRelation</a> <a id="1388" class="Symbol">=</a> <a id="1390" class="Keyword">record</a> <a id="1397" class="Symbol">{</a> <a id="1399" href="Relation.Binary.Bundles.html#10120" class="Field">isApartnessRelation</a> <a id="1419" class="Symbol">=</a> <a id="1421" href="Algebra.Apartness.Structures.html#1144" class="Function">isApartnessRelation</a> <a id="1441" class="Symbol">}</a>
<a id="HeytingCommutativeRing.apartnessRelation"></a><a id="1322" href="Algebra.Apartness.Bundles.html#1322" class="Function">apartnessRelation</a> <a id="1340" class="Symbol">:</a> <a id="1342" href="Relation.Binary.Bundles.html#10630" class="Record">ApartnessRelation</a> <a id="1360" href="Algebra.Apartness.Bundles.html#615" class="Bound">c</a> <a id="1362" href="Algebra.Apartness.Bundles.html#617" class="Bound">ℓ₁</a> <a id="1365" href="Algebra.Apartness.Bundles.html#620" class="Bound">ℓ₂</a>
<a id="1370" href="Algebra.Apartness.Bundles.html#1322" class="Function">apartnessRelation</a> <a id="1388" class="Symbol">=</a> <a id="1390" class="Keyword">record</a> <a id="1397" class="Symbol">{</a> <a id="1399" href="Relation.Binary.Bundles.html#10832" class="Field">isApartnessRelation</a> <a id="1419" class="Symbol">=</a> <a id="1421" href="Algebra.Apartness.Structures.html#1144" class="Function">isApartnessRelation</a> <a id="1441" class="Symbol">}</a>


<a id="1445" class="Keyword">record</a> <a id="HeytingField"></a><a id="1452" href="Algebra.Apartness.Bundles.html#1452" class="Record">HeytingField</a> <a id="1465" href="Algebra.Apartness.Bundles.html#1465" class="Bound">c</a> <a id="1467" href="Algebra.Apartness.Bundles.html#1467" class="Bound">ℓ₁</a> <a id="1470" href="Algebra.Apartness.Bundles.html#1470" class="Bound">ℓ₂</a> <a id="1473" class="Symbol">:</a> <a id="1475" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="1479" class="Symbol">(</a><a id="1480" href="Agda.Primitive.html#931" class="Primitive">suc</a> <a id="1484" class="Symbol">(</a><a id="1485" href="Algebra.Apartness.Bundles.html#1465" class="Bound">c</a> <a id="1487" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1489" href="Algebra.Apartness.Bundles.html#1467" class="Bound">ℓ₁</a> <a id="1492" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1494" href="Algebra.Apartness.Bundles.html#1470" class="Bound">ℓ₂</a><a id="1496" class="Symbol">))</a> <a id="1499" class="Keyword">where</a>
Expand All @@ -62,6 +62,6 @@
<a id="HeytingField.heytingCommutativeRing"></a><a id="1941" href="Algebra.Apartness.Bundles.html#1941" class="Function">heytingCommutativeRing</a> <a id="1964" class="Symbol">:</a> <a id="1966" href="Algebra.Apartness.Bundles.html#592" class="Record">HeytingCommutativeRing</a> <a id="1989" href="Algebra.Apartness.Bundles.html#1465" class="Bound">c</a> <a id="1991" href="Algebra.Apartness.Bundles.html#1467" class="Bound">ℓ₁</a> <a id="1994" href="Algebra.Apartness.Bundles.html#1470" class="Bound">ℓ₂</a>
<a id="1999" href="Algebra.Apartness.Bundles.html#1941" class="Function">heytingCommutativeRing</a> <a id="2022" class="Symbol">=</a> <a id="2024" class="Keyword">record</a> <a id="2031" class="Symbol">{</a> <a id="2033" href="Algebra.Apartness.Bundles.html#1066" class="Field">isHeytingCommutativeRing</a> <a id="2058" class="Symbol">=</a> <a id="2060" href="Algebra.Apartness.Structures.html#1604" class="Function">isHeytingCommutativeRing</a> <a id="2085" class="Symbol">}</a>

<a id="HeytingField.apartnessRelation"></a><a id="2090" href="Algebra.Apartness.Bundles.html#2090" class="Function">apartnessRelation</a> <a id="2108" class="Symbol">:</a> <a id="2110" href="Relation.Binary.Bundles.html#9918" class="Record">ApartnessRelation</a> <a id="2128" href="Algebra.Apartness.Bundles.html#1465" class="Bound">c</a> <a id="2130" href="Algebra.Apartness.Bundles.html#1467" class="Bound">ℓ₁</a> <a id="2133" href="Algebra.Apartness.Bundles.html#1470" class="Bound">ℓ₂</a>
<a id="2138" href="Algebra.Apartness.Bundles.html#2090" class="Function">apartnessRelation</a> <a id="2156" class="Symbol">=</a> <a id="2158" class="Keyword">record</a> <a id="2165" class="Symbol">{</a> <a id="2167" href="Relation.Binary.Bundles.html#10120" class="Field">isApartnessRelation</a> <a id="2187" class="Symbol">=</a> <a id="2189" href="Algebra.Apartness.Structures.html#1144" class="Function">isApartnessRelation</a> <a id="2209" class="Symbol">}</a>
<a id="HeytingField.apartnessRelation"></a><a id="2090" href="Algebra.Apartness.Bundles.html#2090" class="Function">apartnessRelation</a> <a id="2108" class="Symbol">:</a> <a id="2110" href="Relation.Binary.Bundles.html#10630" class="Record">ApartnessRelation</a> <a id="2128" href="Algebra.Apartness.Bundles.html#1465" class="Bound">c</a> <a id="2130" href="Algebra.Apartness.Bundles.html#1467" class="Bound">ℓ₁</a> <a id="2133" href="Algebra.Apartness.Bundles.html#1470" class="Bound">ℓ₂</a>
<a id="2138" href="Algebra.Apartness.Bundles.html#2090" class="Function">apartnessRelation</a> <a id="2156" class="Symbol">=</a> <a id="2158" class="Keyword">record</a> <a id="2165" class="Symbol">{</a> <a id="2167" href="Relation.Binary.Bundles.html#10832" class="Field">isApartnessRelation</a> <a id="2187" class="Symbol">=</a> <a id="2189" href="Algebra.Apartness.Structures.html#1144" class="Function">isApartnessRelation</a> <a id="2209" class="Symbol">}</a>
</pre></body></html>
8 changes: 4 additions & 4 deletions master/Algebra.Apartness.Structures.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
<a id="587" class="Keyword">open</a> <a id="592" class="Keyword">import</a> <a id="599" href="Data.Product.Base.html" class="Module">Data.Product.Base</a> <a id="617" class="Keyword">using</a> <a id="623" class="Symbol">(</a><a id="624" href="Data.Product.Base.html#1371" class="Function">∃-syntax</a><a id="632" class="Symbol">;</a> <a id="634" href="Data.Product.Base.html#1618" class="Function Operator">_×_</a><a id="637" class="Symbol">;</a> <a id="639" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">_,_</a><a id="642" class="Symbol">;</a> <a id="644" href="Data.Product.Base.html#650" class="Field">proj₂</a><a id="649" class="Symbol">)</a>
<a id="651" class="Keyword">open</a> <a id="656" class="Keyword">import</a> <a id="663" href="Algebra.Definitions.html" class="Module">Algebra.Definitions</a> <a id="683" href="Algebra.Apartness.Structures.html#433" class="Bound Operator">_≈_</a> <a id="687" class="Keyword">using</a> <a id="693" class="Symbol">(</a><a id="694" href="Algebra.Definitions.html#2813" class="Function">Invertible</a><a id="704" class="Symbol">)</a>
<a id="706" class="Keyword">open</a> <a id="711" class="Keyword">import</a> <a id="718" href="Algebra.Structures.html" class="Module">Algebra.Structures</a> <a id="737" href="Algebra.Apartness.Structures.html#433" class="Bound Operator">_≈_</a> <a id="741" class="Keyword">using</a> <a id="747" class="Symbol">(</a><a id="748" href="Algebra.Structures.html#25447" class="Record">IsCommutativeRing</a><a id="765" class="Symbol">)</a>
<a id="767" class="Keyword">open</a> <a id="772" class="Keyword">import</a> <a id="779" href="Relation.Binary.Structures.html" class="Module">Relation.Binary.Structures</a> <a id="806" class="Keyword">using</a> <a id="812" class="Symbol">(</a><a id="813" href="Relation.Binary.Structures.html#1550" class="Record">IsEquivalence</a><a id="826" class="Symbol">;</a> <a id="828" href="Relation.Binary.Structures.html#8358" class="Record">IsApartnessRelation</a><a id="847" class="Symbol">)</a>
<a id="767" class="Keyword">open</a> <a id="772" class="Keyword">import</a> <a id="779" href="Relation.Binary.Structures.html" class="Module">Relation.Binary.Structures</a> <a id="806" class="Keyword">using</a> <a id="812" class="Symbol">(</a><a id="813" href="Relation.Binary.Structures.html#1550" class="Record">IsEquivalence</a><a id="826" class="Symbol">;</a> <a id="828" href="Relation.Binary.Structures.html#8654" class="Record">IsApartnessRelation</a><a id="847" class="Symbol">)</a>
<a id="849" class="Keyword">open</a> <a id="854" class="Keyword">import</a> <a id="861" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a> <a id="889" class="Keyword">using</a> <a id="895" class="Symbol">(</a><a id="896" href="Relation.Binary.Definitions.html#3826" class="Function">Tight</a><a id="901" class="Symbol">)</a>
<a id="903" class="Keyword">open</a> <a id="908" class="Keyword">import</a> <a id="915" href="Relation.Nullary.Negation.html" class="Module">Relation.Nullary.Negation</a> <a id="941" class="Keyword">using</a> <a id="947" class="Symbol">(</a><a id="948" href="Relation.Nullary.Negation.Core.html#658" class="Function Operator">¬_</a><a id="950" class="Symbol">)</a>
<a id="952" class="Keyword">import</a> <a id="959" href="Relation.Binary.Properties.ApartnessRelation.html" class="Module">Relation.Binary.Properties.ApartnessRelation</a> <a id="1004" class="Symbol">as</a> <a id="1007" class="Module">AR</a>
Expand All @@ -31,16 +31,16 @@

<a id="1073" class="Keyword">field</a>
<a id="IsHeytingCommutativeRing.isCommutativeRing"></a><a id="1083" href="Algebra.Apartness.Structures.html#1083" class="Field">isCommutativeRing</a> <a id="1103" class="Symbol">:</a> <a id="1105" href="Algebra.Structures.html#25447" class="Record">IsCommutativeRing</a> <a id="1123" href="Algebra.Apartness.Structures.html#483" class="Bound Operator">_+_</a> <a id="1127" href="Algebra.Apartness.Structures.html#487" class="Bound Operator">_*_</a> <a id="1131" href="Algebra.Apartness.Structures.html#507" class="Bound Operator">-_</a> <a id="1134" href="Algebra.Apartness.Structures.html#526" class="Bound">0#</a> <a id="1137" href="Algebra.Apartness.Structures.html#529" class="Bound">1#</a>
<a id="IsHeytingCommutativeRing.isApartnessRelation"></a><a id="1144" href="Algebra.Apartness.Structures.html#1144" class="Field">isApartnessRelation</a> <a id="1164" class="Symbol">:</a> <a id="1166" href="Relation.Binary.Structures.html#8358" class="Record">IsApartnessRelation</a> <a id="1186" href="Algebra.Apartness.Structures.html#433" class="Bound Operator">_≈_</a> <a id="1190" href="Algebra.Apartness.Structures.html#458" class="Bound Operator">_#_</a>
<a id="IsHeytingCommutativeRing.isApartnessRelation"></a><a id="1144" href="Algebra.Apartness.Structures.html#1144" class="Field">isApartnessRelation</a> <a id="1164" class="Symbol">:</a> <a id="1166" href="Relation.Binary.Structures.html#8654" class="Record">IsApartnessRelation</a> <a id="1186" href="Algebra.Apartness.Structures.html#433" class="Bound Operator">_≈_</a> <a id="1190" href="Algebra.Apartness.Structures.html#458" class="Bound Operator">_#_</a>

<a id="1197" class="Keyword">open</a> <a id="1202" href="Algebra.Structures.html#25447" class="Module">IsCommutativeRing</a> <a id="1220" href="Algebra.Apartness.Structures.html#1083" class="Field">isCommutativeRing</a> <a id="1238" class="Keyword">public</a>
<a id="1247" class="Keyword">open</a> <a id="1252" href="Relation.Binary.Structures.html#8358" class="Module">IsApartnessRelation</a> <a id="1272" href="Algebra.Apartness.Structures.html#1144" class="Field">isApartnessRelation</a> <a id="1292" class="Keyword">public</a>
<a id="1247" class="Keyword">open</a> <a id="1252" href="Relation.Binary.Structures.html#8654" class="Module">IsApartnessRelation</a> <a id="1272" href="Algebra.Apartness.Structures.html#1144" class="Field">isApartnessRelation</a> <a id="1292" class="Keyword">public</a>

<a id="1302" class="Keyword">field</a>
<a id="IsHeytingCommutativeRing.#⇒invertible"></a><a id="1312" href="Algebra.Apartness.Structures.html#1312" class="Field">#⇒invertible</a> <a id="1325" class="Symbol">:</a> <a id="1327" class="Symbol">∀</a> <a id="1329" class="Symbol">{</a><a id="1330" href="Algebra.Apartness.Structures.html#1330" class="Bound">x</a> <a id="1332" href="Algebra.Apartness.Structures.html#1332" class="Bound">y</a><a id="1333" class="Symbol">}</a> <a id="1335" class="Symbol">→</a> <a id="1337" href="Algebra.Apartness.Structures.html#1330" class="Bound">x</a> <a id="1339" href="Algebra.Apartness.Structures.html#458" class="Bound Operator">#</a> <a id="1341" href="Algebra.Apartness.Structures.html#1332" class="Bound">y</a> <a id="1343" class="Symbol">→</a> <a id="1345" href="Algebra.Definitions.html#2813" class="Function">Invertible</a> <a id="1356" href="Algebra.Apartness.Structures.html#529" class="Bound">1#</a> <a id="1359" href="Algebra.Apartness.Structures.html#487" class="Bound Operator">_*_</a> <a id="1363" class="Symbol">(</a><a id="1364" href="Algebra.Apartness.Structures.html#1330" class="Bound">x</a> <a id="1366" href="Algebra.Structures.html#8953" class="Function Operator">-</a> <a id="1368" href="Algebra.Apartness.Structures.html#1332" class="Bound">y</a><a id="1369" class="Symbol">)</a>
<a id="IsHeytingCommutativeRing.invertible⇒#"></a><a id="1375" href="Algebra.Apartness.Structures.html#1375" class="Field">invertible⇒#</a> <a id="1388" class="Symbol">:</a> <a id="1390" class="Symbol">∀</a> <a id="1392" class="Symbol">{</a><a id="1393" href="Algebra.Apartness.Structures.html#1393" class="Bound">x</a> <a id="1395" href="Algebra.Apartness.Structures.html#1395" class="Bound">y</a><a id="1396" class="Symbol">}</a> <a id="1398" class="Symbol">→</a> <a id="1400" href="Algebra.Definitions.html#2813" class="Function">Invertible</a> <a id="1411" href="Algebra.Apartness.Structures.html#529" class="Bound">1#</a> <a id="1414" href="Algebra.Apartness.Structures.html#487" class="Bound Operator">_*_</a> <a id="1418" class="Symbol">(</a><a id="1419" href="Algebra.Apartness.Structures.html#1393" class="Bound">x</a> <a id="1421" href="Algebra.Structures.html#8953" class="Function Operator">-</a> <a id="1423" href="Algebra.Apartness.Structures.html#1395" class="Bound">y</a><a id="1424" class="Symbol">)</a> <a id="1426" class="Symbol">→</a> <a id="1428" href="Algebra.Apartness.Structures.html#1393" class="Bound">x</a> <a id="1430" href="Algebra.Apartness.Structures.html#458" class="Bound Operator">#</a> <a id="1432" href="Algebra.Apartness.Structures.html#1395" class="Bound">y</a>

<a id="IsHeytingCommutativeRing.¬#-isEquivalence"></a><a id="1437" href="Algebra.Apartness.Structures.html#1437" class="Function">¬#-isEquivalence</a> <a id="1454" class="Symbol">:</a> <a id="1456" href="Relation.Binary.Structures.html#1550" class="Record">IsEquivalence</a> <a id="1470" href="Relation.Binary.Structures.html#8524" class="Function Operator">_¬#_</a>
<a id="IsHeytingCommutativeRing.¬#-isEquivalence"></a><a id="1437" href="Algebra.Apartness.Structures.html#1437" class="Function">¬#-isEquivalence</a> <a id="1454" class="Symbol">:</a> <a id="1456" href="Relation.Binary.Structures.html#1550" class="Record">IsEquivalence</a> <a id="1470" href="Relation.Binary.Structures.html#8820" class="Function Operator">_¬#_</a>
<a id="1477" href="Algebra.Apartness.Structures.html#1437" class="Function">¬#-isEquivalence</a> <a id="1494" class="Symbol">=</a> <a id="1496" href="Relation.Binary.Properties.ApartnessRelation.html#723" class="Function">AR.¬#-isEquivalence</a> <a id="1516" href="Relation.Binary.Structures.html#1596" class="Function">refl</a> <a id="1521" href="Algebra.Apartness.Structures.html#1144" class="Field">isApartnessRelation</a>


Expand Down
Loading

0 comments on commit 29e72d6

Please sign in to comment.