Deploying to web from @ c2314e9 🚀

TSPL/2022/Assignment2/index.html

@@ -55,7 +55,7 @@
   <a id="TSPL.2022_Assignment2-5897" class="Keyword">open</a> <a id="TSPL.2022_Assignment2-5902" class="Keyword">import</a> <a id="TSPL.2022_Assignment2-5909" href="https://agda.github.io/agda-stdlib/v2.1/Data.Product.html" class="Module">Data.Product</a> <a id="TSPL.2022_Assignment2-5922" class="Keyword">using</a> <a id="TSPL.2022_Assignment2-5928" class="Symbol">(</a><a id="TSPL.2022_Assignment2-5929" href="https://agda.github.io/agda-stdlib/v2.1/Data.Product.Base.html#1618" class="Function Operator">_×_</a><a id="TSPL.2022_Assignment2-5932" class="Symbol">)</a>
   <a id="TSPL.2022_Assignment2-5936" class="Keyword">open</a> <a id="TSPL.2022_Assignment2-5941" class="Keyword">import</a> <a id="TSPL.2022_Assignment2-5948" href="../../../Isomorphism/#" class="Module">plfa.part1.Isomorphism</a> <a id="TSPL.2022_Assignment2-5971" class="Keyword">using</a> <a id="TSPL.2022_Assignment2-5977" class="Symbol">(</a><a id="TSPL.2022_Assignment2-5978" href="../../../Isomorphism/#plfa_plfa-part1-Isomorphism-4308" class="Record Operator">_≃_</a><a id="TSPL.2022_Assignment2-5981" class="Symbol">;</a> <a id="TSPL.2022_Assignment2-5983" href="../../../Isomorphism/#plfa_plfa-part1-Isomorphism-2625" class="Postulate">extensionality</a><a id="TSPL.2022_Assignment2-5997" class="Symbol">)</a>
 </pre><pre class="Agda">  <a id="TSPL.2022_Assignment2-6011" class="Keyword">open</a> <a id="TSPL.2022_Assignment2-6016" class="Keyword">import</a> <a id="TSPL.2022_Assignment2-6023" href="../../../Negation/#" class="Module">plfa.part1.Negation</a>
-    <a id="TSPL.2022_Assignment2-6047" class="Keyword">hiding</a> <a id="TSPL.2022_Assignment2-6054" class="Symbol">(</a><a id="TSPL.2022_Assignment2-6055" href="../../../Negation/#plfa_plfa-part1-Negation-13124" class="Function">Stable</a><a id="TSPL.2022_Assignment2-6061" class="Symbol">)</a>
+    <a id="TSPL.2022_Assignment2-6047" class="Keyword">hiding</a> <a id="TSPL.2022_Assignment2-6054" class="Symbol">(</a><a id="TSPL.2022_Assignment2-6055" href="../../../Negation/#plfa_plfa-part1-Negation-13120" class="Function">Stable</a><a id="TSPL.2022_Assignment2-6061" class="Symbol">)</a>
 </pre><h4 id="exercise--irreflexive-recommended">Exercise <code>&lt;-irreflexive</code> (recommended)</h4><p>Using negation, show that <a href="../../../Relations/#strict-inequality">strict inequality</a> is irreflexive, that is, <code>n &lt; n</code> holds for no <code>n</code>.</p><pre class="Agda">  <a id="TSPL.2022_Assignment2-6252" class="Comment">-- Your code goes here</a>
 </pre><h4 id="exercise-trichotomy-practice">Exercise <code>trichotomy</code> (practice)</h4><p>Show that strict inequality satisfies <a href="../../../Relations/#trichotomy">trichotomy</a>, that is, for any naturals <code>m</code> and <code>n</code> exactly one of the following holds:</p><ul><li><code>m &lt; n</code></li><li><code>m ≡ n</code></li><li><code>m &gt; n</code></li></ul><p>Here “exactly one” means that not only one of the three must hold, but that when one holds the negation of the other two must also hold.</p><pre class="Agda">  <a id="TSPL.2022_Assignment2-6650" class="Comment">-- Your code goes here</a>
 </pre><h4 id="exercise--dual--recommended">Exercise <code>⊎-dual-×</code> (recommended)</h4><p>Show that conjunction, disjunction, and negation are related by a version of De Morgan’s Law.</p><pre><code>¬ (A ⊎ B) ≃ (¬ A) × (¬ B)</code></pre><p>This result is an easy consequence of something we’ve proved previously.</p><pre class="Agda">  <a id="TSPL.2022_Assignment2-6928" class="Comment">-- Your code goes here</a>

TSPL/2023/Assignment2/index.html

@@ -25,7 +25,7 @@
   <a id="TSPL.2023_Assignment2-3174" class="Keyword">open</a> <a id="TSPL.2023_Assignment2-3179" class="Keyword">import</a> <a id="TSPL.2023_Assignment2-3186" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="TSPL.2023_Assignment2-3195" class="Keyword">using</a> <a id="TSPL.2023_Assignment2-3201" class="Symbol">(</a><a id="TSPL.2023_Assignment2-3202" href="https://agda.github.io/agda-stdlib/v2.1/Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a><a id="TSPL.2023_Assignment2-3203" class="Symbol">;</a> <a id="TSPL.2023_Assignment2-3205" href="https://agda.github.io/agda-stdlib/v2.1/Agda.Builtin.Nat.html#221" class="InductiveConstructor">zero</a><a id="TSPL.2023_Assignment2-3209" class="Symbol">;</a> <a id="TSPL.2023_Assignment2-3211" href="https://agda.github.io/agda-stdlib/v2.1/Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a><a id="TSPL.2023_Assignment2-3214" class="Symbol">)</a>
   <a id="TSPL.2023_Assignment2-3218" class="Keyword">open</a> <a id="TSPL.2023_Assignment2-3223" class="Keyword">import</a> <a id="TSPL.2023_Assignment2-3230" href="../../../Isomorphism/#" class="Module">plfa.part1.Isomorphism</a> <a id="TSPL.2023_Assignment2-3253" class="Keyword">using</a> <a id="TSPL.2023_Assignment2-3259" class="Symbol">(</a><a id="TSPL.2023_Assignment2-3260" href="../../../Isomorphism/#plfa_plfa-part1-Isomorphism-4308" class="Record Operator">_≃_</a><a id="TSPL.2023_Assignment2-3263" class="Symbol">;</a> <a id="TSPL.2023_Assignment2-3265" href="../../../Isomorphism/#plfa_plfa-part1-Isomorphism-2625" class="Postulate">extensionality</a><a id="TSPL.2023_Assignment2-3279" class="Symbol">)</a>
   <a id="TSPL.2023_Assignment2-3283" class="Keyword">open</a> <a id="TSPL.2023_Assignment2-3288" class="Keyword">import</a> <a id="TSPL.2023_Assignment2-3295" href="../../../Connectives/#" class="Module">plfa.part1.Connectives</a>
-  <a id="TSPL.2023_Assignment2-3320" class="Keyword">open</a> <a id="TSPL.2023_Assignment2-3325" class="Keyword">import</a> <a id="TSPL.2023_Assignment2-3332" href="../../../Negation/#" class="Module">plfa.part1.Negation</a> <a id="TSPL.2023_Assignment2-3352" class="Keyword">hiding</a> <a id="TSPL.2023_Assignment2-3359" class="Symbol">(</a><a id="TSPL.2023_Assignment2-3360" href="../../../Negation/#plfa_plfa-part1-Negation-13124" class="Function">Stable</a><a id="TSPL.2023_Assignment2-3366" class="Symbol">)</a>
+  <a id="TSPL.2023_Assignment2-3320" class="Keyword">open</a> <a id="TSPL.2023_Assignment2-3325" class="Keyword">import</a> <a id="TSPL.2023_Assignment2-3332" href="../../../Negation/#" class="Module">plfa.part1.Negation</a> <a id="TSPL.2023_Assignment2-3352" class="Keyword">hiding</a> <a id="TSPL.2023_Assignment2-3359" class="Symbol">(</a><a id="TSPL.2023_Assignment2-3360" href="../../../Negation/#plfa_plfa-part1-Negation-13120" class="Function">Stable</a><a id="TSPL.2023_Assignment2-3366" class="Symbol">)</a>
 </pre><h4 id="exercise--irreflexive-recommended">Exercise <code>&lt;-irreflexive</code> (recommended)</h4><p>Using negation, show that <a href="../../../Relations/#strict-inequality">strict inequality</a> is irreflexive, that is, <code>n &lt; n</code> holds for no <code>n</code>.</p><pre class="Agda">  <a id="TSPL.2023_Assignment2-3557" class="Comment">-- Your code goes here</a>
 </pre><h4 id="exercise-trichotomy-practice">Exercise <code>trichotomy</code> (practice)</h4><p>Show that strict inequality satisfies <a href="../../../Relations/#trichotomy">trichotomy</a>, that is, for any naturals <code>m</code> and <code>n</code> exactly one of the following holds:</p><ul><li><code>m &lt; n</code></li><li><code>m ≡ n</code></li><li><code>m &gt; n</code></li></ul><p>Here “exactly one” means that not only one of the three must hold, but that when one holds the negation of the other two must also hold.</p><pre class="Agda">  <a id="TSPL.2023_Assignment2-3955" class="Comment">-- Your code goes here</a>
 </pre><h4 id="exercise--dual--recommended">Exercise <code>⊎-dual-×</code> (recommended)</h4><p>Show that conjunction, disjunction, and negation are related by a version of De Morgan’s Law.</p><pre><code>¬ (A ⊎ B) ≃ (¬ A) × (¬ B)</code></pre><p>This result is an easy consequence of something we’ve proved previously.</p><pre class="Agda">  <a id="TSPL.2023_Assignment2-4233" class="Comment">-- Your code goes here</a>

TSPL/2024/Assignment2/index.html

@@ -26,7 +26,7 @@
   <a id="TSPL.2024_Assignment2-3516" class="Keyword">open</a> <a id="TSPL.2024_Assignment2-3521" class="Keyword">import</a> <a id="TSPL.2024_Assignment2-3528" href="../../../Isomorphism/#" class="Module">plfa.part1.Isomorphism</a> <a id="TSPL.2024_Assignment2-3551" class="Keyword">using</a> <a id="TSPL.2024_Assignment2-3557" class="Symbol">(</a><a id="TSPL.2024_Assignment2-3558" href="../../../Isomorphism/#plfa_plfa-part1-Isomorphism-4308" class="Record Operator">_≃_</a><a id="TSPL.2024_Assignment2-3561" class="Symbol">;</a> <a id="TSPL.2024_Assignment2-3563" href="../../../Isomorphism/#plfa_plfa-part1-Isomorphism-2625" class="Postulate">extensionality</a><a id="TSPL.2024_Assignment2-3577" class="Symbol">)</a>
   <a id="TSPL.2024_Assignment2-3581" class="Keyword">open</a> <a id="TSPL.2024_Assignment2-3586" class="Keyword">import</a> <a id="TSPL.2024_Assignment2-3593" href="../../../Connectives/#" class="Module">plfa.part1.Connectives</a>
   <a id="TSPL.2024_Assignment2-3618" class="Keyword">open</a> <a id="TSPL.2024_Assignment2-3623" class="Keyword">import</a> <a id="TSPL.2024_Assignment2-3630" href="../../../Negation/#" class="Module">plfa.part1.Negation</a>
-    <a id="TSPL.2024_Assignment2-3654" class="Keyword">hiding</a> <a id="TSPL.2024_Assignment2-3661" class="Symbol">(</a><a id="TSPL.2024_Assignment2-3662" href="../../../Negation/#plfa_plfa-part1-Negation-13124" class="Function">Stable</a><a id="TSPL.2024_Assignment2-3668" class="Symbol">)</a>
+    <a id="TSPL.2024_Assignment2-3654" class="Keyword">hiding</a> <a id="TSPL.2024_Assignment2-3661" class="Symbol">(</a><a id="TSPL.2024_Assignment2-3662" href="../../../Negation/#plfa_plfa-part1-Negation-13120" class="Function">Stable</a><a id="TSPL.2024_Assignment2-3668" class="Symbol">)</a>
 </pre><h4 id="exercise--irreflexive-recommended">Exercise <code>&lt;-irreflexive</code> (recommended)</h4><p>Using negation, show that <a href="../../../Relations/#strict-inequality">strict inequality</a> is irreflexive, that is, <code>n &lt; n</code> holds for no <code>n</code>.</p><pre class="Agda">  <a id="TSPL.2024_Assignment2-3859" class="Comment">-- Your code goes here</a>
 </pre><h4 id="exercise-trichotomy-practice">Exercise <code>trichotomy</code> (practice)</h4><p>Show that strict inequality satisfies <a href="../../../Relations/#trichotomy">trichotomy</a>, that is, for any naturals <code>m</code> and <code>n</code> exactly one of the following holds:</p><ul><li><code>m &lt; n</code></li><li><code>m ≡ n</code></li><li><code>m &gt; n</code></li></ul><p>Here “exactly one” means that not only one of the three must hold, but that when one holds the negation of the other two must also hold.</p><pre class="Agda">  <a id="TSPL.2024_Assignment2-4257" class="Comment">-- Your code goes here</a>
 </pre><h4 id="exercise--dual--recommended">Exercise <code>⊎-dual-×</code> (recommended)</h4><p>Show that conjunction, disjunction, and negation are related by a version of De Morgan’s Law.</p><pre><code>¬ (A ⊎ B) ≃ (¬ A) × (¬ B)</code></pre><p>This result is an easy consequence of something we’ve proved previously.</p><pre class="Agda">  <a id="TSPL.2024_Assignment2-4535" class="Comment">-- Your code goes here</a>