From 329ccb88e5cdfa410b02464d268a016028ba4dbc Mon Sep 17 00:00:00 2001
From: Aleksander Wolska <odderwiser@gmail.com>
Date: Fri, 27 Dec 2024 14:30:55 +0100
Subject: [PATCH] Lawful Ord Unit proofs

---
 lib/Haskell/Law/Ord.agda      |  1 +
 lib/Haskell/Law/Ord/Def.agda  |  2 --
 lib/Haskell/Law/Ord/Unit.agda | 23 +++++++++++++++++++++++
 3 files changed, 24 insertions(+), 2 deletions(-)
 create mode 100644 lib/Haskell/Law/Ord/Unit.agda

diff --git a/lib/Haskell/Law/Ord.agda b/lib/Haskell/Law/Ord.agda
index 7f3f2d81..62168ee1 100644
--- a/lib/Haskell/Law/Ord.agda
+++ b/lib/Haskell/Law/Ord.agda
@@ -7,3 +7,4 @@ open import Haskell.Law.Ord.Integer  public
 open import Haskell.Law.Ord.Maybe    public
 open import Haskell.Law.Ord.Nat      public
 open import Haskell.Law.Ord.Ordering public
+open import Haskell.Law.Ord.Unit     public
diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda
index 73b5f387..6d3fd2a4 100644
--- a/lib/Haskell/Law/Ord/Def.agda
+++ b/lib/Haskell/Law/Ord/Def.agda
@@ -178,8 +178,6 @@ postulate instance
 
   iLawfulOrdDouble : IsLawfulOrd Double
 
-  iLawfulOrdUnit : IsLawfulOrd ⊤
-
   iLawfulOrdTuple₂ : ⦃ iOrdA : Ord a ⦄ ⦃ iOrdB : Ord b ⦄
                    → ⦃ IsLawfulOrd a ⦄ → ⦃ IsLawfulOrd b ⦄
                    → IsLawfulOrd (a × b)
diff --git a/lib/Haskell/Law/Ord/Unit.agda b/lib/Haskell/Law/Ord/Unit.agda
new file mode 100644
index 00000000..e8b8d268
--- /dev/null
+++ b/lib/Haskell/Law/Ord/Unit.agda
@@ -0,0 +1,23 @@
+module Haskell.Law.Ord.Unit where
+
+open import Haskell.Prim
+open import Haskell.Prim.Ord
+
+open import Haskell.Law.Ord.Def
+open import Haskell.Law.Eq.Instances
+
+instance
+  iLawfulOrdUnit : IsLawfulOrd ⊤
+
+  iLawfulOrdUnit .comparability _ _ = refl
+  iLawfulOrdUnit .transitivity _ _ _ _ = refl
+  iLawfulOrdUnit .reflexivity _ = refl
+  iLawfulOrdUnit .antisymmetry _ _ _ = refl
+  iLawfulOrdUnit .lte2gte _ _ = refl
+  iLawfulOrdUnit .lt2LteNeq _ _ = refl
+  iLawfulOrdUnit .lt2gt _ _ = refl
+  iLawfulOrdUnit .compareLt _ _ = refl
+  iLawfulOrdUnit .compareGt _ _ = refl
+  iLawfulOrdUnit .compareEq _ _ = refl
+  iLawfulOrdUnit .min2if _ _ = refl
+  iLawfulOrdUnit .max2if _ _ = refl