Skip to content

Commit

Permalink
update html docs
Browse files Browse the repository at this point in the history
  • Loading branch information
@williamdemeo
williamdemeo committed Sep 19, 2021
1 parent dbf8e9f commit e9ce43b
Show file tree
Hide file tree
Showing 35 changed files with 969 additions and 1,094 deletions.
2 changes: 2 additions & 0 deletions UALib/html/Agda.css
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
.Agda .PrimitiveType { color: #0000CD }
.Agda .Pragma { color: black }
.Agda .Operator {}
.Agda .Hole { background: #B4EEB4 }

/* NameKinds. */
.Agda .Bound { color: black }
Expand Down Expand Up @@ -37,3 +38,4 @@
/* Standard attributes. */
.Agda a { text-decoration: none }
.Agda a[href]:hover { background-color: #B4EEB4 }
.Agda [href].hover-highlight { background-color: #B4EEB4; }
24 changes: 12 additions & 12 deletions UALib/html/Algebras.Algebras.md
View file

Large diffs are not rendered by default.

28 changes: 14 additions & 14 deletions UALib/html/Algebras.Congruences.md
View file

Large diffs are not rendered by default.

14 changes: 7 additions & 7 deletions UALib/html/Algebras.Products.md
View file

Large diffs are not rendered by default.

10 changes: 5 additions & 5 deletions UALib/html/Algebras.Signatures.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ This section presents the [Algebras.Signatures][] module of the [Agda Universal

<a id="318" class="Symbol">{-#</a> <a id="322" class="Keyword">OPTIONS</a> <a id="330" class="Pragma">--without-K</a> <a id="342" class="Pragma">--exact-split</a> <a id="356" class="Pragma">--safe</a> <a id="363" class="Symbol">#-}</a>

<a id="368" class="Keyword">open</a> <a id="373" class="Keyword">import</a> <a id="380" href="Universes.html" class="Module">Universes</a> <a id="390" class="Keyword">using</a> <a id="396" class="Symbol">(</a><a id="397" href="Agda.Primitive.html#590" class="Primitive">𝓤₀</a><a id="399" class="Symbol">)</a>
<a id="368" class="Keyword">open</a> <a id="373" class="Keyword">import</a> <a id="380" href="Universes.html" class="Module">Universes</a> <a id="390" class="Keyword">using</a> <a id="396" class="Symbol">(</a><a id="397" href="Agda.Primitive.html#764" class="Primitive">𝓤₀</a><a id="399" class="Symbol">)</a>

<a id="402" class="Keyword">module</a> <a id="409" href="Algebras.Signatures.html" class="Module">Algebras.Signatures</a> <a id="429" class="Keyword">where</a>

Expand All @@ -28,7 +28,7 @@ We define the signature of an algebraic structure in Agda like this.

<pre class="Agda">

<a id="Signature"></a><a id="626" href="Algebras.Signatures.html#626" class="Function">Signature</a> <a id="636" class="Symbol">:</a> <a id="638" class="Symbol">(</a><a id="639" href="Algebras.Signatures.html#639" class="Bound">𝓞</a> <a id="641" href="Algebras.Signatures.html#641" class="Bound">𝓥</a> <a id="643" class="Symbol">:</a> <a id="645" href="Universes.html#205" class="Postulate">Universe</a><a id="653" class="Symbol">)</a> <a id="655" class="Symbol">→</a> <a id="657" class="Symbol">(</a><a id="658" href="Algebras.Signatures.html#639" class="Bound">𝓞</a> <a id="660" href="Agda.Primitive.html#636" class="Primitive Operator">⊔</a> <a id="662" href="Algebras.Signatures.html#641" class="Bound">𝓥</a><a id="663" class="Symbol">)</a> <a id="665" href="Universes.html#181" class="Primitive Operator">⁺</a> <a id="667" href="Universes.html#403" class="Function Operator">̇</a>
<a id="Signature"></a><a id="626" href="Algebras.Signatures.html#626" class="Function">Signature</a> <a id="636" class="Symbol">:</a> <a id="638" class="Symbol">(</a><a id="639" href="Algebras.Signatures.html#639" class="Bound">𝓞</a> <a id="641" href="Algebras.Signatures.html#641" class="Bound">𝓥</a> <a id="643" class="Symbol">:</a> <a id="645" href="Agda.Primitive.html#597" class="Postulate">Universe</a><a id="653" class="Symbol">)</a> <a id="655" class="Symbol">→</a> <a id="657" class="Symbol">(</a><a id="658" href="Algebras.Signatures.html#639" class="Bound">𝓞</a> <a id="660" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="662" href="Algebras.Signatures.html#641" class="Bound">𝓥</a><a id="663" class="Symbol">)</a> <a id="665" href="Agda.Primitive.html#780" class="Primitive Operator">⁺</a> <a id="667" href="Universes.html#403" class="Function Operator">̇</a>
<a id="669" href="Algebras.Signatures.html#626" class="Function">Signature</a> <a id="679" href="Algebras.Signatures.html#679" class="Bound">𝓞</a> <a id="681" href="Algebras.Signatures.html#681" class="Bound">𝓥</a> <a id="683" class="Symbol">=</a> <a id="685" href="MGS-MLTT.html#3074" class="Function">Σ</a> <a id="687" href="Algebras.Signatures.html#687" class="Bound">F</a> <a id="689" href="MGS-MLTT.html#3074" class="Function">꞉</a> <a id="691" href="Algebras.Signatures.html#679" class="Bound">𝓞</a> <a id="693" href="Universes.html#403" class="Function Operator">̇</a> <a id="695" href="MGS-MLTT.html#3074" class="Function">,</a> <a id="697" class="Symbol">(</a><a id="698" href="Algebras.Signatures.html#687" class="Bound">F</a> <a id="700" class="Symbol">→</a> <a id="702" href="Algebras.Signatures.html#681" class="Bound">𝓥</a> <a id="704" href="Universes.html#403" class="Function Operator">̇</a><a id="705" class="Symbol">)</a>

</pre>
Expand All @@ -45,13 +45,13 @@ Here is how we could define the signature for monoids as a member of the type `S

<pre class="Agda">

<a id="1373" class="Keyword">data</a> <a id="monoid-op"></a><a id="1378" href="Algebras.Signatures.html#1378" class="Datatype">monoid-op</a> <a id="1388" class="Symbol">{</a><a id="1389" href="Algebras.Signatures.html#1389" class="Bound">𝓞</a> <a id="1391" class="Symbol">:</a> <a id="1393" href="Universes.html#205" class="Postulate">Universe</a><a id="1401" class="Symbol">}</a> <a id="1403" class="Symbol">:</a> <a id="1405" href="Algebras.Signatures.html#1389" class="Bound">𝓞</a> <a id="1407" href="Universes.html#403" class="Function Operator">̇</a> <a id="1409" class="Keyword">where</a>
<a id="1373" class="Keyword">data</a> <a id="monoid-op"></a><a id="1378" href="Algebras.Signatures.html#1378" class="Datatype">monoid-op</a> <a id="1388" class="Symbol">{</a><a id="1389" href="Algebras.Signatures.html#1389" class="Bound">𝓞</a> <a id="1391" class="Symbol">:</a> <a id="1393" href="Agda.Primitive.html#597" class="Postulate">Universe</a><a id="1401" class="Symbol">}</a> <a id="1403" class="Symbol">:</a> <a id="1405" href="Algebras.Signatures.html#1389" class="Bound">𝓞</a> <a id="1407" href="Universes.html#403" class="Function Operator">̇</a> <a id="1409" class="Keyword">where</a>
<a id="monoid-op.e"></a><a id="1416" href="Algebras.Signatures.html#1416" class="InductiveConstructor">e</a> <a id="1418" class="Symbol">:</a> <a id="1420" href="Algebras.Signatures.html#1378" class="Datatype">monoid-op</a><a id="1429" class="Symbol">;</a> <a id="monoid-op.·"></a><a id="1431" href="Algebras.Signatures.html#1431" class="InductiveConstructor">·</a> <a id="1433" class="Symbol">:</a> <a id="1435" href="Algebras.Signatures.html#1378" class="Datatype">monoid-op</a>

<a id="1446" class="Keyword">open</a> <a id="1451" class="Keyword">import</a> <a id="1458" href="MGS-MLTT.html" class="Module">MGS-MLTT</a> <a id="1467" class="Keyword">using</a> <a id="1473" class="Symbol">(</a><a id="1474" href="MGS-MLTT.html#712" class="Function">𝟘</a><a id="1475" class="Symbol">;</a> <a id="1477" href="MGS-MLTT.html#2482" class="Function">𝟚</a><a id="1478" class="Symbol">)</a>

<a id="monoid-sig"></a><a id="1481" href="Algebras.Signatures.html#1481" class="Function">monoid-sig</a> <a id="1492" class="Symbol">:</a> <a id="1494" href="Algebras.Signatures.html#626" class="Function">Signature</a> <a id="1504" href="Overture.Preliminaries.html#8157" class="Generalizable">𝓞</a> <a id="1506" href="Agda.Primitive.html#590" class="Primitive">𝓤₀</a>
<a id="1509" href="Algebras.Signatures.html#1481" class="Function">monoid-sig</a> <a id="1520" class="Symbol">=</a> <a id="1522" href="Algebras.Signatures.html#1378" class="Datatype">monoid-op</a> <a id="1532" href="MGS-MLTT.html#2929" class="InductiveConstructor Operator">,</a> <a id="1534" class="Symbol">λ</a> <a id="1536" class="Symbol">{</a> <a id="1538" href="Algebras.Signatures.html#1416" class="InductiveConstructor">e</a> <a id="1540" class="Symbol">→</a> <a id="1542" href="MGS-MLTT.html#712" class="Function">𝟘</a><a id="1543" class="Symbol">;</a> <a id="1545" href="Algebras.Signatures.html#1431" class="InductiveConstructor">·</a> <a id="1547" class="Symbol">→</a> <a id="1549" href="MGS-MLTT.html#2482" class="Function">𝟚</a> <a id="1551" class="Symbol">}</a>
<a id="monoid-sig"></a><a id="1481" href="Algebras.Signatures.html#1481" class="Function">monoid-sig</a> <a id="1492" class="Symbol">:</a> <a id="1494" href="Algebras.Signatures.html#626" class="Function">Signature</a> <a id="1504" href="Overture.Preliminaries.html#8157" class="Generalizable">𝓞</a> <a id="1506" href="Agda.Primitive.html#764" class="Primitive">𝓤₀</a>
<a id="1509" href="Algebras.Signatures.html#1481" class="Function">monoid-sig</a> <a id="1520" class="Symbol">=</a> <a id="1522" href="Algebras.Signatures.html#1378" class="Datatype">monoid-op</a> <a id="1532" href="Overture.Preliminaries.html#13136" class="InductiveConstructor Operator">,</a> <a id="1534" class="Symbol">λ</a> <a id="1536" class="Symbol">{</a> <a id="1538" href="Algebras.Signatures.html#1416" class="InductiveConstructor">e</a> <a id="1540" class="Symbol">→</a> <a id="1542" href="MGS-MLTT.html#712" class="Function">𝟘</a><a id="1543" class="Symbol">;</a> <a id="1545" href="Algebras.Signatures.html#1431" class="InductiveConstructor">·</a> <a id="1547" class="Symbol">→</a> <a id="1549" href="MGS-MLTT.html#2482" class="Function">𝟚</a> <a id="1551" class="Symbol">}</a>

</pre>

Expand Down
Loading

0 comments on commit e9ce43b

Please sign in to comment.