Skip to content

Commit

Permalink
Deploying to gh-pages from @ d55da1f 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@omelkonian
omelkonian committed Sep 13, 2024
1 parent 5ef3302 commit f0d1b77
Show file tree
Hide file tree
Showing 364 changed files with 45,520 additions and 43,233 deletions.
453 changes: 232 additions & 221 deletions Agda.Builtin.Reflection.html
View file

Large diffs are not rendered by default.

16 changes: 8 additions & 8 deletions Algebra.Apartness.Bundles.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,9 @@

<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#9903" 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#9918" 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#27248" 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#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>

<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,11 +34,11 @@

<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#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.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#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>
<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="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#9903" 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#10105" 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#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>
</pre></body></html>
Loading

0 comments on commit f0d1b77

Please sign in to comment.