From 2a2eeeedbe4d7208d511580f7fed0e30d7f16076 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Tue, 6 Jan 2026 10:20:03 -0600 Subject: Add functors from categories to preorders to setoids --- Category/Instance/Preorders/Primitive.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Category/Instance/Preorders/Primitive.agda') diff --git a/Category/Instance/Preorders/Primitive.agda b/Category/Instance/Preorders/Primitive.agda index 49b687f..9c36d03 100644 --- a/Category/Instance/Preorders/Primitive.agda +++ b/Category/Instance/Preorders/Primitive.agda @@ -7,7 +7,7 @@ open import Categories.Category.Helper using (categoryHelper) open import Function using (id; _∘_) open import Level using (Level; _⊔_; suc) open import Preorder.Primitive using (Preorder; module Isomorphism) -open import Preorder.Primitive.MonotoneMap using (MonotoneMap; _≃_; ≃-isEquivalence; module ≃; map-resp-≅) +open import Preorder.Primitive.MonotoneMap using (MonotoneMap; _≃_; ≃-isEquivalence; module ≃) -- The category of primitive preorders and monotone maps @@ -39,7 +39,7 @@ private → compose f g ≃ compose h i compose-resp-≃ {C = C} {h = h} {g} f≃h g≃i x = ≅.trans (f≃h (map g x)) (map-resp-≅ h (g≃i x)) where - open MonotoneMap using (map; mono) + open MonotoneMap using (map; mono; map-resp-≅) open Preorder C open Isomorphism C -- cgit v1.2.3