blob: 06b4d6053c609d4fb21cce974233447c4d3a66e8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
{-# OPTIONS --without-K --safe #-}
module CatTheory.Category.Instance.Preorders where
-- The category of preordered sets and order-preserving maps.
open import Level
open import Relation.Binary using (Preorder; IsEquivalence; _Preserves_⟶_)
open import Relation.Binary.Morphism using (IsOrderHomomorphism)
open import Relation.Binary.Morphism.Bundles using (PreorderHomomorphism)
import Relation.Binary.Morphism.Construct.Identity as Id
import Relation.Binary.Morphism.Construct.Composition as Comp
open import Categories.Category
open Preorder renaming (_≈_ to ₍_₎_≈_; _∼_ to ₍_₎_∼_)
open PreorderHomomorphism using (⟦_⟧; cong)
private
variable
a₁ a₂ a₃ b₁ b₂ b₃ : Level
A B C : Preorder a₁ a₂ a₃
module _ {A : Preorder a₁ a₂ a₃} {B : Preorder b₁ b₂ b₃} where
infix 4 _≗_
-- Pointwise equality (on order preserving maps).
_≗_ : (f g : PreorderHomomorphism A B) → Set (a₁ ⊔ b₂)
f ≗ g = ∀ {x} → ₍ B ₎ ⟦ f ⟧ x ≈ ⟦ g ⟧ x
≗-isEquivalence : IsEquivalence _≗_
≗-isEquivalence = record
{ refl = Eq.refl B
; sym = λ f≈g → Eq.sym B f≈g
; trans = λ f≈g g≈h → Eq.trans B f≈g g≈h
}
module ≗ = IsEquivalence ≗-isEquivalence
-- The category of posets and order-preserving maps.
Preorders : ∀ c ℓ₁ ℓ₂ → Category (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) (c ⊔ ℓ₁ ⊔ ℓ₂) (c ⊔ ℓ₁)
Preorders c ℓ₁ ℓ₂ = record
{ Obj = Preorder c ℓ₁ ℓ₂
; _⇒_ = PreorderHomomorphism
; _≈_ = _≗_
; id = λ {A} → Id.preorderHomomorphism A
; _∘_ = λ f g → Comp.preorderHomomorphism g f
; assoc = λ {_ _ _ D} → Eq.refl D
; sym-assoc = λ {_ _ _ D} → Eq.refl D
; identityˡ = λ {_ B} → Eq.refl B
; identityʳ = λ {_ B} → Eq.refl B
; identity² = λ {A} → Eq.refl A
; equiv = ≗-isEquivalence
; ∘-resp-≈ = λ {_ _ C _ h} f≈h g≈i → Eq.trans C f≈h (cong h g≈i)
}
|
