Category/Instance/Preorders.agda


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

{-# OPTIONS --without-K --safe #-}

module Category.Instance.Preorders where

import Relation.Binary.Morphism.Construct.Identity as Id
import Relation.Binary.Morphism.Construct.Composition as Comp

open import Categories.Category using (Category)
open import Level using (Level; _⊔_; suc)
open import Relation.Binary using (Preorder; IsEquivalence)
open import Relation.Binary.Morphism using (PreorderHomomorphism)

open Preorder using (Carrier; module Eq) renaming (_≈_ to ₍_₎_≈_; _≲_ to ₍_₎_≤_)
open PreorderHomomorphism using (⟦_⟧; cong)

module _ {c₁ c₂ ℓ₁ ℓ₂ e₁ e₂ : Level} {A : Preorder c₁ ℓ₁ e₁} {B : Preorder c₂ ℓ₂ e₂} where

  -- Pointwise equality of monotone maps

  _≗_ : (f g : PreorderHomomorphism A B) → Set (c₁ ⊔ ℓ₂)
  f ≗ g = {x : Carrier A} → ₍ B ₎ ⟦ f ⟧ x ≈ ⟦ g ⟧ x

  infix 4 _≗_

  ≗-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 preorders and monotone maps

Preorders : ∀ c ℓ e → Category (suc (c ⊔ ℓ ⊔ e)) (c ⊔ ℓ ⊔ e) (c ⊔ ℓ)
Preorders c ℓ e = record
  { Obj       = Preorder c ℓ e
  ; _⇒_       = 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)
  }