From 2a2eeeedbe4d7208d511580f7fed0e30d7f16076 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 6 Jan 2026 10:20:03 -0600
Subject: Add functors from categories to preorders to setoids

---
 Functor/Forgetful/Instance/Preorder.agda | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 Functor/Forgetful/Instance/Preorder.agda

(limited to 'Functor/Forgetful/Instance')

diff --git a/Functor/Forgetful/Instance/Preorder.agda b/Functor/Forgetful/Instance/Preorder.agda
new file mode 100644
index 0000000..e6957d2
--- /dev/null
+++ b/Functor/Forgetful/Instance/Preorder.agda
@@ -0,0 +1,25 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Forgetful.Instance.Preorder where
+
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor using (Functor)
+open import Category.Instance.Preorders using (Preorders)
+open import Level using (Level)
+open import Relation.Binary.Bundles using (Preorder)
+open import Relation.Binary.Morphism using (PreorderHomomorphism)
+
+-- Get the underlying setoid of a preorder.
+-- This is not the same thing as the setoid induced by _≲_.
+
+Forget : {c ℓ e : Level} → Functor (Preorders c ℓ e) (Setoids c ℓ)
+Forget = let open Preorder.Eq in record
+    { F₀ = setoid
+    ; F₁ = λ F → let open PreorderHomomorphism F in record
+        { to = ⟦_⟧
+        ; cong = cong
+        }
+    ; identity = λ {A} → refl A
+    ; homomorphism = λ {_ _ Z} → refl Z
+    ; F-resp-≈ = λ f≗g → f≗g
+    }
-- 
cgit v1.2.3