Skip to content

Commit

Permalink
Deploying to gh-pages from @ d38e964 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@github-merge-queue
github-merge-queue[bot] committed Dec 10, 2024
1 parent dfd3d5e commit 8a1ae40
Show file tree
Hide file tree
Showing 63 changed files with 1,390 additions and 1,377 deletions.
18 changes: 9 additions & 9 deletions master/Algebra.Apartness.Properties.HeytingCommutativeRing.html
View file

Large diffs are not rendered by default.

6 changes: 3 additions & 3 deletions master/Algebra.Apartness.Structures.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
<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#25369" 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#25812" 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#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>
Expand All @@ -30,10 +30,10 @@
<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#25369" 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#25812" 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#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#25369" 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#25812" 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#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>
Expand Down
Loading

0 comments on commit 8a1ae40

Please sign in to comment.