Skip to content

Commit

Permalink
Deploying to gh-pages from @ 4eaf23d 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@omelkonian
omelkonian committed Mar 26, 2024
1 parent 7e4da10 commit 2267a65
Show file tree
Hide file tree
Showing 276 changed files with 18,151 additions and 15,997 deletions.
6 changes: 3 additions & 3 deletions Algebra.Apartness.Bundles.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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#9903" 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#27143" 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#27248" 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="585" class="Keyword">record</a> <a id="HeytingCommutativeRing"></a><a id="592" href="Algebra.Apartness.Bundles.html#592" class="Record">HeytingCommutativeRing</a> <a id="615" href="Algebra.Apartness.Bundles.html#615" class="Bound">c</a> <a id="617" href="Algebra.Apartness.Bundles.html#617" class="Bound">ℓ₁</a> <a id="620" href="Algebra.Apartness.Bundles.html#620" class="Bound">ℓ₂</a> <a id="623" class="Symbol">:</a> <a id="625" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="629" class="Symbol">(</a><a id="630" href="Agda.Primitive.html#931" class="Primitive">suc</a> <a id="634" class="Symbol">(</a><a id="635" href="Algebra.Apartness.Bundles.html#615" class="Bound">c</a> <a id="637" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="639" href="Algebra.Apartness.Bundles.html#617" class="Bound">ℓ₁</a> <a id="642" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="644" href="Algebra.Apartness.Bundles.html#620" class="Bound">ℓ₂</a><a id="646" class="Symbol">))</a> <a id="649" class="Keyword">where</a>
Expand All @@ -34,8 +34,8 @@

<a id="1146" class="Keyword">open</a> <a id="1151" href="Algebra.Apartness.Structures.html#1019" class="Module">IsHeytingCommutativeRing</a> <a id="1176" href="Algebra.Apartness.Bundles.html#1066" class="Field">isHeytingCommutativeRing</a> <a id="1201" class="Keyword">public</a>

<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#27143" 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#27500" 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.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#27248" 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#27605" 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#9903" 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#10105" 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>
Expand Down
10 changes: 5 additions & 5 deletions Algebra.Apartness.Structures.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,20 +20,20 @@
<a id="552" class="Keyword">open</a> <a id="557" class="Keyword">import</a> <a id="564" href="Level.html" class="Module">Level</a> <a id="570" class="Keyword">using</a> <a id="576" class="Symbol">(</a><a id="577" href="Agda.Primitive.html#961" class="Primitive Operator">_⊔_</a><a id="580" class="Symbol">;</a> <a id="582" href="Agda.Primitive.html#931" class="Primitive">suc</a><a id="585" class="Symbol">)</a>
<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#24288" class="Record">IsCommutativeRing</a><a id="765" 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#23275" 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="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#3921" class="Function">Tight</a><a id="901" 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#3922" 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#698" 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>


<a id="1012" class="Keyword">record</a> <a id="IsHeytingCommutativeRing"></a><a id="1019" href="Algebra.Apartness.Structures.html#1019" class="Record">IsHeytingCommutativeRing</a> <a id="1044" class="Symbol">:</a> <a id="1046" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="1050" class="Symbol">(</a><a id="1051" href="Algebra.Apartness.Structures.html#403" class="Bound">c</a> <a id="1053" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1055" href="Algebra.Apartness.Structures.html#405" class="Bound">ℓ₁</a> <a id="1058" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1060" href="Algebra.Apartness.Structures.html#408" class="Bound">ℓ₂</a><a id="1062" class="Symbol">)</a> <a id="1064" class="Keyword">where</a>

<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#24288" 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.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#23275" 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="1197" class="Keyword">open</a> <a id="1202" href="Algebra.Structures.html#24288" 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="1197" class="Keyword">open</a> <a id="1202" href="Algebra.Structures.html#23275" 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="1302" class="Keyword">field</a>
Expand All @@ -48,7 +48,7 @@

<a id="1594" class="Keyword">field</a>
<a id="IsHeytingField.isHeytingCommutativeRing"></a><a id="1604" href="Algebra.Apartness.Structures.html#1604" class="Field">isHeytingCommutativeRing</a> <a id="1629" class="Symbol">:</a> <a id="1631" href="Algebra.Apartness.Structures.html#1019" class="Record">IsHeytingCommutativeRing</a>
<a id="IsHeytingField.tight"></a><a id="1660" href="Algebra.Apartness.Structures.html#1660" class="Field">tight</a> <a id="1685" class="Symbol">:</a> <a id="1687" href="Relation.Binary.Definitions.html#3921" class="Function">Tight</a> <a id="1693" href="Algebra.Apartness.Structures.html#433" class="Bound Operator">_≈_</a> <a id="1697" href="Algebra.Apartness.Structures.html#458" class="Bound Operator">_#_</a>
<a id="IsHeytingField.tight"></a><a id="1660" href="Algebra.Apartness.Structures.html#1660" class="Field">tight</a> <a id="1685" class="Symbol">:</a> <a id="1687" href="Relation.Binary.Definitions.html#3922" class="Function">Tight</a> <a id="1693" href="Algebra.Apartness.Structures.html#433" class="Bound Operator">_≈_</a> <a id="1697" href="Algebra.Apartness.Structures.html#458" class="Bound Operator">_#_</a>

<a id="1704" class="Keyword">open</a> <a id="1709" href="Algebra.Apartness.Structures.html#1019" class="Module">IsHeytingCommutativeRing</a> <a id="1734" href="Algebra.Apartness.Structures.html#1604" class="Field">isHeytingCommutativeRing</a> <a id="1759" class="Keyword">public</a>
</pre></body></html>
Loading

0 comments on commit 2267a65

Please sign in to comment.