Skip to content

Commit 2e629e0

Browse files
jmougeotjmougeot
committed
Review
1 parent 49deef9 commit 2e629e0

File tree

5 files changed

+47
-40
lines changed

5 files changed

+47
-40
lines changed

‎src/Relation/Binary/Domain.agda

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Order-theoretic Domains
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
module Relation.Binary.Domain where
10+
11+
------------------------------------------------------------------------
12+
-- Re-export various components of the Domain hierarchy
13+
14+
open import Relation.Binary.Domain.Definitions public
15+
open import Relation.Binary.Domain.Structures public
16+
open import Relation.Binary.Domain.Bundles public

‎src/Relation/Binary/Domain/Bundles.agda

Lines changed: 12 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -34,26 +34,20 @@ record DCPO (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) wher
3434
-- Scott-continuous functions
3535
------------------------------------------------------------------------
3636

37-
module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) (Q : Poset c ℓ₁ ℓ₂) where
38-
private
39-
module P = Poset P
40-
module Q = Poset Q
41-
42-
record ScottContinuous : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
43-
field
44-
f : P.Carrier → Q.Carrier
45-
Scottfunction : IsScottContinuous {P = P} {Q = Q} f
37+
record ScottContinuous {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} :
38+
Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
39+
field
40+
f : Poset.Carrier P → Poset.Carrier Q
41+
Scottfunction : IsScottContinuous {P = P} {Q = Q} f
4642

4743
------------------------------------------------------------------------
4844
-- Lubs
4945
------------------------------------------------------------------------
5046

51-
module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
52-
open Poset P
53-
54-
record Lub {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
55-
constructor mkLub
56-
field
57-
lub : Carrier
58-
is-upperbound : ∀ i → s i ≤ lub
59-
is-least : ∀ y → (∀ i → s i ≤ y) → lub ≤ y
47+
record Lub {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Ix : Set c} (s : Ix → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
48+
private
49+
module P = Poset P
50+
field
51+
lub : P.Carrier
52+
is-upperbound : ∀ i → P._≤_ (s i) lub
53+
is-least : ∀ y → (∀ i → P._≤_ (s i) y) → P._≤_ lub y

‎src/Relation/Binary/Domain/Definitions.agda

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -19,13 +19,6 @@ private
1919
Ix A B : Set o
2020
P : Poset c ℓ e
2121

22-
------------------------------------------------------------------------
23-
-- Monotonicity
24-
------------------------------------------------------------------------
25-
26-
IsMonotone : (P : Poset o ℓ e) → (Q : Poset o' ℓ' e') → (f : Poset.Carrier P → Poset.Carrier Q) → Set (o ⊔ ℓ ⊔ e ⊔ ℓ' ⊔ e')
27-
IsMonotone P Q f = IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ Q) (Poset._≤_ P) (Poset._≤_ Q) f
28-
2922
------------------------------------------------------------------------
3023
-- Directed families
3124
------------------------------------------------------------------------

‎src/Relation/Binary/Domain/Structures.agda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ open import Function using (_∘_)
1414
open import Level using (Level; _⊔_; suc)
1515
open import Relation.Binary.Bundles using (Poset)
1616
open import Relation.Binary.Domain.Definitions
17+
open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
1718

1819
private variable
1920
o ℓ e o' ℓ' e' ℓ₂ : Level

‎src/Relation/Binary/Properties/Domain.agda

Lines changed: 18 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
------------------------------------------------------------------------
22
-- The Agda standard library
33
--
4-
-- Defintions for domain theory
4+
-- Properties satisfied by directed complete partial orders (DCPOs)
55
------------------------------------------------------------------------
66

77
{-# OPTIONS --cubical-compatible --safe #-}
@@ -14,7 +14,6 @@ open import Function using (_∘_; id)
1414
open import Data.Product using (_,_)
1515
open import Data.Bool using (Bool; true; false; if_then_else_)
1616
open import Relation.Binary.Domain.Bundles using (DCPO)
17-
open import Relation.Binary.Domain.Definitions using (IsMonotone)
1817
open import Relation.Binary.Domain.Structures
1918
using (IsDirectedFamily; IsDCPO; IsLub; IsScottContinuous)
2019
open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
@@ -53,7 +52,7 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ
5352
dcpo+scott→monotone : (P-dcpo : IsDCPO P)
5453
→ (f : P.Carrier → Q.Carrier)
5554
→ (scott : IsScottContinuous f)
56-
→ IsMonotone P Q f
55+
→ IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ Q) (Poset._≤_ P) (Poset._≤_ Q) f
5756
dcpo+scott→monotone P-dcpo f scott = record
5857
{ cong = λ {x} {y} x≈y → IsScottContinuous.PreserveEquality scott x≈y
5958
; mono = λ {x} {y} x≤y → mono-proof x y x≤y
@@ -86,7 +85,7 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ
8685

8786
monotone∘directed : ∀ {Ix : Set c} {s : Ix → P.Carrier}
8887
→ (f : P.Carrier → Q.Carrier)
89-
→ IsMonotone P Q f
88+
→ IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ Q) (Poset._≤_ P) (Poset._≤_ Q) f
9089
→ IsDirectedFamily P s
9190
→ IsDirectedFamily Q (f ∘ s)
9291
monotone∘directed f ismonotone dir = record
@@ -106,9 +105,9 @@ module _ where
106105
scott-∘ : ∀ {c ℓ₁ ℓ₂} {P Q R : Poset c ℓ₁ ℓ₂}
107106
→ (f : Poset.Carrier R → Poset.Carrier Q) (g : Poset.Carrier P → Poset.Carrier R)
108107
→ IsScottContinuous {P = R} {Q = Q} f → IsScottContinuous {P = P} {Q = R} g
109-
→ IsMonotone R Q f → IsMonotone P R g
108+
→ IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ R) (Poset._≤_ P) (Poset._≤_ R) g
110109
→ IsScottContinuous {P = P} {Q = Q} (f ∘ g)
111-
scott-∘ f g scottf scottg monof monog = record
110+
scott-∘ f g scottf scottg monog = record
112111
{ PreserveLub = λ dir lub z → f.PreserveLub
113112
(monotone∘directed g monog dir)
114113
(g lub)
@@ -134,14 +133,16 @@ module _ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} (D : DCPO c ℓ₁ ℓ₂
134133
D.⋁-least (D.⋁ s' fam') λ i → D.trans (p i) (D.⋁-≤ i)
135134

136135
module Scott
137-
{c ℓ₁ ℓ₂}
138-
{P : Poset c ℓ₁ ℓ₂}
139-
{D E : DCPO c ℓ₁ ℓ₂}
140-
(let module D = DCPO D)
141-
(let module E = DCPO E)
142-
(f : D.Carrier → E.Carrier)
143-
(isScott : IsScottContinuous {P = D.poset} {Q = E.poset} f)
144-
(mono : IsMonotone D.poset E.poset f) where
136+
{c ℓ₁ ℓ₂}
137+
{P : Poset c ℓ₁ ℓ₂}
138+
{D E : DCPO c ℓ₁ ℓ₂}
139+
(let module D = DCPO D)
140+
(let module E = DCPO E)
141+
(f : D.Carrier → E.Carrier)
142+
(isScott : IsScottContinuous {P = D.poset} {Q = E.poset} f)
143+
(mono : IsOrderHomomorphism (Poset._≈_ D.poset) (Poset._≈_ E.poset)
144+
(Poset._≤_ D.poset) (Poset._≤_ E.poset) f)
145+
where
145146

146147
open DCPO D
147148
open DCPO E
@@ -166,7 +167,9 @@ module _ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} {D E : DCPO c ℓ₁ ℓ
166167
module D = DCPO D
167168
module E = DCPO E
168169

169-
to-scott : (f : D.Carrier → E.Carrier) → IsMonotone D.poset E.poset f
170+
to-scott : (f : D.Carrier → E.Carrier)
171+
→ IsOrderHomomorphism (Poset._≈_ D.poset) (Poset._≈_ E.poset)
172+
(Poset._≤_ D.poset) (Poset._≤_ E.poset) f
170173
→ (∀ {Ix} (s : Ix → D.Carrier) (dir : IsDirectedFamily D.poset s)
171174
→ IsLub E.poset (f ∘ s) (f (D.⋁ s dir)))
172175
→ IsScottContinuous {P = D.poset} {Q = E.poset} f

0 commit comments

Comments
 (0)