diff options
| -rw-r--r-- | Category/Instance/Preorders/Primitive.agda | 58 | ||||
| -rw-r--r-- | Preorder/Primitive.agda | 83 | ||||
| -rw-r--r-- | Preorder/Primitive/MonotoneMap.agda | 65 |
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 |