blob: aad8f0f9ea00fb8c995778513203f7e62aa04361 (
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
59
60
61
62
63
64
|
{-# 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
private
module P′ = Isomorphism P
module Q′ = Isomorphism Q
map-resp-≅ : {x y : P.Carrier} → x P′.≅ y → map x Q′.≅ map y
map-resp-≅ x≅y = let open P′._≅_ x≅y in record
{ from = mono from
; to = mono to
}
-- Pointwise isomorphism of monotone maps
module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {P : Preorder c₁ ℓ₁} {Q : Preorder c₂ ℓ₂} where
private
module P = Preorder P
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
|
