Add functors from categories to preorders to setoids

1 files changed, 25 insertions, 0 deletions

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
+    }