From 0b783d89327eb5de1d20223559aa6ac9111075b7 Mon Sep 17 00:00:00 2001
From: Alan Jeffrey <403333+asajeffrey@users.noreply.github.com>
Date: Fri, 18 Feb 2022 16:47:04 -0600
Subject: [PATCH] Add Properties.Equality to prototyping (#376)

---
 prototyping/Properties.agda               |  2 ++
 prototyping/Properties/Contradiction.agda |  9 +++++++++
 prototyping/Properties/Equality.agda      | 23 +++++++++++++++++++++++
 3 files changed, 34 insertions(+)
 create mode 100644 prototyping/Properties/Contradiction.agda
 create mode 100644 prototyping/Properties/Equality.agda

diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda
index b08a3a81..1a6f92fa 100644
--- a/prototyping/Properties.agda
+++ b/prototyping/Properties.agda
@@ -1,5 +1,7 @@
 module Properties where
 
+import Properties.Contradiction
 import Properties.Dec
+import Properties.Equality
 import Properties.Step
 import Properties.Remember
diff --git a/prototyping/Properties/Contradiction.agda b/prototyping/Properties/Contradiction.agda
new file mode 100644
index 00000000..e9a92ad5
--- /dev/null
+++ b/prototyping/Properties/Contradiction.agda
@@ -0,0 +1,9 @@
+module Properties.Contradiction where
+
+data ⊥ : Set where
+
+¬ : Set → Set
+¬ A = A → ⊥
+
+CONTRADICTION : ∀ {A : Set} → ⊥ → A
+CONTRADICTION ()
diff --git a/prototyping/Properties/Equality.agda b/prototyping/Properties/Equality.agda
new file mode 100644
index 00000000..c027bee3
--- /dev/null
+++ b/prototyping/Properties/Equality.agda
@@ -0,0 +1,23 @@
+module Properties.Equality where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Properties.Contradiction using (¬)
+
+sym : ∀ {A : Set} {a b : A} → (a ≡ b) → (b ≡ a)
+sym refl = refl
+
+trans : ∀ {A : Set} {a b c : A} → (a ≡ b) → (b ≡ c) → (a ≡ c)
+trans refl refl = refl
+
+cong : ∀ {A B : Set} {a b : A} (f : A → B) → (a ≡ b) → (f a ≡ f b)
+cong f refl = refl
+
+subst₁ : ∀ {A : Set} {a b : A} (F : A → Set) → (a ≡ b) → (F a) → (F b)
+subst₁ F refl x = x
+
+subst₂ : ∀ {A B : Set} {a b : A} {c d : B} (F : A → B → Set) → (a ≡ b) → (c ≡ d) → (F a c) → (F b d)
+subst₂ F refl refl x = x
+
+_≢_ : ∀ {A : Set} → A → A → Set
+(a ≢ b) = ¬(a ≡ b)
+