Write about equivalence relations

author: Ohad Kammar <ohad.kammar@ed.ac.uk> 2022-08-07 23:35:19 +0100
committer: Ohad Kammar <ohad.kammar@ed.ac.uk> 2022-08-07 23:35:19 +0100
commit: 85b191cd3134102c7205c1771806ee16f73b3a89 (patch)
tree: 9ca3e343244e8a1e5fc15f4874e220f4c852651a
parent: bc260cdfa7b309820594b7caf14f62be8343358e (diff)
6 files changed, 553 insertions, 8 deletions
diff --git a/doc/Makefile b/doc/Makefile
index ac7e6e3..c50a300 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -6,8 +6,8 @@ ttms:
 	pack build setoid-doc.ipkg
 
 %.html: .PHONY
-	pack run katla markdown --config ./setoid-doc-style.dhall sources/$*.md ./build/ttc/$*.ttm \
-  | pandoc -o $*.html
+	pack run katla markdown --config ./setoid-doc-style.dhall sources/$*.md ./build/ttc/$*.ttm > $*.md
+	pandoc $*.md -o $*.html
 
 install-deps:
 	pack install-deps setoid-doc.ipkg
diff --git a/doc/Tutorial.html b/doc/Tutorial.html
index ae77959..5336f7a 100644
--- a/doc/Tutorial.html
+++ b/doc/Tutorial.html
@@ -44,5 +44,44 @@
 <li><p>constructing types with an equality relation that’s better behaved than Idris’s built-in <code>Equal</code> type.</p></li>
 <li><p>types with an equality relation that carries additional information</p></li>
 </ul>
-<h2 id="basic-interface">Basic interface</h2>
-<p><code class="IdrisCode"> <br /> </code></p>
+<p>If you want to see the source-code behind this tutorial, check the <a href="sources/Tutorial.md">source-code</a> out.</p>
+<h2 id="equivalence-relations">Equivalence relations</h2>
+<p>A <em>relation</em> over a type <code>ty</code> in Idris is any two-argument type-valued function:</p>
+<pre><code>namespace Control.Relation
+  Rel : Type -&gt; Type
+  Rel ty = ty -&gt; ty -&gt; Type</code></pre>
+<p>This definition and its associated interfaces ship with idris’s standard library. Given a relation <code>rel : Rel ty</code> and <code>x,y : ty</code>, we can form <code>x `rel` y : Type</code>: the type of ways in which <code>x</code> and <code>y</code> can be related.</p>
+<p>For example, two lists <em>overlap</em> when they have a common element: <code class="IdrisCode"> <span class="IdrisKeyword">record</span> <span class="IdrisType">Overlap</span> <span class="IdrisKeyword">{0</span> <span class="IdrisBound">a</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Type</span><span class="IdrisKeyword">}</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">xs</span><span class="IdrisKeyword">,</span><span class="IdrisBound">ys</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">List</span> <span class="IdrisBound">a</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">where</span><br />   constructor <span class="IdrisData">Overlapping</span><br />   <span class="IdrisFunction">common</span> <span class="IdrisKeyword">:</span> <span class="IdrisBound">a</span><br />   <span class="IdrisFunction">lhsPos</span> <span class="IdrisKeyword">:</span> <span class="IdrisBound">common</span> <span class="IdrisType"><code>Elem</code></span> <span class="IdrisBound">xs</span><br />   <span class="IdrisFunction">rhsPos</span> <span class="IdrisKeyword">:</span> <span class="IdrisBound">common</span> <span class="IdrisType"><code>Elem</code></span> <span class="IdrisBound">ys</span><br /> <br /> </code> Lists can overlap in exactly one position: <code class="IdrisCode"> <span class="IdrisFunction">Ex1</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Overlap</span> <span class="IdrisData">[1,2,3]</span> <span class="IdrisData">[6,7,2,8]</span><br /> <span class="IdrisFunction">Ex1</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">Overlapping</span><br />   <span class="IdrisKeyword">{</span> <span class="IdrisBound">common</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">2</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">lhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">There</span> <span class="IdrisData">Here</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">rhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">There</span> <span class="IdrisKeyword">(</span><span class="IdrisData">There</span> <span class="IdrisData">Here</span><span class="IdrisKeyword">)</span><br />   <span class="IdrisKeyword">}</span><br /> </code> But they can overlap in several ways: <code class="IdrisCode"> <span class="IdrisFunction">Ex2a</span> <span class="IdrisKeyword">,</span><br /> <span class="IdrisFunction">Ex2b</span> <span class="IdrisKeyword">,</span><br /> <span class="IdrisFunction">Ex2c</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Overlap</span> <span class="IdrisData">[1,2,3]</span> <span class="IdrisData">[2,3,2]</span><br /> <span class="IdrisFunction">Ex2a</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">Overlapping</span><br />   <span class="IdrisKeyword">{</span> <span class="IdrisBound">common</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">3</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">lhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">There</span> <span class="IdrisKeyword">(</span><span class="IdrisData">There</span> <span class="IdrisData">Here</span><span class="IdrisKeyword">)</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">rhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">There</span> <span class="IdrisData">Here</span><br />   <span class="IdrisKeyword">}</span><br /> <span class="IdrisFunction">Ex2b</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">Overlapping</span><br />   <span class="IdrisKeyword">{</span> <span class="IdrisBound">common</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">2</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">lhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">There</span> <span class="IdrisData">Here</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">rhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">Here</span><br />   <span class="IdrisKeyword">}</span><br /> <span class="IdrisFunction">Ex2c</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">Overlapping</span><br />   <span class="IdrisKeyword">{</span> <span class="IdrisBound">common</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">2</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">lhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">There</span> <span class="IdrisData">Here</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">rhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">There</span> <span class="IdrisKeyword">(</span><span class="IdrisData">There</span> <span class="IdrisData">Here</span><span class="IdrisKeyword">)</span><br />   <span class="IdrisKeyword">}</span><br /> </code> We can think of a relation <code>rel : Rel ty</code> as the type of edges in a directed graph between vertices in <code>ty</code>:</p>
+<ul>
+<li><p>edges have a direction: the type <code>rel x y</code> is different to <code>rel y x</code></p></li>
+<li><p>multiple different edges between the same vertices <code>e1, e2 : rel x y</code></p></li>
+<li><p>self-loops between the same vertex are allowed <code>loop : rel x x</code>.</p></li>
+</ul>
+<p>An <em>equivalence relation</em> is a relation that’s:</p>
+<ul>
+<li><p><em>reflexive</em>: we guarantee a specific way in which every element is related to itself;</p></li>
+<li><p><em>symmetric</em>: we can reverse an edge between two edges; and</p></li>
+<li><p><em>transitive</em>: we can compose paths of related elements into a single edge.</p></li>
+</ul>
+<p><code class="IdrisCode"> <span class="IdrisKeyword">record</span> <span class="IdrisType">Equivalence</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">A</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Type</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">where</span><br />   constructor <span class="IdrisData">MkEquivalence</span><br />   <span class="IdrisKeyword">0</span> <span class="IdrisFunction">relation</span><span class="IdrisKeyword">:</span> <span class="IdrisFunction">Rel</span> <span class="IdrisBound">A</span><br />   <span class="IdrisFunction">reflexive</span> <span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span>       <span class="IdrisKeyword">:</span> <span class="IdrisBound">A</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">-&gt;</span> <span class="IdrisBound">relation</span> <span class="IdrisBound">x</span> <span class="IdrisBound">x</span><br />   <span class="IdrisFunction">symmetric</span> <span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span> <span class="IdrisBound">y</span>    <span class="IdrisKeyword">:</span> <span class="IdrisBound">A</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">-&gt;</span> <span class="IdrisBound">relation</span> <span class="IdrisBound">x</span> <span class="IdrisBound">y</span> <span class="IdrisKeyword">-&gt;</span> <span class="IdrisBound">relation</span> <span class="IdrisBound">y</span> <span class="IdrisBound">x</span><br />   <span class="IdrisFunction">transitive</span><span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span> <span class="IdrisBound">y</span><span class="IdrisKeyword">,</span> <span class="IdrisBound">z</span> <span class="IdrisKeyword">:</span> <span class="IdrisBound">A</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">-&gt;</span> <span class="IdrisBound">relation</span> <span class="IdrisBound">x</span> <span class="IdrisBound">y</span> <span class="IdrisKeyword">-&gt;</span> <span class="IdrisBound">relation</span> <span class="IdrisBound">y</span> <span class="IdrisBound">z</span><br />                             <span class="IdrisKeyword">-&gt;</span> <span class="IdrisBound">relation</span> <span class="IdrisBound">x</span> <span class="IdrisBound">z</span><br /> </code></p>
+<p>We equip the built-in relation <code>Equal</code> with the structure of an equivalence relation, using the constructor <code>Refl</code> and the stdlib functions <code>sym</code>, and <code>trans</code>: <code class="IdrisCode"> <span class="IdrisFunction">EqualityEquivalence</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Equivalence</span> <span class="IdrisBound">a</span><br /> <span class="IdrisFunction">EqualityEquivalence</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">MkEquivalence</span><br />   <span class="IdrisKeyword">{</span> <span class="IdrisBound">relation</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">(===)</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">reflexive</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisData">Refl</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">symmetric</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x_eq_y</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisFunction">sym</span> <span class="IdrisBound">x_eq_y</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">transitive</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">z</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x_eq_y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y_eq_z</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisFunction">trans</span> <span class="IdrisBound">x_eq_y</span> <span class="IdrisBound">y_eq_z</span><br />   <span class="IdrisKeyword">}</span><br /> </code></p>
+<p>We’ll use the following relation on pairs of natural numbers as a running example. We can represent an integer as the difference between a pair of natural numbers: <code class="IdrisCode"> <span class="IdrisKeyword">infix</span> <span class="IdrisKeyword">8</span> .-.<br /> <br /> <span class="IdrisKeyword">record</span> <span class="IdrisType">INT</span> <span class="IdrisKeyword">where</span><br />   constructor <span class="IdrisData">(.-.)</span><br />   <span class="IdrisFunction">pos</span><span class="IdrisKeyword">,</span> <span class="IdrisFunction">neg</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Nat</span><br /> <br /> <span class="IdrisKeyword">record</span> <span class="IdrisType">SameDiff</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span> <span class="IdrisBound">y</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">INT</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">where</span><br />   constructor <span class="IdrisData">Check</span><br />   <span class="IdrisFunction">same</span> <span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisFunction">.pos + </span><span class="IdrisBound">y</span><span class="IdrisFunction">.neg === </span><span class="IdrisBound">y</span><span class="IdrisFunction">.pos + </span><span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span><br /> </code> The <code>SameDiff x y</code> relation is equivalent to mathematical equation that states that the difference between the positive and negative parts is identical: <br /><span class="math display"><em>x</em><sub><em>p</em><em>o</em><em>s</em></sub> − <em>x</em><sub><em>n</em><em>e</em><em>g</em></sub> = <em>y</em><sub><em>p</em><em>o</em><em>s</em></sub> − <em>y</em><sub><em>n</em><em>e</em><em>g</em></sub></span><br /> But, unlike the last equation which requires us to define integers and subtraction, its equivalent <code>(.same)</code> is expressed using only addition, and so addition on <code>Nat</code> is enough.</p>
+<p>The relation <code>SameDiff</code> is an equivalence relation. The proofs are straightforward, and a good opportunity to practice Idris’s equational reasoning combinators from <code>Syntax.PreorderReasoning</code>: <code class="IdrisCode"> <span class="IdrisFunction">SameDiffEquivalence</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Equivalence</span> <span class="IdrisType">INT</span><br /> <span class="IdrisFunction">SameDiffEquivalence</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">MkEquivalence</span><br />   <span class="IdrisKeyword">{</span> <span class="IdrisBound">relation</span> <span class="IdrisKeyword">=</span> <span class="IdrisType">SameDiff</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">reflexive</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisData">Check</span> <span class="math inline">$&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;Calc&lt;/span&gt;&amp;nbsp;$</span><br />       <span class="IdrisData">|~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><br />       <span class="IdrisData">~~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span> <span class="IdrisData">…</span><span class="IdrisKeyword">(</span><span class="IdrisData">Refl</span><span class="IdrisKeyword">)</span><br /> </code> This equational proof represents the single-step equational proof:</p>
+<p>&quot;Calculate:</p>
+<ol type="1">
+<li><span class="math inline"><em>x</em><sub><em>p</em><em>o</em><em>s</em></sub> + <em>x</em><sub><em>n</em><em>e</em><em>g</em></sub></span></li>
+<li><span class="math inline"> = <em>x</em><sub><em>p</em><em>o</em><em>s</em></sub> + <em>x</em><sub><em>n</em><em>e</em><em>g</em></sub></span> (by reflexivity)&quot;</li>
+</ol>
+<p>The mnemonic behind the ASCII-art is that the first step in the proof starts with a logical-judgement symbol <span class="math inline">⊢</span>, each step continues with an equality sign <span class="math inline">=</span>, and justified by a thought bubble <code>(...)</code>.</p>
+<p><code class="IdrisCode">   <span class="IdrisKeyword">,</span> <span class="IdrisBound">symmetric</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x_eq_y</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisData">Check</span> <span class="math inline">$&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;Calc&lt;/span&gt;&amp;nbsp;$</span><br />       <span class="IdrisData">|~</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><br />       <span class="IdrisData">~~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.neg</span> <span class="IdrisFunction">..&lt;</span><span class="IdrisKeyword">(</span><span class="IdrisBound">x_eq_y</span><span class="IdrisFunction">.same</span><span class="IdrisKeyword">)</span><br /> </code> In this proof, we were given the proof <code>x_eq_y.same : x.pos + y.neg = y.pos + x.neg</code> and so we appealed to the symmetric equation. The mnemonic here is that the last bubble in the thought bubble <code>(...)</code> is replace with a left-pointing arrow, reversing the reasoning step. <code class="IdrisCode">   <span class="IdrisKeyword">,</span> <span class="IdrisBound">transitive</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">z</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x_eq_y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y_eq_z</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisData">Check</span> <span class="math inline">$&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;plusRightCancel&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;\_&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;\_&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;y&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.pos&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;$</span> <span class="IdrisFunction">Calc</span> <span class="math inline">$&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class=&quot;IdrisData&quot;&gt;|~&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;x&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;z&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.neg&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;y&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.pos&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class=&quot;IdrisData&quot;&gt;~~&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;x&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;(&lt;/span&gt;&lt;span class=&quot;IdrisBound&quot;&gt;y&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;z&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.neg&lt;/span&gt;&lt;span class=&quot;IdrisKeyword&quot;&gt;)&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisData&quot;&gt;...&lt;/span&gt;&lt;span class=&quot;IdrisKeyword&quot;&gt;(&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;solve&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisData&quot;&gt;3&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;Monoid.Commutative.Free.Free&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;{&lt;/span&gt;&lt;span class=&quot;IdrisBound&quot;&gt;a&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;=&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;Nat.Additive&lt;/span&gt;&lt;span class=&quot;IdrisKeyword&quot;&gt;}&lt;/span&gt;&amp;nbsp;$</span><br />                                      <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><br />                                   <span class="IdrisFunction">=-=</span> <span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">2</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">))</span><br />       <span class="IdrisData">~~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span> <span class="IdrisData">…</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">cong</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span><span class="IdrisKeyword">)</span> <span class="math inline">$&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;y\_eq\_z&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.same&lt;/span&gt;&lt;span class=&quot;IdrisKeyword&quot;&gt;)&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class=&quot;IdrisData&quot;&gt;~~&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;(&lt;/span&gt;&lt;span class=&quot;IdrisBound&quot;&gt;x&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;y&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.neg&lt;/span&gt;&lt;span class=&quot;IdrisKeyword&quot;&gt;)&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;z&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisData&quot;&gt;...&lt;/span&gt;&lt;span class=&quot;IdrisKeyword&quot;&gt;(&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;solve&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisData&quot;&gt;3&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;Monoid.Commutative.Free.Free&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;{&lt;/span&gt;&lt;span class=&quot;IdrisBound&quot;&gt;a&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;=&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;Nat.Additive&lt;/span&gt;&lt;span class=&quot;IdrisKeyword&quot;&gt;}&lt;/span&gt;&amp;nbsp;$</span><br />                                      <span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">1</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><span class="IdrisKeyword">)</span><br />                                  <span class="IdrisFunction">=-=</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span><br />       <span class="IdrisData">~~</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span> <span class="IdrisData">…</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">cong</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">+</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span><span class="IdrisKeyword">)</span> ?h2<span class="IdrisKeyword">)</span><br />       <span class="IdrisData">~~</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span>   <span class="IdrisData">…</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">solve</span> <span class="IdrisData">3</span> <span class="IdrisFunction">Monoid.Commutative.Free.Free</span><br />                                      <span class="IdrisKeyword">{</span><span class="IdrisBound">a</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">Nat.Additive</span><span class="IdrisKeyword">}</span> $<br />                                      <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><br />                                  <span class="IdrisFunction">=-=</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">2</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">0</span><span class="IdrisKeyword">)</span><br />   <span class="IdrisKeyword">}</span><br /> </code> This proof is a lot more involved:</p>
+<ol type="1">
+<li>We appeal to the cancellation property of addition: <span class="math inline"><em>a</em> + <em>c</em> = <em>b</em> + <em>c</em> ⇒ <em>a</em> = <em>b</em></span></li>
+<li>We rearrange the term, bringing the appropriate part of <code>y</code> into contact with the appropriate part of <code>z</code> and <code>x</code> to transform the term.</li>
+</ol>
+<p>Here we use the idris library <a href="http://www.github.com/frex-project/idris-frex"><code>Frex</code></a> that can perform such routine rearrangements for common algebraic structures. In this case, we use the commutative monoid simplifier from <code>Frex</code>. If you want to read more about <code>Frex</code>, check the <a href="https://www.denotational.co.uk/drafts/allais-brady-corbyn-kammar-yallop-frex-dependently-typed-algebraic-simplification.pdf">paper</a> out.</p>
+<p>Idris’s <code>Control.Relation</code> defines interfaces for properties like reflexivity and transitivity. While the setoid package doesn’t use them, we’ll use them in a few examples.</p>
+<p>The <code>Overlap</code> relation from Examples 1 and 2 is symmetric: <code class="IdrisCode"> Sy<span class="IdrisFunction">mmetric (</span>L<span class="IdrisBound">ist a) Overlap</span> <span class="IdrisKeyword">w</span>h<span class="IdrisData">ere</span><br />   sy<span class="IdrisKeyword">m</span>m<span class="IdrisBound">etric </span>x<span class="IdrisKeyword">s</span>_<span class="IdrisBound">overlaps_ys = </span><span class="IdrisFunction">Overlap</span>ping<br />     <span class="IdrisKeyword">{</span> <span class="IdrisBound">common</span> <span class="IdrisKeyword">=</span> <span class="IdrisBound">xs_overlaps_ys</span><span class="IdrisFunction">.common</span><br />     <span class="IdrisKeyword">,</span> <span class="IdrisBound">lhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisBound">xs_overlaps_ys</span><span class="IdrisFunction">.rhsPos</span><br />     <span class="IdrisKeyword">,</span> rhsPos = xs_overlaps_ys.lhsPos<br />     }<br /> </code> However, <code>Overlap</code> is neither reflexive nor transitive:</p>
+<ul>
+<li><p>The empty list doesn’t overlap with itself: <code class="IdrisCode"> <span class="IdrisFunction">Ex3</span> <span class="IdrisBound">: Not (Overlap [</span>]<span class="IdrisKeyword"> </span>[<span class="IdrisKeyword">])</span><br /> Ex<span class="IdrisKeyword">3</span> <span class="IdrisKeyword">nil_overla</span>ps_nil = case nil_overlaps_nil.lhsPos of<br />   _ impossible<br /> </code></p></li>
+<li><p>Two lists may overlap with a middle list, but on different elements. For example: <code class="IdrisCode"> Ex4 : <span class="IdrisType">(</span> <span class="IdrisType">Overlap</span> <span class="IdrisData">[1] [</span>1<span class="IdrisData">,2]</span><br />       <span class="IdrisType">,</span> <span class="IdrisFunction">Ove</span>r<span class="IdrisKeyword">l</span><span class="IdrisType">ap [1,2</span>]<span class="IdrisData"> [2</span>]<br /> <span class="IdrisFunction">   </span> <span class="IdrisKeyword"> </span> , Not (Overlap [1] [2]))<br /> Ex<span class="IdrisKeyword">4</span> <span class="IdrisData">=</span><br />   <span class="IdrisData">(</span> <span class="IdrisData">Overlapping</span> <span class="IdrisData">1</span> <span class="IdrisKeyword">H</span><span class="IdrisData">ere H</span>e<span class="IdrisData">re</span><br />   <span class="IdrisData">,</span> <span class="IdrisKeyword">O</span>v<span class="IdrisBound">erlapping 2 (The</span>r<span class="IdrisKeyword">e </span>H<span class="IdrisKeyword">ere)</span> <span class="IdrisBound">Here</span><br />   , &lt;span class=“IdrisData”&gt; one_</span>o<span class="IdrisKeyword">v</span>e<span class="IdrisKeyword">rlaps_two </span>=&gt; case one_overlaps_two.lhsPos of<br />   <span class="IdrisKeyword"> </span>  There _ impossible<br />   )<br /> </code> The outer lists agree on <code>1</code> and <code>2</code>, respectively, but they can’t overlap on on the first element of either, which exhausts all possibilities of overlap.</p></li>
+</ul>
diff --git a/doc/Tutorial.md b/doc/Tutorial.md
new file mode 100644
index 0000000..c0d0896
--- /dev/null
+++ b/doc/Tutorial.md
@@ -0,0 +1,270 @@
+<style>
+.IdrisData {
+  color: darkred
+}
+.IdrisType {
+  color: blue
+}
+.IdrisBound {
+  color: black
+}
+.IdrisFunction {
+  color: darkgreen
+}
+.IdrisKeyword {
+  font-weight: bold;
+}
+.IdrisComment {
+  color: #b22222
+}
+.IdrisNamespace {
+  font-style: italic;
+  color: black
+}
+.IdrisPostulate {
+  font-weight: bold;
+  color: red
+}
+.IdrisModule {
+  font-style: italic;
+  color: black
+}
+.IdrisCode {
+  display: block;
+  background-color: whitesmoke;
+}
+</style>
+
+# Tutorial: Setoids
+
+A _setoid_ is a type equipped with an equivalence relation. Setoids come up when
+you need types with a better behaved equality relation, or when you want the
+equality relation to carry additional information. After completing this
+tutorial you will:
+
+1. Know the user interface to the `setoid` package.
+2. Know two different applications in which it can be used:
+  + constructing types with an equality relation that's better behaved than
+    Idris's built-in `Equal` type.
+
+  + types with an equality relation that carries additional information
+
+If you want to see the source-code behind this tutorial, check the
+[source-code](sources/Tutorial.md) out.
+
+## Equivalence relations
+
+A _relation_ over a type `ty` in Idris is any two-argument type-valued function:
+```
+namespace Control.Relation
+  Rel : Type -> Type
+  Rel ty = ty -> ty -> Type
+```
+This definition and its associated interfaces ship with idris's standard
+library. Given a relation `rel : Rel ty` and `x,y : ty`, we can form
+```x `rel` y : Type```: the type of ways in which `x` and `y` can be related.
+
+For example, two lists _overlap_ when they have a common element:
+<code class="IdrisCode">
+<span class="IdrisKeyword">record</span>&nbsp;<span class="IdrisType">Overlap</span>&nbsp;<span class="IdrisKeyword">{0</span>&nbsp;<span class="IdrisBound">a</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisType">Type</span><span class="IdrisKeyword">}</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">xs</span><span class="IdrisKeyword">,</span><span class="IdrisBound">ys</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisType">List</span>&nbsp;<span class="IdrisBound">a</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisKeyword">where</span><br />
+&nbsp;&nbsp;constructor&nbsp;<span class="IdrisData">Overlapping</span><br />
+&nbsp;&nbsp;<span class="IdrisFunction">common</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisBound">a</span><br />
+&nbsp;&nbsp;<span class="IdrisFunction">lhsPos</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisBound">common</span>&nbsp;<span class="IdrisType">`Elem`</span>&nbsp;<span class="IdrisBound">xs</span><br />
+&nbsp;&nbsp;<span class="IdrisFunction">rhsPos</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisBound">common</span>&nbsp;<span class="IdrisType">`Elem`</span>&nbsp;<span class="IdrisBound">ys</span><br />
+<br />
+</code>
+Lists can overlap in exactly one position:
+<code class="IdrisCode">
+<span class="IdrisFunction">Ex1</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisType">Overlap</span>&nbsp;<span class="IdrisData">[1,2,3]</span>&nbsp;<span class="IdrisData">[6,7,2,8]</span><br />
+<span class="IdrisFunction">Ex1</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">Overlapping</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">{</span>&nbsp;<span class="IdrisBound">common</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">2</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">lhsPos</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">There</span>&nbsp;<span class="IdrisData">Here</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">rhsPos</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">There</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisData">There</span>&nbsp;<span class="IdrisData">Here</span><span class="IdrisKeyword">)</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">}</span><br />
+</code>
+But they can overlap in several ways:
+<code class="IdrisCode">
+<span class="IdrisFunction">Ex2a</span>&nbsp;<span class="IdrisKeyword">,</span><br />
+<span class="IdrisFunction">Ex2b</span>&nbsp;<span class="IdrisKeyword">,</span><br />
+<span class="IdrisFunction">Ex2c</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisType">Overlap</span>&nbsp;<span class="IdrisData">[1,2,3]</span>&nbsp;<span class="IdrisData">[2,3,2]</span><br />
+<span class="IdrisFunction">Ex2a</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">Overlapping</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">{</span>&nbsp;<span class="IdrisBound">common</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">3</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">lhsPos</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">There</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisData">There</span>&nbsp;<span class="IdrisData">Here</span><span class="IdrisKeyword">)</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">rhsPos</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">There</span>&nbsp;<span class="IdrisData">Here</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">}</span><br />
+<span class="IdrisFunction">Ex2b</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">Overlapping</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">{</span>&nbsp;<span class="IdrisBound">common</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">2</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">lhsPos</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">There</span>&nbsp;<span class="IdrisData">Here</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">rhsPos</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">Here</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">}</span><br />
+<span class="IdrisFunction">Ex2c</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">Overlapping</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">{</span>&nbsp;<span class="IdrisBound">common</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">2</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">lhsPos</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">There</span>&nbsp;<span class="IdrisData">Here</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">rhsPos</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">There</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisData">There</span>&nbsp;<span class="IdrisData">Here</span><span class="IdrisKeyword">)</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">}</span><br />
+</code>
+We can think of a relation `rel : Rel ty` as the type of edges in a directed
+graph between vertices in `ty`:
+
+* edges have a direction: the type `rel x y` is different to `rel y x`
+
+* multiple different edges between the same vertices `e1, e2 : rel x y`
+
+* self-loops between the same vertex are allowed `loop : rel x x`.
+
+An _equivalence relation_ is a relation that's:
+
+*  _reflexive_: we guarantee a specific way in which every element is related to
+  itself;
+
+* _symmetric_: we can reverse an edge between two edges; and
+
+* _transitive_: we can compose paths of related elements into a single edge.
+
+<code class="IdrisCode">
+<span class="IdrisKeyword">record</span>&nbsp;<span class="IdrisType">Equivalence</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">A</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisType">Type</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisKeyword">where</span><br />
+&nbsp;&nbsp;constructor&nbsp;<span class="IdrisData">MkEquivalence</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">0</span>&nbsp;<span class="IdrisFunction">relation</span><span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisFunction">Rel</span>&nbsp;<span class="IdrisBound">A</span><br />
+&nbsp;&nbsp;<span class="IdrisFunction">reflexive</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">x</span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisBound">A</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisKeyword">-&gt;</span>&nbsp;<span class="IdrisBound">relation</span>&nbsp;<span class="IdrisBound">x</span>&nbsp;<span class="IdrisBound">x</span><br />
+&nbsp;&nbsp;<span class="IdrisFunction">symmetric</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">y</span>&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisBound">A</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisKeyword">-&gt;</span>&nbsp;<span class="IdrisBound">relation</span>&nbsp;<span class="IdrisBound">x</span>&nbsp;<span class="IdrisBound">y</span>&nbsp;<span class="IdrisKeyword">-&gt;</span>&nbsp;<span class="IdrisBound">relation</span>&nbsp;<span class="IdrisBound">y</span>&nbsp;<span class="IdrisBound">x</span><br />
+&nbsp;&nbsp;<span class="IdrisFunction">transitive</span><span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">y</span><span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">z</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisBound">A</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisKeyword">-&gt;</span>&nbsp;<span class="IdrisBound">relation</span>&nbsp;<span class="IdrisBound">x</span>&nbsp;<span class="IdrisBound">y</span>&nbsp;<span class="IdrisKeyword">-&gt;</span>&nbsp;<span class="IdrisBound">relation</span>&nbsp;<span class="IdrisBound">y</span>&nbsp;<span class="IdrisBound">z</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">-&gt;</span>&nbsp;<span class="IdrisBound">relation</span>&nbsp;<span class="IdrisBound">x</span>&nbsp;<span class="IdrisBound">z</span><br />
+</code>
+
+We equip the built-in relation `Equal` with the structure of an equivalence
+relation, using the constructor `Refl` and the stdlib functions `sym`, and
+`trans`:
+<code class="IdrisCode">
+<span class="IdrisFunction">EqualityEquivalence</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisType">Equivalence</span>&nbsp;<span class="IdrisBound">a</span><br />
+<span class="IdrisFunction">EqualityEquivalence</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">MkEquivalence</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">{</span>&nbsp;<span class="IdrisBound">relation</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisFunction">(===)</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">reflexive</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisKeyword">\</span><span class="IdrisBound">x</span>&nbsp;<span class="IdrisKeyword">=&gt;</span>&nbsp;<span class="IdrisData">Refl</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">symmetric</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisKeyword">\</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x\_eq\_y</span>&nbsp;<span class="IdrisKeyword">=&gt;</span>&nbsp;<span class="IdrisFunction">sym</span>&nbsp;<span class="IdrisBound">x\_eq\_y</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">transitive</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisKeyword">\</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">z</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x\_eq\_y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y\_eq\_z</span>&nbsp;<span class="IdrisKeyword">=&gt;</span>&nbsp;<span class="IdrisFunction">trans</span>&nbsp;<span class="IdrisBound">x\_eq\_y</span>&nbsp;<span class="IdrisBound">y\_eq\_z</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">}</span><br />
+</code>
+
+We'll use the following relation on pairs of natural numbers as a running
+example. We can represent an integer as the difference between a pair of natural
+numbers:
+<code class="IdrisCode">
+<span class="IdrisKeyword">infix</span>&nbsp;<span class="IdrisKeyword">8</span>&nbsp;.-.<br />
+<br />
+<span class="IdrisKeyword">record</span>&nbsp;<span class="IdrisType">INT</span>&nbsp;<span class="IdrisKeyword">where</span><br />
+&nbsp;&nbsp;constructor&nbsp;<span class="IdrisData">(.-.)</span><br />
+&nbsp;&nbsp;<span class="IdrisFunction">pos</span><span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisFunction">neg</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisType">Nat</span><br />
+<br />
+<span class="IdrisKeyword">record</span>&nbsp;<span class="IdrisType">SameDiff</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">y</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisType">INT</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisKeyword">where</span><br />
+&nbsp;&nbsp;constructor&nbsp;<span class="IdrisData">Check</span><br />
+&nbsp;&nbsp;<span class="IdrisFunction">same</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisFunction">.pos&nbsp;+&nbsp;</span><span class="IdrisBound">y</span><span class="IdrisFunction">.neg&nbsp;===&nbsp;</span><span class="IdrisBound">y</span><span class="IdrisFunction">.pos&nbsp;+&nbsp;</span><span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span><br />
+</code>
+The `SameDiff x y` relation is equivalent to mathematical equation that states
+that the difference between the positive and negative parts is identical:
+$$x_{pos} - x_{neg} = y_{pos} - y_{neg}$$
+But, unlike the last equation which requires us to define integers and
+subtraction, its equivalent `(.same)` is expressed using only addition, and
+so addition on `Nat` is enough.
+
+The relation `SameDiff` is an equivalence relation. The proofs are
+straightforward, and a good opportunity to practice Idris's equational
+reasoning combinators from `Syntax.PreorderReasoning`:
+<code class="IdrisCode">
+<span class="IdrisFunction">SameDiffEquivalence</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisType">Equivalence</span>&nbsp;<span class="IdrisType">INT</span><br />
+<span class="IdrisFunction">SameDiffEquivalence</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">MkEquivalence</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">{</span>&nbsp;<span class="IdrisBound">relation</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisType">SameDiff</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">reflexive</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisKeyword">\</span><span class="IdrisBound">x</span>&nbsp;<span class="IdrisKeyword">=&gt;</span>&nbsp;<span class="IdrisData">Check</span>&nbsp;$&nbsp;<span class="IdrisFunction">Calc</span>&nbsp;$<br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">|~</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">~~</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span>&nbsp;<span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisData">Refl</span><span class="IdrisKeyword">)</span><br />
+</code>
+This equational proof represents the single-step equational proof:
+
+"Calculate:
+
+1.   $x_{pos} + x_{neg}$
+2. $= x_{pos} + x_{neg}$ (by reflexivity)"
+
+The mnemonic behind the ASCII-art is that the first step in the proof
+starts with a logical-judgement symbol $\vdash$, each step continues with an
+equality sign $=$, and justified by a thought bubble `(...)`.
+
+<code class="IdrisCode">
+&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">symmetric</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisKeyword">\</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x\_eq\_y</span>&nbsp;<span class="IdrisKeyword">=&gt;</span>&nbsp;<span class="IdrisData">Check</span>&nbsp;$&nbsp;<span class="IdrisFunction">Calc</span>&nbsp;$<br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">|~</span>&nbsp;<span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">~~</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">y</span><span class="IdrisFunction">.neg</span>&nbsp;<span class="IdrisFunction">..&lt;</span><span class="IdrisKeyword">(</span><span class="IdrisBound">x\_eq\_y</span><span class="IdrisFunction">.same</span><span class="IdrisKeyword">)</span><br />
+</code>
+  In this proof, we were given the proof `x_eq_y.same : x.pos + y.neg = y.pos + x.neg`
+  and so we appealed to the symmetric equation. The mnemonic here is that the
+  last bubble in the thought bubble `(...)` is replace with a left-pointing arrow,
+  reversing the reasoning step.
+<code class="IdrisCode">
+&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">transitive</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisKeyword">\</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">z</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x\_eq\_y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y\_eq\_z</span>&nbsp;<span class="IdrisKeyword">=&gt;</span>&nbsp;<span class="IdrisData">Check</span>&nbsp;$&nbsp;<span class="IdrisFunction">plusRightCancel</span>&nbsp;<span class="IdrisKeyword">\_</span>&nbsp;<span class="IdrisKeyword">\_</span>&nbsp;<span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$&nbsp;<span class="IdrisFunction">Calc</span>&nbsp;$<br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">|~</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">z</span><span class="IdrisFunction">.neg</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">~~</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">z</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">solve</span>&nbsp;<span class="IdrisData">3</span>&nbsp;<span class="IdrisFunction">Monoid.Commutative.Free.Free</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">{</span><span class="IdrisBound">a</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisFunction">Nat.Additive</span><span class="IdrisKeyword">}</span>&nbsp;$<br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">0</span>&nbsp;<span class="IdrisFunction">.+.</span>&nbsp;<span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">1</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisFunction">.+.</span>&nbsp;<span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">2</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisFunction">=-=</span>&nbsp;<span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">0</span>&nbsp;<span class="IdrisFunction">.+.</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">2</span>&nbsp;<span class="IdrisFunction">.+.</span>&nbsp;<span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">1</span><span class="IdrisKeyword">))</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">~~</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">y</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">cong</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span><span class="IdrisKeyword">)</span>&nbsp;$&nbsp;<span class="IdrisBound">y\_eq\_z</span><span class="IdrisFunction">.same</span><span class="IdrisKeyword">)</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">~~</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">y</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">solve</span>&nbsp;<span class="IdrisData">3</span>&nbsp;<span class="IdrisFunction">Monoid.Commutative.Free.Free</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">{</span><span class="IdrisBound">a</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisFunction">Nat.Additive</span><span class="IdrisKeyword">}</span>&nbsp;$<br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">0</span>&nbsp;<span class="IdrisFunction">.+.</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">1</span>&nbsp;<span class="IdrisFunction">.+.</span>&nbsp;<span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">2</span><span class="IdrisKeyword">)</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisFunction">=-=</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">0</span>&nbsp;<span class="IdrisFunction">.+.</span>&nbsp;<span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">2</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisFunction">.+.</span>&nbsp;<span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">1</span><span class="IdrisKeyword">)</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">~~</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">cong</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span><span class="IdrisKeyword">)</span>&nbsp;?h2<span class="IdrisKeyword">)</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">~~</span>&nbsp;<span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span>&nbsp;&nbsp;&nbsp;<span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">solve</span>&nbsp;<span class="IdrisData">3</span>&nbsp;<span class="IdrisFunction">Monoid.Commutative.Free.Free</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">{</span><span class="IdrisBound">a</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisFunction">Nat.Additive</span><span class="IdrisKeyword">}</span>&nbsp;$<br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">0</span>&nbsp;<span class="IdrisFunction">.+.</span>&nbsp;<span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">1</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisFunction">.+.</span>&nbsp;<span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">2</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisFunction">=-=</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">2</span>&nbsp;<span class="IdrisFunction">.+.</span>&nbsp;<span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">1</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisFunction">.+.</span>&nbsp;<span class="IdrisFunction">X</span>&nbsp;<span class="IdrisData">0</span><span class="IdrisKeyword">)</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">}</span><br />
+</code>
+This proof is a lot more involved:
+
+1. We appeal to the cancellation property of addition:
+  $a + c = b + c \Rightarrow a = b$
+2. We rearrange the term, bringing the appropriate part of `y` into contact with
+  the appropriate part of `z` and `x` to transform the term.
+
+Here we use the idris library [`Frex`](http://www.github.com/frex-project/idris-frex)
+that can perform such routine
+rearrangements for common algebraic structures. In this case, we use the
+commutative monoid simplifier from `Frex`.
+If you want to read more about `Frex`, check the
+[paper](https://www.denotational.co.uk/drafts/allais-brady-corbyn-kammar-yallop-frex-dependently-typed-algebraic-simplification.pdf) out.
+
+
+Idris's `Control.Relation` defines interfaces for properties like reflexivity
+and transitivity. While the
+setoid package doesn't use them, we'll use them in a few examples.
+
+The `Overlap` relation from Examples 1 and 2 is symmetric:
+<code class="IdrisCode">
+Sy<span class="IdrisFunction">mmetric&nbsp;(</span>L<span class="IdrisBound">ist&nbsp;a)&nbsp;Overlap</span>&nbsp;<span class="IdrisKeyword">w</span>h<span class="IdrisData">ere</span><br />
+&nbsp;&nbsp;sy<span class="IdrisKeyword">m</span>m<span class="IdrisBound">etric&nbsp;</span>x<span class="IdrisKeyword">s</span>\_<span class="IdrisBound">overlaps\_ys&nbsp;=&nbsp;</span><span class="IdrisFunction">Overlap</span>ping<br />
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">{</span>&nbsp;<span class="IdrisBound">common</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisBound">xs\_overlaps\_ys</span><span class="IdrisFunction">.common</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">lhsPos</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisBound">xs\_overlaps\_ys</span><span class="IdrisFunction">.rhsPos</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;rhsPos&nbsp;=&nbsp;xs\_overlaps\_ys.lhsPos<br />
+&nbsp;&nbsp;&nbsp;&nbsp;}<br />
+</code>
+However, `Overlap` is neither reflexive nor transitive:
+
+* The empty list doesn't overlap with itself:
+<code class="IdrisCode">
+<span class="IdrisFunction">Ex3</span>&nbsp;<span class="IdrisBound">:&nbsp;Not&nbsp;(Overlap&nbsp;[</span>]<span class="IdrisKeyword">&nbsp;</span>[<span class="IdrisKeyword">])</span><br />
+Ex<span class="IdrisKeyword">3</span>&nbsp;<span class="IdrisKeyword">nil\_overla</span>ps\_nil&nbsp;=&nbsp;case&nbsp;nil\_overlaps\_nil.lhsPos&nbsp;of<br />
+&nbsp;&nbsp;\_&nbsp;impossible<br />
+</code>
+
+* Two lists may overlap with a middle list, but on different elements. For example:
+<code class="IdrisCode">
+Ex4&nbsp;:&nbsp;<span class="IdrisType">(</span>&nbsp;<span class="IdrisType">Overlap</span>&nbsp;<span class="IdrisData">[1]&nbsp;[</span>1<span class="IdrisData">,2]</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisType">,</span>&nbsp;<span class="IdrisFunction">Ove</span>r<span class="IdrisKeyword">l</span><span class="IdrisType">ap&nbsp;[1,2</span>]<span class="IdrisData">&nbsp;[2</span>]<br />
+<span class="IdrisFunction">&nbsp;&nbsp;&nbsp;</span>&nbsp;<span class="IdrisKeyword">&nbsp;</span>&nbsp;,&nbsp;Not&nbsp;(Overlap&nbsp;[1]&nbsp;[2]))<br />
+Ex<span class="IdrisKeyword">4</span>&nbsp;<span class="IdrisData">=</span><br />
+&nbsp;&nbsp;<span class="IdrisData">(</span>&nbsp;<span class="IdrisData">Overlapping</span>&nbsp;<span class="IdrisData">1</span>&nbsp;<span class="IdrisKeyword">H</span><span class="IdrisData">ere&nbsp;H</span>e<span class="IdrisData">re</span><br />
+&nbsp;&nbsp;<span class="IdrisData">,</span>&nbsp;<span class="IdrisKeyword">O</span>v<span class="IdrisBound">erlapping&nbsp;2&nbsp;(The</span>r<span class="IdrisKeyword">e&nbsp;</span>H<span class="IdrisKeyword">ere)</span>&nbsp;<span class="IdrisBound">Here</span><br />
+&nbsp;&nbsp;,&nbsp;\<span class="IdrisData">&nbsp;one\_</span>o<span class="IdrisKeyword">v</span>e<span class="IdrisKeyword">rlaps\_two&nbsp;</span>=&gt;&nbsp;case&nbsp;one\_overlaps\_two.lhsPos&nbsp;of<br />
+&nbsp;&nbsp;<span class="IdrisKeyword">&nbsp;</span>&nbsp;&nbsp;There&nbsp;\_&nbsp;impossible<br />
+&nbsp;&nbsp;)<br />
+</code>
+The outer lists agree on `1` and `2`, respectively, but they can't overlap on
+on the first element of either, which exhausts all possibilities of overlap.
+
diff --git a/doc/pack.toml b/doc/pack.toml
index d555f03..3aff702 100644
--- a/doc/pack.toml
+++ b/doc/pack.toml
@@ -1,4 +1,10 @@
-[doc.setoid]
+[custom.all.setoid]
 type = "local"
 path = ".."
 ipkg = "setoid.ipkg"
+
+[custom.all.frex]
+type = "github"
+url = "https://github.com/frex-project/idris-frex"
+commit = "latest:main"
+ipkg = "frex.ipkg"
diff --git a/doc/setoid-doc.ipkg b/doc/setoid-doc.ipkg
index 5d183fd..b97fb59 100644
--- a/doc/setoid-doc.ipkg
+++ b/doc/setoid-doc.ipkg
@@ -13,8 +13,10 @@ authors = "Ohad Kammar"
 -- langversion
 
 -- packages to add to search path
--- depends =
-
+depends
+  = contrib
+  , setoid
+  , frex
 modules
   = Tutorial
 
diff --git a/doc/sources/Tutorial.md b/doc/sources/Tutorial.md
index f143d45..85b09c8 100644
--- a/doc/sources/Tutorial.md
+++ b/doc/sources/Tutorial.md
@@ -1,5 +1,17 @@
 ```idris hide
 module Tutorial
+
+import Data.Setoid
+import Syntax.PreorderReasoning
+import Syntax.PreorderReasoning.Setoid
+import Data.List.Elem
+import Data.List
+import Data.Nat
+import Frex
+import Frexlet.Monoid.Commutative
+import Notation.Additive
+import Frexlet.Monoid.Notation.Additive
+import Frexlet.Monoid.Commutative.Nat
 ```
 # Tutorial: Setoids
 
@@ -15,7 +27,223 @@ tutorial you will:
 
   + types with an equality relation that carries additional information
 
-## Basic interface
+If you want to see the source-code behind this tutorial, check the
+[source-code](sources/Tutorial.md) out.
+
+## Equivalence relations
+
+A _relation_ over a type `ty` in Idris is any two-argument type-valued function:
+```
+namespace Control.Relation
+  Rel : Type -> Type
+  Rel ty = ty -> ty -> Type
+```
+This definition and its associated interfaces ship with idris's standard
+library. Given a relation `rel : Rel ty` and `x,y : ty`, we can form
+```x `rel` y : Type```: the type of ways in which `x` and `y` can be related.
+
+For example, two lists _overlap_ when they have a common element:
+```idris
+record Overlap {0 a : Type} (xs,ys : List a) where
+  constructor Overlapping
+  common : a
+  lhsPos : common `Elem` xs
+  rhsPos : common `Elem` ys
+
+```
+Lists can overlap in exactly one position:
+```idris
+Ex1 : Overlap [1,2,3] [6,7,2,8]
+Ex1 = Overlapping
+  { common = 2
+  , lhsPos = There Here
+  , rhsPos = There (There Here)
+  }
+```
+But they can overlap in several ways:
 ```idris
+Ex2a ,
+Ex2b ,
+Ex2c : Overlap [1,2,3] [2,3,2]
+Ex2a = Overlapping
+  { common = 3
+  , lhsPos = There (There Here)
+  , rhsPos = There Here
+  }
+Ex2b = Overlapping
+  { common = 2
+  , lhsPos = There Here
+  , rhsPos = Here
+  }
+Ex2c = Overlapping
+  { common = 2
+  , lhsPos = There Here
+  , rhsPos = There (There Here)
+  }
+```
+We can think of a relation `rel : Rel ty` as the type of edges in a directed
+graph between vertices in `ty`:
+
+* edges have a direction: the type `rel x y` is different to `rel y x`
+
+* multiple different edges between the same vertices `e1, e2 : rel x y`
 
+* self-loops between the same vertex are allowed `loop : rel x x`.
+
+An _equivalence relation_ is a relation that's:
+
+*  _reflexive_: we guarantee a specific way in which every element is related to
+  itself;
+
+* _symmetric_: we can reverse an edge between two edges; and
+
+* _transitive_: we can compose paths of related elements into a single edge.
+
+```idris
+record Equivalence (A : Type) where
+  constructor MkEquivalence
+  0 relation: Rel A
+  reflexive : (x       : A) -> relation x x
+  symmetric : (x, y    : A) -> relation x y -> relation y x
+  transitive: (x, y, z : A) -> relation x y -> relation y z
+                            -> relation x z
+```
+```idris hide
+%hide Tutorial.Equivalence
+```
+We equip the built-in relation `Equal` with the structure of an equivalence
+relation, using the constructor `Refl` and the stdlib functions `sym`, and
+`trans`:
+```idris
+EqualityEquivalence : Equivalence a
+EqualityEquivalence = MkEquivalence
+  { relation = (===)
+  , reflexive = \x => Refl
+  , symmetric = \x,y,x_eq_y => sym x_eq_y
+  , transitive = \x,y,z,x_eq_y,y_eq_z => trans x_eq_y y_eq_z
+  }
+```
+
+We'll use the following relation on pairs of natural numbers as a running
+example. We can represent an integer as the difference between a pair of natural
+numbers:
+```idris
+infix 8 .-.
+
+record INT where
+  constructor (.-.)
+  pos, neg : Nat
+
+record SameDiff (x, y : INT) where
+  constructor Check
+  same : (x.pos + y.neg === y.pos + x.neg)
+```
+The `SameDiff x y` relation is equivalent to mathematical equation that states
+that the difference between the positive and negative parts is identical:
+$$x_{pos} - x_{neg} = y_{pos} - y_{neg}$$
+But, unlike the last equation which requires us to define integers and
+subtraction, its equivalent `(.same)` is expressed using only addition, and
+so addition on `Nat` is enough.
+
+The relation `SameDiff` is an equivalence relation. The proofs are
+straightforward, and a good opportunity to practice Idris's equational
+reasoning combinators from `Syntax.PreorderReasoning`:
+```idris
+SameDiffEquivalence : Equivalence INT
+SameDiffEquivalence = MkEquivalence
+  { relation = SameDiff
+  , reflexive = \x => Check $ Calc $
+      |~ x.pos + x.neg
+      ~~ x.pos + x.neg ...(Refl)
+```
+This equational proof represents the single-step equational proof:
+
+"Calculate:
+
+1.   $x_{pos} + x_{neg}$
+2. $= x_{pos} + x_{neg}$ (by reflexivity)"
+
+The mnemonic behind the ASCII-art is that the first step in the proof
+starts with a logical-judgement symbol $\vdash$, each step continues with an
+equality sign $=$, and justified by a thought bubble `(...)`.
+
+```idris
+  , symmetric = \x,y,x_eq_y => Check $ Calc $
+      |~ y.pos + x.neg
+      ~~ x.pos + y.neg ..<(x_eq_y.same)
+```
+  In this proof, we were given the proof `x_eq_y.same : x.pos + y.neg = y.pos + x.neg`
+  and so we appealed to the symmetric equation. The mnemonic here is that the
+  last bubble in the thought bubble `(...)` is replace with a left-pointing arrow,
+  reversing the reasoning step.
+```idris
+  , transitive = \x,y,z,x_eq_y,y_eq_z => Check $ plusRightCancel _ _ y.pos
+      $ Calc $
+      |~ x.pos + z.neg + y.pos
+      ~~ x.pos + (y.pos + z.neg) ...(solve 3 Monoid.Commutative.Free.Free
+                                     {a = Nat.Additive} $
+                                     (X 0 .+. X 1) .+. X 2
+                                  =-= X 0 .+. (X 2 .+. X 1))
+      ~~ x.pos + (z.pos + y.neg) ...(cong (x.pos +) $ y_eq_z.same)
+      ~~ (x.pos + y.neg) + z.pos ...(solve 3 Monoid.Commutative.Free.Free
+                                     {a = Nat.Additive} $
+                                     X 0 .+. (X 1 .+. X 2)
+                                 =-= (X 0 .+. X 2) .+. X 1)
+      ~~ (y.pos + x.neg) + z.pos ...(cong (+ z.pos) ?h2)
+      ~~ z.pos + x.neg + y.pos   ...(solve 3 Monoid.Commutative.Free.Free
+                                     {a = Nat.Additive} $
+                                     (X 0 .+. X 1) .+. X 2
+                                 =-= (X 2 .+. X 1) .+. X 0)
+  }
+```
+This proof is a lot more involved:
+
+1. We appeal to the cancellation property of addition:
+  $a + c = b + c \Rightarrow a = b$
+2. We rearrange the term, bringing the appropriate part of `y` into contact with
+  the appropriate part of `z` and `x` to transform the term.
+
+Here we use the idris library [`Frex`](http://www.github.com/frex-project/idris-frex)
+that can perform such routine
+rearrangements for common algebraic structures. In this case, we use the
+commutative monoid simplifier from `Frex`.
+If you want to read more about `Frex`, check the
+[paper](https://www.denotational.co.uk/drafts/allais-brady-corbyn-kammar-yallop-frex-dependently-typed-algebraic-simplification.pdf) out.
+
+
+Idris's `Control.Relation` defines interfaces for properties like reflexivity
+and transitivity. While the
+setoid package doesn't use them, we'll use them in a few examples.
+
+The `Overlap` relation from Examples 1 and 2 is symmetric:
+```idris
+Symmetric (List a) Overlap where
+  symmetric xs_overlaps_ys = Overlapping
+    { common = xs_overlaps_ys.common
+    , lhsPos = xs_overlaps_ys.rhsPos
+    , rhsPos = xs_overlaps_ys.lhsPos
+    }
+```
+However, `Overlap` is neither reflexive nor transitive:
+
+* The empty list doesn't overlap with itself:
+```idris
+Ex3 : Not (Overlap [] [])
+Ex3 nil_overlaps_nil = case nil_overlaps_nil.lhsPos of
+  _ impossible
+```
+
+* Two lists may overlap with a middle list, but on different elements. For example:
+```idris
+Ex4 : ( Overlap [1] [1,2]
+      , Overlap [1,2] [2]
+      , Not (Overlap [1] [2]))
+Ex4 =
+  ( Overlapping 1 Here Here
+  , Overlapping 2 (There Here) Here
+  , \ one_overlaps_two => case one_overlaps_two.lhsPos of
+     There _ impossible
+  )
 ```
+The outer lists agree on `1` and `2`, respectively, but they can't overlap on
+on the first element of either, which exhausts all possibilities of overlap.
author	Ohad Kammar <ohad.kammar@ed.ac.uk>	2022-08-07 23:35:19 +0100
committer	Ohad Kammar <ohad.kammar@ed.ac.uk>	2022-08-07 23:35:19 +0100
commit	85b191cd3134102c7205c1771806ee16f73b3a89 (patch)
tree	9ca3e343244e8a1e5fc15f4874e220f4c852651a
parent	bc260cdfa7b309820594b7caf14f62be8343358e (diff)