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

---
 Category/Instance/Preorders/Primitive.agda |  4 +-
 Functor/Forgetful/Instance/Preorder.agda   | 25 +++++++++++
 Functor/Free/Instance/InducedSetoid.agda   | 47 +++++++++++++++++++++
 Functor/Free/Instance/Preorder.agda        | 68 ++++++++++++++++++++++++++++++
 Preorder/Primitive/MonotoneMap.agda        | 23 +++++-----
 5 files changed, 153 insertions(+), 14 deletions(-)
 create mode 100644 Functor/Forgetful/Instance/Preorder.agda
 create mode 100644 Functor/Free/Instance/InducedSetoid.agda
 create mode 100644 Functor/Free/Instance/Preorder.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
 
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
+    }
diff --git a/Functor/Free/Instance/InducedSetoid.agda b/Functor/Free/Instance/InducedSetoid.agda
new file mode 100644
index 0000000..08b65e3
--- /dev/null
+++ b/Functor/Free/Instance/InducedSetoid.agda
@@ -0,0 +1,47 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Free.Instance.InducedSetoid where
+
+-- The induced setoid of a (primitive) preorder
+
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor using (Functor)
+open import Category.Instance.Preorders.Primitive using (Preorders)
+open import Function using (Func)
+open import Level using (Level)
+open import Preorder.Primitive using (Preorder; module Isomorphism)
+open import Preorder.Primitive.MonotoneMap using (MonotoneMap)
+open import Relation.Binary using (Setoid)
+
+module _ {c ℓ : Level} where
+
+  module _ (P : Preorder c ℓ) where
+
+    open Preorder P
+    open Isomorphism P using (_≅_; ≅-isEquivalence)
+
+    ≅-setoid : Setoid c ℓ
+    ≅-setoid = record
+        { Carrier = Carrier
+        ; _≈_ = _≅_
+        ; isEquivalence = ≅-isEquivalence
+        }
+
+  func : {A B : Preorder c ℓ} → MonotoneMap A B → Func (≅-setoid A) (≅-setoid B)
+  func {A} {B} f = let open MonotoneMap f in record
+      { to = map
+      ; cong = map-resp-≅
+      }
+
+  open Isomorphism using (module ≅)
+
+  InducedSetoid : Functor (Preorders c ℓ) (Setoids c ℓ)
+  InducedSetoid = record
+      { F₀ = ≅-setoid
+      ; F₁ = func
+      ; identity = λ {P} → ≅.refl P
+      ; homomorphism = λ {Z = Z} → ≅.refl Z
+      ; F-resp-≈ = λ f≃g {x} → f≃g x
+      }
+
+  module InducedSetoid = Functor InducedSetoid
diff --git a/Functor/Free/Instance/Preorder.agda b/Functor/Free/Instance/Preorder.agda
new file mode 100644
index 0000000..27be24e
--- /dev/null
+++ b/Functor/Free/Instance/Preorder.agda
@@ -0,0 +1,68 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Free.Instance.Preorder where
+
+open import Categories.Category using (Category)
+open import Categories.Category.Instance.Cats using (Cats)
+open import Function using (flip)
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
+open import Category.Instance.Preorders.Primitive using (Preorders)
+open import Level using (Level; _⊔_; suc)
+open import Preorder.Primitive using (Preorder; module Isomorphism)
+open import Preorder.Primitive.MonotoneMap using (MonotoneMap; _≃_; module ≃)
+ 
+-- The "free preorder" of a category
+-- i.e. (0,1)-truncation
+
+-- In this setting, a category is a proof-relevant preorder,
+-- i.e. each proof of A ≤ B is a distinct morphism.
+
+-- To get a preorder from a category,
+-- we ignore this distinction,
+-- making all morphisms A ⇒ B "the same".
+-- Identity and composition become reflexivity and transitivity.
+
+-- Likewise, we can get a monotone map from a functor,
+-- and a pointwise isomorphism of monotone maps from
+-- a natural isomorphism of functors, simply by
+-- forgetting morphism equalities.
+
+module _ {o ℓ e : Level} where
+
+  preorder : Category o ℓ e → Preorder o ℓ
+  preorder C = let open Category C in record
+      { Carrier = Obj
+      ; _≲_ = _⇒_
+      ; refl = id
+      ; trans = flip _∘_
+      }
+
+  module _ {A B : Category o ℓ e} where
+
+    monotoneMap : Functor A B → MonotoneMap (preorder A) (preorder B)
+    monotoneMap F = let open Functor F in record
+        { map = F₀
+        ; mono = F₁
+        }
+
+    open NaturalIsomorphism using (module ⇒; module ⇐)
+
+    pointwiseIsomorphism : {F G : Functor A B} → NaturalIsomorphism F G → monotoneMap F ≃ monotoneMap G
+    pointwiseIsomorphism F≃G X = record
+        { from = ⇒.η F≃G X
+        ; to = ⇐.η F≃G X
+        }
+
+Free : {o ℓ e : Level} → Functor (Cats o ℓ e) (Preorders o ℓ)
+Free = record
+    { F₀ = preorder
+    ; F₁ = monotoneMap
+    ; identity = ≃.refl {x = id}
+    ; homomorphism = λ {f = f} {h} → ≃.refl {x = monotoneMap (h ∘F f)}
+    ; F-resp-≈ = pointwiseIsomorphism
+    }
+  where
+    open Category (Preorders _ _) using (id)
+
+module Free {o ℓ e} = Functor (Free {o} {ℓ} {e})
diff --git a/Preorder/Primitive/MonotoneMap.agda b/Preorder/Primitive/MonotoneMap.agda
index 6a2224b..aad8f0f 100644
--- a/Preorder/Primitive/MonotoneMap.agda
+++ b/Preorder/Primitive/MonotoneMap.agda
@@ -18,14 +18,22 @@ record MonotoneMap {c₁ c₂ ℓ₁ ℓ₂ : Level} (P : Preorder c₁ ℓ₁)
     map : P.Carrier → Q.Carrier
     mono : {x y : P.Carrier} → x P.≲ y → map x Q.≲ map y
 
+  private
+    module P′ = Isomorphism P
+    module Q′ = Isomorphism Q
+
+  map-resp-≅ : {x y : P.Carrier} → x P′.≅ y → map x Q′.≅ map y
+  map-resp-≅ x≅y = let open P′._≅_ x≅y in record
+      { from = mono from
+      ; to = mono to
+      }
+
 -- Pointwise isomorphism of monotone maps
 
 module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {P : Preorder c₁ ℓ₁} {Q : Preorder c₂ ℓ₂} where
 
   private
-    module P where
-      open Preorder P public
-      open Isomorphism P public
+    module P = Preorder P
     module Q = Isomorphism Q
 
   open MonotoneMap using (map)
@@ -54,12 +62,3 @@ module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {P : Preorder c₁ ℓ₁} {Q : Preor
       }
 
   module ≃ = IsEquivalence ≃-isEquivalence
-
-  map-resp-≅ : (f : MonotoneMap P Q) {x y : P.Carrier} → x P.≅ y → map f x Q.≅ map f y
-  map-resp-≅ f x≅y = record
-      { from = mono from
-      ; to = mono to
-      }
-    where
-      open P._≅_ x≅y
-      open MonotoneMap f
-- 
cgit v1.2.3