From b5e583bb067749f80bd3f7e24e807674eba8b394 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 9 Dec 2025 13:26:36 -0600
Subject: Update Nat properties

---
 Nat/Properties.agda | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Nat/Properties.agda b/Nat/Properties.agda
index 6e04346..0b3da1e 100644
--- a/Nat/Properties.agda
+++ b/Nat/Properties.agda
@@ -19,16 +19,15 @@ open import Categories.Object.Coproduct Nat using (Coproduct; IsCoproduct; IsCop
 open import Coeq Nat using (coequalizer-on-coproduct)
 open import FinMerge using (glue-iter; glue-unglue-once)
 open import FinMerge.Properties using (lemma₂; merge-unmerge; unmerge-merge)
-open import Util using (compare; less; equal; greater; _<_<_)
+open import FinMerge.Util using (compare; less; equal; greater)
 
 open Category Nat
 
-
 makeZeroCoequalizer : {B : ℕ} {f g : 0 ⇒ B} → Coequalizer f g
 makeZeroCoequalizer = record
     { arr = id
     ; isCoequalizer = record
-        { equality = λ()
+        { equality = λ ()
         ; coequalize = λ {_} {h} _ → h
         ; universal = λ _ → refl
         ; unique = λ h≈i∘id → Equiv.sym h≈i∘id
-- 
cgit v1.2.3