Skip to content

Commit fc175cf

Browse files
williamdemeowilliamdemeo
committed
complete transition to new Relations.Extensionality module
1 parent 29725af commit fc175cf

30 files changed

+95
-832
lines changed

‎UALib/Algebras/Signatures.lagda

+1-1
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ open import Universes using (𝓤₀)
1717

1818
module Algebras.Signatures where
1919

20-
open import Relations.RelExtensionality public
20+
open import Relations.Extensionality public
2121

2222
\end{code}
2323

‎UALib/Relations.lagda

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ open import Relations.Discrete
2020
open import Relations.Continuous
2121
open import Relations.Quotients
2222
open import Relations.Truncation
23-
open import Relations.RelExtensionality
23+
open import Relations.Extensionality
2424

2525
\end{code}
2626

‎UALib/Relations/Extensionality.lagda

+4-3
Original file line numberDiff line numberDiff line change
@@ -5,15 +5,15 @@ date : 2021-02-23
55
author: William DeMeo
66
---
77

8-
### <a id="extensionality">Extensionality</a>
8+
### <a id="relation-extensionality">Relation Extensionality</a>
99

10-
This section presents the [Relations.RelExtensionality][] module of the [Agda Universal Algebra Library][].
10+
This section presents the [Relations.Extensionality][] module of the [Agda Universal Algebra Library][].
1111

1212
\begin{code}
1313

1414
{-# OPTIONS --without-K --exact-split --safe #-}
1515

16-
module Relations.RelExtensionality where
16+
module Relations.Extensionality where
1717

1818
open import Relations.Truncation public
1919

@@ -126,3 +126,4 @@ While we're at it, we might as well take the abstraction one step further and de
126126
<span style="float:right;">[Algebras →](Algebras.html)</span>
127127

128128

129+
{% include UALib.Links.md %}

‎UALib/Relations/Truncation.lagda

+1-1
Original file line numberDiff line numberDiff line change
@@ -123,7 +123,7 @@ Embeddings are always monic, so we conclude that when a function's codomain is a
123123
<br>
124124

125125
[← Relations.Quotients](Relations.Quotients.html)
126-
<span style="float:right;">[Relations.RelExtensionality →](Relations.RelExtensionality.html)</span>
126+
<span style="float:right;">[Relations.Extensionality →](Relations.Extensionality.html)</span>
127127

128128

129129
{% include UALib.Links.md %}

‎UALib/UALib.lagda

+2-2
Original file line numberDiff line numberDiff line change
@@ -96,9 +96,9 @@ open import Varieties
9696
- [Relation and Quotient Types](Relations.html)
9797
- [Discrete Relations](Relations.Discrete.html)
9898
- [Continuous Relations](Relations.Continuous.html)
99-
- [Equivalence Relations and Quotients](Relations.Quotients.html)
99+
- [Quotients](Relations.Quotients.html)
100100
- [Truncation](Relations.Truncation.html)
101-
- [Relation Extensionality](Relations.RelExtensionality.html)
101+
- [Relation Extensionality](Relations.Extensionality.html)
102102

103103
- [Algebra Types](Algebras.html)
104104
- [Operations and Signatures](Algebras.Signatures.html)

‎UALib/generate-md

+1-1
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ NAMES="UALib
4040
Relations.Continuous
4141
Relations.Quotients
4242
Relations.Truncation
43-
Relations.RelExtensionality
43+
Relations.Extensionality
4444
Algebras
4545
Algebras.Signatures
4646
Algebras.Algebras

‎UALib/generate-tex

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ NAMES="UALib
1313
Relations/Continuous
1414
Relations/Quotients
1515
Relations/Truncation
16-
Relations/RelExtensionality
16+
Relations/Extensionality
1717
Algebras
1818
Algebras/Signatures
1919
Algebras/Algebras

‎UALib/html/Algebras.Algebras.md

+5-5
Large diffs are not rendered by default.

‎UALib/html/Algebras.Congruences.md

+2-2
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,9 @@ This section presents the [Algebras.Congruences][] module of the [Agda Universal
1212

1313
<a id="313" class="Symbol">{-#</a> <a id="317" class="Keyword">OPTIONS</a> <a id="325" class="Pragma">--without-K</a> <a id="337" class="Pragma">--exact-split</a> <a id="351" class="Pragma">--safe</a> <a id="358" class="Symbol">#-}</a>
1414

15-
<a id="363" class="Keyword">open</a> <a id="368" class="Keyword">import</a> <a id="375" href="Algebras.Signatures.html" class="Module">Algebras.Signatures</a> <a id="395" class="Keyword">using</a> <a id="401" class="Symbol">(</a><a id="402" href="Algebras.Signatures.html#629" class="Function">Signature</a><a id="411" class="Symbol">;</a> <a id="413" href="Overture.Preliminaries.html#8157" class="Generalizable">𝓞</a><a id="414" class="Symbol">;</a> <a id="416" href="Universes.html#262" class="Generalizable">𝓥</a><a id="417" class="Symbol">)</a>
15+
<a id="363" class="Keyword">open</a> <a id="368" class="Keyword">import</a> <a id="375" href="Algebras.Signatures.html" class="Module">Algebras.Signatures</a> <a id="395" class="Keyword">using</a> <a id="401" class="Symbol">(</a><a id="402" href="Algebras.Signatures.html#626" class="Function">Signature</a><a id="411" class="Symbol">;</a> <a id="413" href="Overture.Preliminaries.html#8157" class="Generalizable">𝓞</a><a id="414" class="Symbol">;</a> <a id="416" href="Universes.html#262" class="Generalizable">𝓥</a><a id="417" class="Symbol">)</a>
1616

17-
<a id="420" class="Keyword">module</a> <a id="427" href="Algebras.Congruences.html" class="Module">Algebras.Congruences</a> <a id="448" class="Symbol">{</a><a id="449" href="Algebras.Congruences.html#449" class="Bound">𝑆</a> <a id="451" class="Symbol">:</a> <a id="453" href="Algebras.Signatures.html#629" class="Function">Signature</a> <a id="463" href="Overture.Preliminaries.html#8157" class="Generalizable">𝓞</a> <a id="465" href="Universes.html#262" class="Generalizable">𝓥</a><a id="466" class="Symbol">}</a> <a id="468" class="Keyword">where</a>
17+
<a id="420" class="Keyword">module</a> <a id="427" href="Algebras.Congruences.html" class="Module">Algebras.Congruences</a> <a id="448" class="Symbol">{</a><a id="449" href="Algebras.Congruences.html#449" class="Bound">𝑆</a> <a id="451" class="Symbol">:</a> <a id="453" href="Algebras.Signatures.html#626" class="Function">Signature</a> <a id="463" href="Overture.Preliminaries.html#8157" class="Generalizable">𝓞</a> <a id="465" href="Universes.html#262" class="Generalizable">𝓥</a><a id="466" class="Symbol">}</a> <a id="468" class="Keyword">where</a>
1818

1919
<a id="475" class="Keyword">open</a> <a id="480" class="Keyword">import</a> <a id="487" href="Algebras.Products.html" class="Module">Algebras.Products</a> <a id="505" class="Symbol">{</a><a id="506" class="Argument">𝑆</a> <a id="508" class="Symbol">=</a> <a id="510" href="Algebras.Congruences.html#449" class="Bound">𝑆</a><a id="511" class="Symbol">}</a> <a id="513" class="Keyword">public</a>
2020

‎UALib/html/Algebras.Products.md

+2-2
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,9 @@ Notice that we begin this module by assuming a signature `𝑆 : Signature 𝓞
1818

1919
<a id="567" class="Symbol">{-#</a> <a id="571" class="Keyword">OPTIONS</a> <a id="579" class="Pragma">--without-K</a> <a id="591" class="Pragma">--exact-split</a> <a id="605" class="Pragma">--safe</a> <a id="612" class="Symbol">#-}</a>
2020

21-
<a id="617" class="Keyword">open</a> <a id="622" class="Keyword">import</a> <a id="629" href="Algebras.Signatures.html" class="Module">Algebras.Signatures</a> <a id="649" class="Keyword">using</a> <a id="655" class="Symbol">(</a><a id="656" href="Algebras.Signatures.html#629" class="Function">Signature</a><a id="665" class="Symbol">;</a> <a id="667" href="Overture.Preliminaries.html#8157" class="Generalizable">𝓞</a><a id="668" class="Symbol">;</a> <a id="670" href="Universes.html#262" class="Generalizable">𝓥</a><a id="671" class="Symbol">)</a>
21+
<a id="617" class="Keyword">open</a> <a id="622" class="Keyword">import</a> <a id="629" href="Algebras.Signatures.html" class="Module">Algebras.Signatures</a> <a id="649" class="Keyword">using</a> <a id="655" class="Symbol">(</a><a id="656" href="Algebras.Signatures.html#626" class="Function">Signature</a><a id="665" class="Symbol">;</a> <a id="667" href="Overture.Preliminaries.html#8157" class="Generalizable">𝓞</a><a id="668" class="Symbol">;</a> <a id="670" href="Universes.html#262" class="Generalizable">𝓥</a><a id="671" class="Symbol">)</a>
2222

23-
<a id="674" class="Keyword">module</a> <a id="681" href="Algebras.Products.html" class="Module">Algebras.Products</a> <a id="699" class="Symbol">{</a><a id="700" href="Algebras.Products.html#700" class="Bound">𝑆</a> <a id="702" class="Symbol">:</a> <a id="704" href="Algebras.Signatures.html#629" class="Function">Signature</a> <a id="714" href="Overture.Preliminaries.html#8157" class="Generalizable">𝓞</a> <a id="716" href="Universes.html#262" class="Generalizable">𝓥</a><a id="717" class="Symbol">}</a> <a id="719" class="Keyword">where</a>
23+
<a id="674" class="Keyword">module</a> <a id="681" href="Algebras.Products.html" class="Module">Algebras.Products</a> <a id="699" class="Symbol">{</a><a id="700" href="Algebras.Products.html#700" class="Bound">𝑆</a> <a id="702" class="Symbol">:</a> <a id="704" href="Algebras.Signatures.html#626" class="Function">Signature</a> <a id="714" href="Overture.Preliminaries.html#8157" class="Generalizable">𝓞</a> <a id="716" href="Universes.html#262" class="Generalizable">𝓥</a><a id="717" class="Symbol">}</a> <a id="719" class="Keyword">where</a>
2424

2525
<a id="726" class="Keyword">open</a> <a id="731" class="Keyword">import</a> <a id="738" href="Algebras.Algebras.html" class="Module">Algebras.Algebras</a> <a id="756" class="Keyword">hiding</a> <a id="763" class="Symbol">(</a><a id="764" href="Overture.Preliminaries.html#8157" class="Generalizable">𝓞</a><a id="765" class="Symbol">;</a> <a id="767" href="Universes.html#262" class="Generalizable">𝓥</a><a id="768" class="Symbol">)</a> <a id="770" class="Keyword">public</a>
2626

‎UALib/html/Algebras.Signatures.md

+9-9
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ This section presents the [Algebras.Signatures][] module of the [Agda Universal
1717

1818
<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>
1919

20-
<a id="436" class="Keyword">open</a> <a id="441" class="Keyword">import</a> <a id="448" href="Relations.RelExtensionality.html" class="Module">Relations.RelExtensionality</a> <a id="476" class="Keyword">public</a>
20+
<a id="436" class="Keyword">open</a> <a id="441" class="Keyword">import</a> <a id="448" href="Relations.Extensionality.html" class="Module">Relations.Extensionality</a> <a id="473" class="Keyword">public</a>
2121

2222
</pre>
2323

@@ -28,8 +28,8 @@ We define the signature of an algebraic structure in Agda like this.
2828

2929
<pre class="Agda">
3030

31-
<a id="Signature"></a><a id="629" href="Algebras.Signatures.html#629" class="Function">Signature</a> <a id="639" class="Symbol">:</a> <a id="641" class="Symbol">(</a><a id="642" href="Algebras.Signatures.html#642" class="Bound">𝓞</a> <a id="644" href="Algebras.Signatures.html#644" class="Bound">𝓥</a> <a id="646" class="Symbol">:</a> <a id="648" href="Universes.html#205" class="Postulate">Universe</a><a id="656" class="Symbol">)</a> <a id="658" class="Symbol">→</a> <a id="660" class="Symbol">(</a><a id="661" href="Algebras.Signatures.html#642" class="Bound">𝓞</a> <a id="663" href="Agda.Primitive.html#636" class="Primitive Operator">⊔</a> <a id="665" href="Algebras.Signatures.html#644" class="Bound">𝓥</a><a id="666" class="Symbol">)</a> <a id="668" href="Universes.html#181" class="Primitive Operator">⁺</a> <a id="670" href="Universes.html#403" class="Function Operator">̇</a>
32-
<a id="672" href="Algebras.Signatures.html#629" class="Function">Signature</a> <a id="682" href="Algebras.Signatures.html#682" class="Bound">𝓞</a> <a id="684" href="Algebras.Signatures.html#684" class="Bound">𝓥</a> <a id="686" class="Symbol">=</a> <a id="688" href="MGS-MLTT.html#3074" class="Function">Σ</a> <a id="690" href="Algebras.Signatures.html#690" class="Bound">F</a> <a id="692" href="MGS-MLTT.html#3074" class="Function">꞉</a> <a id="694" href="Algebras.Signatures.html#682" class="Bound">𝓞</a> <a id="696" href="Universes.html#403" class="Function Operator">̇</a> <a id="698" href="MGS-MLTT.html#3074" class="Function">,</a> <a id="700" class="Symbol">(</a><a id="701" href="Algebras.Signatures.html#690" class="Bound">F</a> <a id="703" class="Symbol">→</a> <a id="705" href="Algebras.Signatures.html#684" class="Bound">𝓥</a> <a id="707" href="Universes.html#403" class="Function Operator">̇</a><a id="708" class="Symbol">)</a>
31+
<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>
32+
<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>
3333

3434
</pre>
3535

@@ -45,14 +45,14 @@ Here is how we could define the signature for monoids as a member of the type `S
4545

4646
<pre class="Agda">
4747

48-
<a id="1376" class="Keyword">data</a> <a id="monoid-op"></a><a id="1381" href="Algebras.Signatures.html#1381" class="Datatype">monoid-op</a> <a id="1391" class="Symbol">{</a><a id="1392" href="Algebras.Signatures.html#1392" class="Bound">𝓞</a> <a id="1394" class="Symbol">:</a> <a id="1396" href="Universes.html#205" class="Postulate">Universe</a><a id="1404" class="Symbol">}</a> <a id="1406" class="Symbol">:</a> <a id="1408" href="Algebras.Signatures.html#1392" class="Bound">𝓞</a> <a id="1410" href="Universes.html#403" class="Function Operator">̇</a> <a id="1412" class="Keyword">where</a>
49-
<a id="monoid-op.e"></a><a id="1419" href="Algebras.Signatures.html#1419" class="InductiveConstructor">e</a> <a id="1421" class="Symbol">:</a> <a id="1423" href="Algebras.Signatures.html#1381" class="Datatype">monoid-op</a>
50-
<a id="monoid-op.·"></a><a id="1434" href="Algebras.Signatures.html#1434" class="InductiveConstructor">·</a> <a id="1436" class="Symbol">:</a> <a id="1438" href="Algebras.Signatures.html#1381" class="Datatype">monoid-op</a>
48+
<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>
49+
<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>
50+
<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>
5151

52-
<a id="1449" class="Keyword">open</a> <a id="1454" class="Keyword">import</a> <a id="1461" href="MGS-MLTT.html" class="Module">MGS-MLTT</a> <a id="1470" class="Keyword">using</a> <a id="1476" class="Symbol">(</a><a id="1477" href="MGS-MLTT.html#712" class="Function">𝟘</a><a id="1478" class="Symbol">;</a> <a id="1480" href="MGS-MLTT.html#2482" class="Function">𝟚</a><a id="1481" class="Symbol">)</a>
52+
<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>
5353

54-
<a id="monoid-sig"></a><a id="1484" href="Algebras.Signatures.html#1484" class="Function">monoid-sig</a> <a id="1495" class="Symbol">:</a> <a id="1497" href="Algebras.Signatures.html#629" class="Function">Signature</a> <a id="1507" href="Overture.Preliminaries.html#8157" class="Generalizable">𝓞</a> <a id="1509" href="Agda.Primitive.html#590" class="Primitive">𝓤₀</a>
55-
<a id="1512" href="Algebras.Signatures.html#1484" class="Function">monoid-sig</a> <a id="1523" class="Symbol">=</a> <a id="1525" href="Algebras.Signatures.html#1381" class="Datatype">monoid-op</a> <a id="1535" href="MGS-MLTT.html#2929" class="InductiveConstructor Operator">,</a> <a id="1537" class="Symbol">λ</a> <a id="1539" class="Symbol">{</a> <a id="1541" href="Algebras.Signatures.html#1419" class="InductiveConstructor">e</a> <a id="1543" class="Symbol">→</a> <a id="1545" href="MGS-MLTT.html#712" class="Function">𝟘</a><a id="1546" class="Symbol">;</a> <a id="1548" href="Algebras.Signatures.html#1434" class="InductiveConstructor">·</a> <a id="1550" class="Symbol">→</a> <a id="1552" href="MGS-MLTT.html#2482" class="Function">𝟚</a> <a id="1554" class="Symbol">}</a>
54+
<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>
55+
<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>
5656

5757
</pre>
5858

0 commit comments

Comments
 (0)