use equiv from Category

agda · May 23, 2024 · 1342696 · 1342696
1 parent 73a5449
commit 1342696
Showing 1 changed file with 1 addition and 5 deletions.
diff --git a/src/Categories/Category/Restriction/Properties/Poset.agda b/src/Categories/Category/Restriction/Properties/Poset.agda
@@ -23,11 +23,7 @@ module Categories.Category.Restriction.Properties.Poset {o ℓ e} {𝒞 : Catego
     ; _≤_ = λ f g → f ≈ g ∘ f ↓
     ; isPartialOrder = record 
       { isPreorder = record 
-        { isEquivalence = record 
-          { refl = refl 
-          ; sym = sym 
-          ; trans = trans 
-          } 
+        { isEquivalence = equiv
         ; reflexive = λ {x} {y} x≈y → begin 
           x       ≈˘⟨ pidʳ ⟩ 
           x ∘ x ↓ ≈⟨ x≈y ⟩∘⟨refl ⟩