diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-06 10:20:03 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-06 10:20:03 -0600 |
| commit | 2a2eeeedbe4d7208d511580f7fed0e30d7f16076 (patch) | |
| tree | e4a802387735e1c46a9b05cf5d0b571e28728371 /Category/Instance/Preorders/Primitive.agda | |
| parent | 1c0a486856d80ad7d8cb6174c49ad990d5f36088 (diff) | |
Add functors from categories to preorders to setoids
Diffstat (limited to 'Category/Instance/Preorders/Primitive.agda')
| -rw-r--r-- | Category/Instance/Preorders/Primitive.agda | 4 |
1 files changed, 2 insertions, 2 deletions
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 |