Lawful Ord Unit proofs

Author: odderwiser

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

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)

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