2 files changed, 148 insertions, 0 deletions
diff --git a/Preorder/Primitive.agda b/Preorder/Primitive.agda
new file mode 100644
index 0000000..04e052f
--- /dev/null
+++ b/Preorder/Primitive.agda
@@ -0,0 +1,83 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_; suc)
+
+module Preorder.Primitive where
+
+import Relation.Binary.Bundles as SetoidBased using (Preorder)
+
+open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEquivalence)
+
+-- A primitive preorder is a type with a reflexive and transitive
+-- relation (in other words, a preorder). The "primitive" qualifier
+-- is used to distinguish it from preorders in the Agda standard library,
+-- which include an underlying equivalence relation on the carrier set.
+
+record Preorder (c ℓ : Level) : Set (suc (c ⊔ ℓ)) where
+
+  field
+    Carrier : Set c
+    _≲_ : Rel Carrier ℓ
+    refl : Reflexive _≲_
+    trans : Transitive _≲_
+
+  infix 4 _≲_
+
+-- Isomorphism in a primitive preorder
+
+module Isomorphism {c ℓ : Level} (P : Preorder c ℓ) where
+
+  open Preorder P
+
+  record _≅_ (x y : Carrier) : Set ℓ where
+    field
+      from : x ≲ y
+      to : y ≲ x
+
+  infix 4 _≅_
+
+  private
+
+    ≅-refl : Reflexive _≅_
+    ≅-refl = record
+        { from = refl
+        ; to = refl
+        }
+
+    ≅-sym : Symmetric _≅_
+    ≅-sym x≅y = let open _≅_ x≅y in record
+        { from = to
+        ; to = from
+        }
+
+    ≅-trans : Transitive _≅_
+    ≅-trans x≅y y≅z = let open _≅_ in record
+        { from = trans (from x≅y) (from y≅z)
+        ; to = trans (to y≅z) (to x≅y)
+        }
+
+  ≅-isEquivalence : IsEquivalence _≅_
+  ≅-isEquivalence = record
+      { refl = ≅-refl
+      ; sym = ≅-sym
+      ; trans = ≅-trans
+      }
+
+  module ≅ = IsEquivalence ≅-isEquivalence
+
+-- Every primitive preorder can be extended to a setoid-based preorder
+-- using isomorphism (_≅_) as the underlying equivalence relation.
+setoidBased : {c ℓ : Level} → Preorder c ℓ → SetoidBased.Preorder c ℓ ℓ
+setoidBased P = record
+    { Carrier = Carrier
+    ; _≈_ = _≅_
+    ; _≲_ = _≲_
+    ; isPreorder = record
+        { isEquivalence = ≅-isEquivalence
+        ; reflexive = _≅_.from
+        ; trans = trans
+        }
+    }
+  where
+    open Preorder P
+    open Isomorphism P
diff --git a/Preorder/Primitive/MonotoneMap.agda b/Preorder/Primitive/MonotoneMap.agda
new file mode 100644
index 0000000..6a2224b
--- /dev/null
+++ b/Preorder/Primitive/MonotoneMap.agda
@@ -0,0 +1,65 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Preorder.Primitive.MonotoneMap where
+
+open import Level using (Level; _⊔_)
+open import Preorder.Primitive using (Preorder; module Isomorphism)
+open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEquivalence)
+
+-- Monotone (order preserving) maps betweeen primitive preorders
+
+record MonotoneMap {c₁ c₂ ℓ₁ ℓ₂ : Level} (P : Preorder c₁ ℓ₁) (Q : Preorder c₂ ℓ₂) : Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂) where
+
+  private
+    module P = Preorder P
+    module Q = Preorder Q
+
+  field
+    map : P.Carrier → Q.Carrier
+    mono : {x y : P.Carrier} → x P.≲ y → map x Q.≲ map y
+
+-- 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 Q = Isomorphism Q
+
+  open MonotoneMap using (map)
+
+  _≃_ : Rel (MonotoneMap P Q) (c₁ ⊔ ℓ₂)
+  _≃_ f g = (x : P.Carrier) → map f x Q.≅ map g x
+
+  infix 4 _≃_
+
+  private
+
+    ≃-refl : Reflexive _≃_
+    ≃-refl {f} x = Q.≅.refl {map f x}
+
+    ≃-sym : Symmetric _≃_
+    ≃-sym f≃g x = Q.≅.sym (f≃g x)
+
+    ≃-trans : Transitive _≃_
+    ≃-trans f≃g g≃h x = Q.≅.trans (f≃g x) (g≃h x)
+
+  ≃-isEquivalence : IsEquivalence _≃_
+  ≃-isEquivalence = record
+      { refl = λ {f} → ≃-refl {f}
+      ; sym = λ {f g} → ≃-sym {f} {g}
+      ; trans = λ {f g h} → ≃-trans {f} {g} {h}
+      }
+
+  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