Merge branch 'dev' into fix/negation_¬¬¬-elim

plfa · Nov 5, 2024 · 4d16d0a · 4d16d0a
2 parents 89ed5ab + 4b60d3f
commit 4d16d0a
Show file tree

Hide file tree

Showing 6 changed files with 772 additions and 18 deletions.
diff --git a/courses/TSPL/2024/Assignment1.lagda.md b/courses/TSPL/2024/Assignment1.lagda.md
@@ -349,6 +349,8 @@ module Relations where
   open import Data.Nat.Properties
     using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
            +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
+
+  open import plfa.part1.Relations hiding (_≤_; z≤n; s≤s)
 ```
 
 

diff --git a/courses/TSPL/2024/Assignment2.lagda.md b/courses/TSPL/2024/Assignment2.lagda.md
@@ -252,10 +252,12 @@ module Quantifiers where
   open import Relation.Nullary using (¬_)
   open import Function using (_∘_)
   open import plfa.part1.Isomorphism using (_≃_; extensionality; ∀-extensionality)
-  open import plfa.part1.Connectives
-    hiding (Tri)
-  open import plfa.part1.Quantifiers
-    hiding (∀-distrib-×; ⊎∀-implies-∀⊎; ∃-distrib-⊎; ∃×-implies-×∃; ∃¬-implies-¬∀; Tri)
+  open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+  open import Data.Unit using (⊤; tt)
+  open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
+  open import Data.Empty using (⊥; ⊥-elim)
+  open import Function.Bundles using (_⇔_)
+  open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
 ```
 
 #### Exercise `∀-distrib-×` (recommended)