Deploying to gh-pages from @ b13a032 🚀

agda · Jun 5, 2024 · 0070b74 · 0070b74
1 parent 2857149
commit 0070b74
Show file tree

Hide file tree

Showing 451 changed files with 6,263 additions and 6,182 deletions.
diff --git a/master/Algebra.Apartness.Properties.HeytingCommutativeRing.html b/master/Algebra.Apartness.Properties.HeytingCommutativeRing.html
@@ -21,7 +21,7 @@
 
 <a id="758" class="Keyword">open</a> <a id="763" class="Keyword">import</a> <a id="770" href="Algebra.Properties.Ring.html" class="Module">Algebra.Properties.Ring</a> <a id="794" href="Algebra.Bundles.html#28491" class="Function">ring</a>
   <a id="801" class="Keyword">using</a> <a id="807" class="Symbol">(</a><a id="808" href="Algebra.Properties.RingWithoutOne.html#749" class="Function">-0#≈0#</a><a id="814" class="Symbol">;</a> <a id="816" href="Algebra.Properties.RingWithoutOne.html#1218" class="Function">-‿distribˡ-*</a><a id="828" class="Symbol">;</a> <a id="830" href="Algebra.Properties.RingWithoutOne.html#1787" class="Function">-‿distribʳ-*</a><a id="842" class="Symbol">;</a> <a id="844" href="Algebra.Properties.RingWithoutOne.html#954" class="Function">-‿anti-homo-+</a><a id="857" class="Symbol">;</a> <a id="859" href="Algebra.Properties.RingWithoutOne.html#881" class="Function">-‿involutive</a><a id="871" class="Symbol">)</a>
-<a id="873" class="Keyword">open</a> <a id="878" class="Keyword">import</a> <a id="885" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a> <a id="913" class="Keyword">using</a> <a id="919" class="Symbol">(</a><a id="920" href="Relation.Binary.Definitions.html#1566" class="Function">Symmetric</a><a id="929" class="Symbol">)</a>
+<a id="873" class="Keyword">open</a> <a id="878" class="Keyword">import</a> <a id="885" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a> <a id="913" class="Keyword">using</a> <a id="919" class="Symbol">(</a><a id="920" href="Relation.Binary.Definitions.html#1491" class="Function">Symmetric</a><a id="929" class="Symbol">)</a>
 <a id="931" class="Keyword">import</a> <a id="938" href="Relation.Binary.Reasoning.Setoid.html" class="Module">Relation.Binary.Reasoning.Setoid</a> <a id="971" class="Symbol">as</a> <a id="974" class="Module">≈-Reasoning</a>
 <a id="986" class="Keyword">open</a> <a id="991" class="Keyword">import</a> <a id="998" href="Algebra.Properties.CommutativeMonoid.html" class="Module">Algebra.Properties.CommutativeMonoid</a> <a id="1035" href="Algebra.Bundles.html#18992" class="Function">*-commutativeMonoid</a>
 
@@ -65,7 +65,7 @@
       <a id="2453" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1802" class="Bound">y⁻¹</a> <a id="2457" href="Algebra.Apartness.Bundles.html#902" class="Field Operator">*</a> <a id="2459" class="Symbol">(</a><a id="2460" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1611" class="Bound">y</a> <a id="2462" href="Algebra.Structures.html#8128" class="Function Operator">-</a> <a id="2464" href="Algebra.Apartness.Bundles.html#988" class="Field">0#</a><a id="2466" class="Symbol">)</a>               <a id="2482" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="2485" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1808" class="Bound">y⁻¹*y≈1</a> <a id="2493" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>
       <a id="2501" href="Algebra.Apartness.Bundles.html#1027" class="Field">1#</a> <a id="2504" href="Relation.Binary.Reasoning.Syntax.html#12345" class="Function Operator">∎</a>
 
-<a id="#-sym"></a><a id="2507" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#2507" class="Function">#-sym</a> <a id="2513" class="Symbol">:</a> <a id="2515" href="Relation.Binary.Definitions.html#1566" class="Function">Symmetric</a> <a id="2525" href="Algebra.Apartness.Bundles.html#813" class="Field Operator">_#_</a>
+<a id="#-sym"></a><a id="2507" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#2507" class="Function">#-sym</a> <a id="2513" class="Symbol">:</a> <a id="2515" href="Relation.Binary.Definitions.html#1491" class="Function">Symmetric</a> <a id="2525" href="Algebra.Apartness.Bundles.html#813" class="Field Operator">_#_</a>
 <a id="2529" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#2507" class="Function">#-sym</a> <a id="2535" class="Symbol">{</a><a id="2536" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#2536" class="Bound">x</a><a id="2537" class="Symbol">}</a> <a id="2539" class="Symbol">{</a><a id="2540" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#2540" class="Bound">y</a><a id="2541" class="Symbol">}</a> <a id="2543" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#2543" class="Bound">x#y</a> <a id="2547" class="Symbol">=</a> <a id="2549" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1092" class="Function">invertibleˡ⇒#</a> <a id="2563" class="Symbol">(</a><a id="2564" href="Algebra.Apartness.Bundles.html#945" class="Field Operator">-</a> <a id="2566" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#2693" class="Function">x-y⁻¹</a> <a id="2572" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2574" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#2874" class="Function">x-y⁻¹*y-x≈1</a><a id="2585" class="Symbol">)</a>
   <a id="2589" class="Keyword">where</a>
   <a id="2597" class="Keyword">open</a> <a id="2602" href="Relation.Binary.Reasoning.Setoid.html" class="Module">≈-Reasoning</a> <a id="2614" href="Algebra.Structures.html#1873" class="Function">setoid</a>

diff --git a/master/Algebra.Apartness.Structures.html b/master/Algebra.Apartness.Structures.html
@@ -22,8 +22,8 @@
 <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#24177" 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#3901" 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="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>
 
 
@@ -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#3901" 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#3826" 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>
diff --git a/master/Algebra.Bundles.Raw.html b/master/Algebra.Bundles.Raw.html
@@ -12,7 +12,7 @@
 <a id="291" class="Keyword">open</a> <a id="296" class="Keyword">import</a> <a id="303" href="Algebra.Core.html" class="Module">Algebra.Core</a>
 <a id="316" class="Keyword">open</a> <a id="321" class="Keyword">import</a> <a id="328" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a> <a id="349" class="Keyword">using</a> <a id="355" class="Symbol">(</a><a id="356" href="Relation.Binary.Core.html#896" class="Function">Rel</a><a id="359" class="Symbol">)</a>
 <a id="361" class="Keyword">open</a> <a id="366" class="Keyword">import</a> <a id="373" href="Level.html" class="Module">Level</a> <a id="379" class="Keyword">using</a> <a id="385" class="Symbol">(</a><a id="386" href="Agda.Primitive.html#931" class="Primitive">suc</a><a id="389" class="Symbol">;</a> <a id="391" href="Agda.Primitive.html#961" class="Primitive Operator">_⊔_</a><a id="394" class="Symbol">)</a>
-<a id="396" class="Keyword">open</a> <a id="401" class="Keyword">import</a> <a id="408" href="Relation.Nullary.Negation.Core.html" class="Module">Relation.Nullary.Negation.Core</a> <a id="439" class="Keyword">using</a> <a id="445" class="Symbol">(</a><a id="446" href="Relation.Nullary.Negation.Core.html#698" class="Function Operator">¬_</a><a id="448" class="Symbol">)</a>
+<a id="396" class="Keyword">open</a> <a id="401" class="Keyword">import</a> <a id="408" href="Relation.Nullary.Negation.Core.html" class="Module">Relation.Nullary.Negation.Core</a> <a id="439" class="Keyword">using</a> <a id="445" class="Symbol">(</a><a id="446" href="Relation.Nullary.Negation.Core.html#658" class="Function Operator">¬_</a><a id="448" class="Symbol">)</a>
 
 <a id="451" class="Comment">------------------------------------------------------------------------</a>
 <a id="524" class="Comment">-- Raw bundles with 1 unary operation &amp; 1 element</a>
@@ -42,7 +42,7 @@
 
   <a id="1227" class="Keyword">infix</a> <a id="1233" class="Number">4</a> <a id="1235" href="Algebra.Bundles.Raw.html#1241" class="Function Operator">_≉_</a>
   <a id="RawMagma._≉_"></a><a id="1241" href="Algebra.Bundles.Raw.html#1241" class="Function Operator">_≉_</a> <a id="1245" class="Symbol">:</a> <a id="1247" href="Relation.Binary.Core.html#896" class="Function">Rel</a> <a id="1251" href="Algebra.Bundles.Raw.html#1154" class="Field">Carrier</a> <a id="1259" class="Symbol">_</a>
-  <a id="1263" href="Algebra.Bundles.Raw.html#1263" class="Bound">x</a> <a id="1265" href="Algebra.Bundles.Raw.html#1241" class="Function Operator">≉</a> <a id="1267" href="Algebra.Bundles.Raw.html#1267" class="Bound">y</a> <a id="1269" class="Symbol">=</a> <a id="1271" href="Relation.Nullary.Negation.Core.html#698" class="Function Operator">¬</a> <a id="1273" class="Symbol">(</a><a id="1274" href="Algebra.Bundles.Raw.html#1263" class="Bound">x</a> <a id="1276" href="Algebra.Bundles.Raw.html#1174" class="Field Operator">≈</a> <a id="1278" href="Algebra.Bundles.Raw.html#1267" class="Bound">y</a><a id="1279" class="Symbol">)</a>
+  <a id="1263" href="Algebra.Bundles.Raw.html#1263" class="Bound">x</a> <a id="1265" href="Algebra.Bundles.Raw.html#1241" class="Function Operator">≉</a> <a id="1267" href="Algebra.Bundles.Raw.html#1267" class="Bound">y</a> <a id="1269" class="Symbol">=</a> <a id="1271" href="Relation.Nullary.Negation.Core.html#658" class="Function Operator">¬</a> <a id="1273" class="Symbol">(</a><a id="1274" href="Algebra.Bundles.Raw.html#1263" class="Bound">x</a> <a id="1276" href="Algebra.Bundles.Raw.html#1174" class="Field Operator">≈</a> <a id="1278" href="Algebra.Bundles.Raw.html#1267" class="Bound">y</a><a id="1279" class="Symbol">)</a>
 
 <a id="1282" class="Comment">------------------------------------------------------------------------</a>
 <a id="1355" class="Comment">-- Raw bundles with 1 binary operation &amp; 1 element</a>

diff --git a/master/Algebra.Consequences.Base.html b/master/Algebra.Consequences.Base.html
@@ -15,7 +15,7 @@
 <a id="451" class="Keyword">open</a> <a id="456" class="Keyword">import</a> <a id="463" href="Algebra.Definitions.html" class="Module">Algebra.Definitions</a>
 <a id="483" class="Keyword">open</a> <a id="488" class="Keyword">import</a> <a id="495" href="Data.Sum.Base.html" class="Module">Data.Sum.Base</a>
 <a id="509" class="Keyword">open</a> <a id="514" class="Keyword">import</a> <a id="521" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a>
-<a id="542" class="Keyword">open</a> <a id="547" class="Keyword">import</a> <a id="554" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a> <a id="582" class="Keyword">using</a> <a id="588" class="Symbol">(</a><a id="589" href="Relation.Binary.Definitions.html#1407" class="Function">Reflexive</a><a id="598" class="Symbol">)</a>
+<a id="542" class="Keyword">open</a> <a id="547" class="Keyword">import</a> <a id="554" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a> <a id="582" class="Keyword">using</a> <a id="588" class="Symbol">(</a><a id="589" href="Relation.Binary.Definitions.html#1332" class="Function">Reflexive</a><a id="598" class="Symbol">)</a>
 
 <a id="601" class="Keyword">module</a> <a id="608" href="Algebra.Consequences.Base.html#608" class="Module">_</a> <a id="610" class="Symbol">{</a><a id="611" href="Algebra.Consequences.Base.html#611" class="Bound">ℓ</a><a id="612" class="Symbol">}</a> <a id="614" class="Symbol">{</a><a id="615" href="Algebra.Consequences.Base.html#615" class="Bound Operator">_•_</a> <a id="619" class="Symbol">:</a> <a id="621" href="Algebra.Core.html#527" class="Function">Op₂</a> <a id="625" href="Algebra.Consequences.Base.html#408" class="Bound">A</a><a id="626" class="Symbol">}</a> <a id="628" class="Symbol">(</a><a id="629" href="Algebra.Consequences.Base.html#629" class="Bound Operator">_≈_</a> <a id="633" class="Symbol">:</a> <a id="635" href="Relation.Binary.Core.html#896" class="Function">Rel</a> <a id="639" href="Algebra.Consequences.Base.html#408" class="Bound">A</a> <a id="641" href="Algebra.Consequences.Base.html#611" class="Bound">ℓ</a><a id="642" class="Symbol">)</a> <a id="644" class="Keyword">where</a>
 
@@ -24,7 +24,7 @@
 
 <a id="740" class="Keyword">module</a> <a id="747" href="Algebra.Consequences.Base.html#747" class="Module">_</a> <a id="749" class="Symbol">{</a><a id="750" href="Algebra.Consequences.Base.html#750" class="Bound">ℓ</a><a id="751" class="Symbol">}</a> <a id="753" class="Symbol">{</a><a id="754" href="Algebra.Consequences.Base.html#754" class="Bound">f</a> <a id="756" class="Symbol">:</a> <a id="758" href="Algebra.Core.html#484" class="Function">Op₁</a> <a id="762" href="Algebra.Consequences.Base.html#408" class="Bound">A</a><a id="763" class="Symbol">}</a> <a id="765" class="Symbol">(</a><a id="766" href="Algebra.Consequences.Base.html#766" class="Bound Operator">_≈_</a> <a id="770" class="Symbol">:</a> <a id="772" href="Relation.Binary.Core.html#896" class="Function">Rel</a> <a id="776" href="Algebra.Consequences.Base.html#408" class="Bound">A</a> <a id="778" href="Algebra.Consequences.Base.html#750" class="Bound">ℓ</a><a id="779" class="Symbol">)</a> <a id="781" class="Keyword">where</a>
 
-  <a id="790" href="Algebra.Consequences.Base.html#790" class="Function">reflexive∧selfInverse⇒involutive</a> <a id="823" class="Symbol">:</a> <a id="825" href="Relation.Binary.Definitions.html#1407" class="Function">Reflexive</a> <a id="835" href="Algebra.Consequences.Base.html#766" class="Bound Operator">_≈_</a> <a id="839" class="Symbol">→</a>
+  <a id="790" href="Algebra.Consequences.Base.html#790" class="Function">reflexive∧selfInverse⇒involutive</a> <a id="823" class="Symbol">:</a> <a id="825" href="Relation.Binary.Definitions.html#1332" class="Function">Reflexive</a> <a id="835" href="Algebra.Consequences.Base.html#766" class="Bound Operator">_≈_</a> <a id="839" class="Symbol">→</a>
                                      <a id="878" href="Algebra.Definitions.html#4200" class="Function">SelfInverse</a> <a id="890" href="Algebra.Consequences.Base.html#766" class="Bound Operator">_≈_</a> <a id="894" href="Algebra.Consequences.Base.html#754" class="Bound">f</a> <a id="896" class="Symbol">→</a>
                                      <a id="935" href="Algebra.Definitions.html#4273" class="Function">Involutive</a> <a id="946" href="Algebra.Consequences.Base.html#766" class="Bound Operator">_≈_</a> <a id="950" href="Algebra.Consequences.Base.html#754" class="Bound">f</a>
   <a id="954" href="Algebra.Consequences.Base.html#790" class="Function">reflexive∧selfInverse⇒involutive</a> <a id="987" href="Algebra.Consequences.Base.html#987" class="Bound">refl</a> <a id="992" href="Algebra.Consequences.Base.html#992" class="Bound">inv</a> <a id="996" class="Symbol">_</a> <a id="998" class="Symbol">=</a> <a id="1000" href="Algebra.Consequences.Base.html#992" class="Bound">inv</a> <a id="1004" href="Algebra.Consequences.Base.html#987" class="Bound">refl</a>