Add non-setoid-based preorders

3 files changed, 206 insertions, 0 deletions

diff --git a/Category/Instance/Preorders/Primitive.agda b/Category/Instance/Preorders/Primitive.agda
new file mode 100644
index 0000000..49b687f
--- /dev/null
+++ b/Category/Instance/Preorders/Primitive.agda
@@ -0,0 +1,58 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Category.Instance.Preorders.Primitive where
+
+open import Categories.Category using (Category)
+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-≅)
+
+-- The category of primitive preorders and monotone maps
+
+private
+
+  module _ {c ℓ : Level} where
+
+    identity : {A : Preorder c ℓ} → MonotoneMap A A
+    identity = record
+        { map = id
+        ; mono = id
+        }
+
+    compose : {A B C : Preorder c ℓ} → MonotoneMap B C → MonotoneMap A B → MonotoneMap A C
+    compose f g = record
+        { map = f.map ∘ g.map
+        ; mono = f.mono ∘ g.mono
+        }
+      where
+        module f = MonotoneMap f
+        module g = MonotoneMap g
+
+    compose-resp-≃
+        : {A B C : Preorder c ℓ}
+          {f h : MonotoneMap B C}
+          {g i : MonotoneMap A B}
+        → f ≃ h
+        → g ≃ i
+        → 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 Preorder C
+        open Isomorphism C
+
+Preorders : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
+Preorders c ℓ = categoryHelper record
+    { Obj = Preorder c ℓ
+    ; _⇒_ = MonotoneMap
+    ; _≈_ = _≃_
+    ; id = identity
+    ; _∘_ = compose
+    ; assoc = λ {f = f} {g h} → ≃.refl {x = compose (compose h g) f}
+    ; identityˡ = λ {f = f} → ≃.refl {x = f}
+    ; identityʳ = λ {f = f} → ≃.refl {x = f}
+    ; equiv = ≃-isEquivalence
+    ; ∘-resp-≈ = λ {f = f} {g h i} → compose-resp-≃ {f = f} {g} {h} {i}
+    }
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