← Back to branch summary

~ubuntu-branches/ubuntu/precise/agda-stdlib/precise

« back to all changes in this revision

Viewing changes to src/Relation/Binary/Product/StrictLex.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-02-25 22:28:40 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110225222840-jt16gl302kca7h0g
Tags: 0.5-1~ubuntu1
https://launchpad.net/bugs/725364
http://bugs.debian.org/573807
http://bugs.debian.org/598708

* Upload to Ubuntu from Debian's VCS due to delays in unstable caused by
  the GHC 7 transition (LP: #725364)
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [0fb0600] Standards-Version → 3.9.1, no changes required
* [d3f13b8] Update required Agda version to 2.2.8
* [cc1f5c8] Imported Upstream version 0.4
* [2c82171] Add watch file
* [9251e0b] Imported Upstream version 0.5
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Binary/Product/StrictLex.agda
2
2
-- Lexicographic products of binary relations
3
3
------------------------------------------------------------------------
4
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
5
7
-- The definition of lexicographic product used here is suitable if
6
8
-- the left-hand relation is a strict partial order.
7
9
 
8
10
module Relation.Binary.Product.StrictLex where
9
11
 
10
 
open import Data.Function
 
12
open import Function
11
13
open import Data.Product
12
14
open import Data.Sum
13
15
open import Data.Empty
18
20
open import Relation.Binary.Consequences
19
21
open import Relation.Binary.Product.Pointwise as Pointwise
20
22
  using (_×-Rel_)
 
23
open import Relation.Nullary
21
24
 
22
25
private
23
 
 module Dummy {a₁ a₂ : Set} where
 
26
 module Dummy {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where
24
27
 
25
 
  ×-Lex : (≈₁ <₁ : Rel a₁ zero) → (≤₂ : Rel a₂ zero) →
26
 
          Rel (a₁ × a₂) zero
27
 
  ×-Lex ≈₁ <₁ ≤₂ = (<₁ on proj₁) -⊎- (≈₁ on proj₁) -×- (≤₂ on proj₂)
 
28
  ×-Lex : (_≈₁_ _<₁_ : Rel A₁ ℓ₁) → (_≤₂_ : Rel A₂ ℓ₂) →
 
29
          Rel (A₁ × A₂) _
 
30
  ×-Lex _≈₁_ _<₁_ _≤₂_ =
 
31
    (_<₁_ on proj₁) -⊎- (_≈₁_ on proj₁) -×- (_≤₂_ on proj₂)
28
32
 
29
33
  -- Some properties which are preserved by ×-Lex (under certain
30
34
  -- assumptions).
31
35
 
32
 
  ×-reflexive : ∀ ≈₁ ∼₁ {≈₂} ≤₂ →
33
 
                ≈₂ ⇒ ≤₂ → (≈₁ ×-Rel ≈₂) ⇒ (×-Lex ≈₁ ∼₁ ≤₂)
 
36
  ×-reflexive : ∀ _≈₁_ _∼₁_ {_≈₂_ : Rel A₂ ℓ₂} _≤₂_ →
 
37
                _≈₂_ ⇒ _≤₂_ → (_≈₁_ ×-Rel _≈₂_) ⇒ (×-Lex _≈₁_ _∼₁_ _≤₂_)
34
38
  ×-reflexive _ _ _ refl₂ = λ x≈y →
35
39
    inj₂ (proj₁ x≈y , refl₂ (proj₂ x≈y))
36
40
 
37
 
  _×-irreflexive_ : ∀ {≈₁ <₁} → Irreflexive ≈₁ <₁ →
38
 
                    ∀ {≈₂ <₂} → Irreflexive ≈₂ <₂ →
39
 
                    Irreflexive (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ <₁ <₂)
 
41
  _×-irreflexive_ : ∀ {_≈₁_ _<₁_}             → Irreflexive _≈₁_ _<₁_ →
 
42
                    ∀ {_≈₂_ _<₂_ : Rel A₂ ℓ₂} → Irreflexive _≈₂_ _<₂_ →
 
43
                    Irreflexive (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_)
40
44
  (ir₁ ×-irreflexive ir₂) x≈y (inj₁ x₁<y₁) = ir₁ (proj₁ x≈y) x₁<y₁
41
45
  (ir₁ ×-irreflexive ir₂) x≈y (inj₂ x≈<y)  =
42
46
    ir₂ (proj₂ x≈y) (proj₂ x≈<y)
43
47
 
44
48
  ×-transitive :
45
 
    ∀ {≈₁ <₁} → IsEquivalence ≈₁ → <₁ Respects₂ ≈₁ → Transitive <₁ →
46
 
    ∀ {≤₂} → Transitive ≤₂ →
47
 
    Transitive (×-Lex ≈₁ <₁ ≤₂)
48
 
  ×-transitive {≈₁ = ≈₁} {<₁ = <₁} eq₁ resp₁ trans₁
49
 
               {≤₂ = ≤₂} trans₂ {x} {y} {z} = trans {x} {y} {z}
 
49
    ∀ {_≈₁_ _<₁_} →
 
50
    IsEquivalence _≈₁_ → _<₁_ Respects₂ _≈₁_ → Transitive _<₁_ →
 
51
    ∀ {_≤₂_} →
 
52
    Transitive _≤₂_ →
 
53
    Transitive (×-Lex _≈₁_ _<₁_ _≤₂_)
 
54
  ×-transitive {_≈₁_ = _≈₁_} {_<₁_ = _<₁_} eq₁ resp₁ trans₁
 
55
               {_≤₂_ = _≤₂_} trans₂ {x} {y} {z} = trans {x} {y} {z}
50
56
    where
51
57
    module Eq₁ = IsEquivalence eq₁
52
58
 
53
 
    trans : Transitive (×-Lex ≈₁ <₁ ≤₂)
 
59
    trans : Transitive (×-Lex _≈₁_ _<₁_ _≤₂_)
54
60
    trans (inj₁ x₁<y₁) (inj₁ y₁<z₁) = inj₁ (trans₁ x₁<y₁ y₁<z₁)
55
61
    trans (inj₁ x₁<y₁) (inj₂ y≈≤z)  =
56
62
      inj₁ (proj₁ resp₁ (proj₁ y≈≤z) x₁<y₁)
61
67
           , trans₂    (proj₂ x≈≤y) (proj₂ y≈≤z) )
62
68
 
63
69
  ×-antisymmetric :
64
 
    ∀ {≈₁ <₁} → Symmetric ≈₁ → Irreflexive ≈₁ <₁ → Asymmetric <₁ →
65
 
    ∀ {≈₂ ≤₂} → Antisymmetric ≈₂ ≤₂ →
66
 
    Antisymmetric (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ <₁ ≤₂)
67
 
  ×-antisymmetric {≈₁ = ≈₁} {<₁ = <₁} sym₁ irrefl₁ asym₁
68
 
                  {≈₂ = ≈₂} {≤₂ = ≤₂} antisym₂ {x} {y} =
 
70
    ∀ {_≈₁_ _<₁_} →
 
71
    Symmetric _≈₁_ → Irreflexive _≈₁_ _<₁_ → Asymmetric _<₁_ →
 
72
    ∀ {_≈₂_ _≤₂_ : Rel A₂ ℓ₂} →
 
73
    Antisymmetric _≈₂_ _≤₂_ →
 
74
    Antisymmetric (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _≤₂_)
 
75
  ×-antisymmetric {_≈₁_ = _≈₁_} {_<₁_ = _<₁_} sym₁ irrefl₁ asym₁
 
76
                  {_≈₂_ = _≈₂_} {_≤₂_ = _≤₂_} antisym₂ {x} {y} =
69
77
    antisym {x} {y}
70
78
    where
71
 
    antisym : Antisymmetric (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ <₁ ≤₂)
 
79
    antisym : Antisymmetric (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _≤₂_)
72
80
    antisym (inj₁ x₁<y₁) (inj₁ y₁<x₁) =
73
81
      ⊥-elim {Whatever = _ × _} $ asym₁ x₁<y₁ y₁<x₁
74
82
    antisym (inj₁ x₁<y₁) (inj₂ y≈≤x)  =
79
87
      proj₁ x≈≤y , antisym₂ (proj₂ x≈≤y) (proj₂ y≈≤x)
80
88
 
81
89
  ×-asymmetric :
82
 
    ∀ {≈₁ <₁} → Symmetric ≈₁ → <₁ Respects₂ ≈₁ → Asymmetric <₁ →
83
 
    ∀ {<₂} → Asymmetric <₂ →
84
 
    Asymmetric (×-Lex ≈₁ <₁ <₂)
85
 
  ×-asymmetric {≈₁ = ≈₁} {<₁ = <₁} sym₁ resp₁ asym₁
86
 
               {<₂ = <₂} asym₂ {x} {y} = asym {x} {y}
 
90
    ∀ {_≈₁_ _<₁_} →
 
91
    Symmetric _≈₁_ → _<₁_ Respects₂ _≈₁_ → Asymmetric _<₁_ →
 
92
    ∀ {_<₂_} →
 
93
    Asymmetric _<₂_ →
 
94
    Asymmetric (×-Lex _≈₁_ _<₁_ _<₂_)
 
95
  ×-asymmetric {_≈₁_ = _≈₁_} {_<₁_ = _<₁_} sym₁ resp₁ asym₁
 
96
               {_<₂_ = _<₂_} asym₂ {x} {y} = asym {x} {y}
87
97
    where
88
 
    irrefl₁ : Irreflexive ≈₁ <₁
 
98
    irrefl₁ : Irreflexive _≈₁_ _<₁_
89
99
    irrefl₁ = asym⟶irr resp₁ sym₁ asym₁
90
100
 
91
 
    asym : Asymmetric (×-Lex ≈₁ <₁ <₂)
 
101
    asym : Asymmetric (×-Lex _≈₁_ _<₁_ _<₂_)
92
102
    asym (inj₁ x₁<y₁) (inj₁ y₁<x₁) = asym₁ x₁<y₁ y₁<x₁
93
103
    asym (inj₁ x₁<y₁) (inj₂ y≈<x)  = irrefl₁ (sym₁ $ proj₁ y≈<x) x₁<y₁
94
104
    asym (inj₂ x≈<y)  (inj₁ y₁<x₁) = irrefl₁ (sym₁ $ proj₁ x≈<y) y₁<x₁
95
105
    asym (inj₂ x≈<y)  (inj₂ y≈<x)  = asym₂ (proj₂ x≈<y) (proj₂ y≈<x)
96
106
 
97
107
  ×-≈-respects₂ :
98
 
    ∀ {≈₁ <₁} → IsEquivalence ≈₁ → <₁ Respects₂ ≈₁ →
99
 
    ∀ {≈₂ <₂} → <₂ Respects₂ ≈₂ →
100
 
    (×-Lex ≈₁ <₁ <₂) Respects₂ (≈₁ ×-Rel ≈₂)
101
 
  ×-≈-respects₂ {≈₁ = ≈₁} {<₁ = <₁} eq₁ resp₁
102
 
                {≈₂ = ≈₂} {<₂ = <₂}     resp₂ =
 
108
    ∀ {_≈₁_ _<₁_} → IsEquivalence _≈₁_ → _<₁_ Respects₂ _≈₁_ →
 
109
    {_≈₂_ _<₂_ : Rel A₂ ℓ₂} → _<₂_ Respects₂ _≈₂_ →
 
110
    (×-Lex _≈₁_ _<₁_ _<₂_) Respects₂ (_≈₁_ ×-Rel _≈₂_)
 
111
  ×-≈-respects₂ {_≈₁_ = _≈₁_} {_<₁_ = _<₁_} eq₁ resp₁
 
112
                {_≈₂_ = _≈₂_} {_<₂_ = _<₂_}     resp₂ =
103
113
    (λ {x y z} → resp¹ {x} {y} {z}) ,
104
114
    (λ {x y z} → resp² {x} {y} {z})
105
115
    where
106
 
    < = ×-Lex ≈₁ <₁ <₂
 
116
    _<_ = ×-Lex _≈₁_ _<₁_ _<₂_
107
117
 
108
118
    open IsEquivalence eq₁ renaming (sym to sym₁; trans to trans₁)
109
119
 
110
 
    resp¹ : ∀ {x} → (< x) Respects (≈₁ ×-Rel ≈₂)
 
120
    resp¹ : ∀ {x} → (_<_ x) Respects (_≈₁_ ×-Rel _≈₂_)
111
121
    resp¹ y≈y' (inj₁ x₁<y₁) = inj₁ (proj₁ resp₁ (proj₁ y≈y') x₁<y₁)
112
122
    resp¹ y≈y' (inj₂ x≈<y)  =
113
123
      inj₂ ( trans₁ (proj₁ x≈<y) (proj₁ y≈y')
114
124
           , proj₁ resp₂ (proj₂ y≈y') (proj₂ x≈<y) )
115
125
 
116
 
    resp² : ∀ {y} → (flip < y) Respects (≈₁ ×-Rel ≈₂)
 
126
    resp² : ∀ {y} → (flip _<_ y) Respects (_≈₁_ ×-Rel _≈₂_)
117
127
    resp² x≈x' (inj₁ x₁<y₁) = inj₁ (proj₂ resp₁ (proj₁ x≈x') x₁<y₁)
118
128
    resp² x≈x' (inj₂ x≈<y)  =
119
129
      inj₂ ( trans₁ (sym₁ $ proj₁ x≈x') (proj₁ x≈<y)
120
130
           , proj₂ resp₂ (proj₂ x≈x') (proj₂ x≈<y) )
121
131
 
122
 
  ×-decidable : ∀ {≈₁ <₁} → Decidable ≈₁ → Decidable <₁ →
123
 
                ∀ {≤₂} → Decidable ≤₂ →
124
 
                Decidable (×-Lex ≈₁ <₁ ≤₂)
 
132
  ×-decidable : ∀ {_≈₁_ _<₁_} → Decidable _≈₁_ → Decidable _<₁_ →
 
133
                ∀ {_≤₂_} → Decidable _≤₂_ →
 
134
                Decidable (×-Lex _≈₁_ _<₁_ _≤₂_)
125
135
  ×-decidable dec-≈₁ dec-<₁ dec-≤₂ = λ x y →
126
136
    dec-<₁ (proj₁ x) (proj₁ y)
127
137
      ⊎-dec
129
139
       ×-dec
130
140
     dec-≤₂ (proj₂ x) (proj₂ y))
131
141
 
132
 
  ×-total : ∀ {≈₁ <₁} → Total <₁ →
133
 
            ∀ {≤₂} →
134
 
            Total (×-Lex ≈₁ <₁ ≤₂)
135
 
  ×-total {≈₁ = ≈₁} {<₁ = <₁} total₁ {≤₂ = ≤₂} = total
 
142
  ×-total : ∀ {_≈₁_ _<₁_} → Total _<₁_ →
 
143
            ∀ {_≤₂_} →
 
144
            Total (×-Lex _≈₁_ _<₁_ _≤₂_)
 
145
  ×-total {_≈₁_ = _≈₁_} {_<₁_ = _<₁_} total₁ {_≤₂_ = _≤₂_} = total
136
146
    where
137
 
    total : Total (×-Lex ≈₁ <₁ ≤₂)
 
147
    total : Total (×-Lex _≈₁_ _<₁_ _≤₂_)
138
148
    total x y with total₁ (proj₁ x) (proj₁ y)
139
149
    ... | inj₁ x₁<y₁ = inj₁ (inj₁ x₁<y₁)
140
150
    ... | inj₂ x₁>y₁ = inj₂ (inj₁ x₁>y₁)
141
151
 
142
 
  ×-compare : ∀ {≈₁ <₁} → Symmetric ≈₁ → Trichotomous ≈₁ <₁ →
143
 
              ∀ {≈₂ <₂} → Trichotomous ≈₂ <₂ →
144
 
              Trichotomous (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ <₁ <₂)
145
 
  ×-compare {≈₁} {<₁} sym₁ compare₁ {≈₂} {<₂} compare₂ = cmp
 
152
  ×-compare :
 
153
    {_≈₁_ _<₁_ : Rel A₁ ℓ₁} → Symmetric _≈₁_ → Trichotomous _≈₁_ _<₁_ →
 
154
    {_≈₂_ _<₂_ : Rel A₂ ℓ₂} → Trichotomous _≈₂_ _<₂_ →
 
155
    Trichotomous (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_)
 
156
  ×-compare {_≈₁_} {_<₁_} sym₁ compare₁ {_≈₂_} {_<₂_} compare₂ = cmp
146
157
    where
147
 
    cmp : Trichotomous (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ <₁ <₂)
148
 
    cmp (x₁ , x₂) (y₁ , y₂) with compare₁ x₁ y₁
149
 
    ... | tri< x₁<y₁ x₁≉y₁ x₁≯y₁ = tri< (inj₁ x₁<y₁) (x₁≉y₁ ∘ proj₁)
150
 
                                        [ x₁≯y₁ , x₁≉y₁ ∘ sym₁ ∘ proj₁ ]
151
 
    ... | tri> x₁≮y₁ x₁≉y₁ x₁>y₁ = tri> [ x₁≮y₁ , x₁≉y₁ ∘ proj₁ ]
152
 
                                        (x₁≉y₁ ∘ proj₁) (inj₁ x₁>y₁)
153
 
    ... | tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁ with compare₂ x₂ y₂
154
 
    ...   | tri< x₂<y₂ x₂≉y₂ x₂≯y₂ = tri< (inj₂ (x₁≈y₁ , x₂<y₂))
155
 
                                          (x₂≉y₂ ∘ proj₂)
156
 
                                          [ x₁≯y₁ , x₂≯y₂ ∘ proj₂ ]
157
 
    ...   | tri> x₂≮y₂ x₂≉y₂ x₂>y₂ = tri> [ x₁≮y₁ , x₂≮y₂ ∘ proj₂ ]
158
 
                                          (x₂≉y₂ ∘ proj₂)
159
 
                                          (inj₂ (sym₁ x₁≈y₁ , x₂>y₂))
160
 
    ...   | tri≈ x₂≮y₂ x₂≈y₂ x₂≯y₂ = tri≈ [ x₁≮y₁ , x₂≮y₂ ∘ proj₂ ]
161
 
                                          (x₁≈y₁ , x₂≈y₂)
162
 
                                          [ x₁≯y₁ , x₂≯y₂ ∘ proj₂ ]
 
158
    cmp″ : ∀ {x₁ y₁ x₂ y₂} →
 
159
           ¬ (x₁ <₁ y₁) → x₁ ≈₁ y₁ → ¬ (y₁ <₁ x₁) →
 
160
           Tri (x₂ <₂ y₂) (x₂ ≈₂ y₂) (y₂ <₂ x₂) →
 
161
           Tri (×-Lex _≈₁_ _<₁_ _<₂_ (x₁ , x₂) (y₁ , y₂))
 
162
               ((_≈₁_ ×-Rel _≈₂_) (x₁ , x₂) (y₁ , y₂))
 
163
               (×-Lex _≈₁_ _<₁_ _<₂_ (y₁ , y₂) (x₁ , x₂))
 
164
    cmp″ x₁≮y₁ x₁≈y₁ x₁≯y₁ (tri< x₂<y₂ x₂≉y₂ x₂≯y₂) =
 
165
      tri< (inj₂ (x₁≈y₁ , x₂<y₂))
 
166
           (x₂≉y₂ ∘ proj₂)
 
167
           [ x₁≯y₁ , x₂≯y₂ ∘ proj₂ ]
 
168
    cmp″ x₁≮y₁ x₁≈y₁ x₁≯y₁ (tri> x₂≮y₂ x₂≉y₂ x₂>y₂) =
 
169
      tri> [ x₁≮y₁ , x₂≮y₂ ∘ proj₂ ]
 
170
           (x₂≉y₂ ∘ proj₂)
 
171
           (inj₂ (sym₁ x₁≈y₁ , x₂>y₂))
 
172
    cmp″ x₁≮y₁ x₁≈y₁ x₁≯y₁ (tri≈ x₂≮y₂ x₂≈y₂ x₂≯y₂) =
 
173
      tri≈ [ x₁≮y₁ , x₂≮y₂ ∘ proj₂ ]
 
174
           (x₁≈y₁ , x₂≈y₂)
 
175
           [ x₁≯y₁ , x₂≯y₂ ∘ proj₂ ]
 
176
 
 
177
    cmp′ : ∀ {x₁ y₁} → Tri (x₁ <₁ y₁) (x₁ ≈₁ y₁) (y₁ <₁ x₁) →
 
178
           ∀ x₂ y₂ →
 
179
           Tri (×-Lex _≈₁_ _<₁_ _<₂_ (x₁ , x₂) (y₁ , y₂))
 
180
               ((_≈₁_ ×-Rel _≈₂_) (x₁ , x₂) (y₁ , y₂))
 
181
               (×-Lex _≈₁_ _<₁_ _<₂_ (y₁ , y₂) (x₁ , x₂))
 
182
    cmp′ (tri< x₁<y₁ x₁≉y₁ x₁≯y₁) x₂ y₂ =
 
183
      tri< (inj₁ x₁<y₁) (x₁≉y₁ ∘ proj₁) [ x₁≯y₁ , x₁≉y₁ ∘ sym₁ ∘ proj₁ ]
 
184
    cmp′ (tri> x₁≮y₁ x₁≉y₁ x₁>y₁) x₂ y₂ =
 
185
      tri> [ x₁≮y₁ , x₁≉y₁ ∘ proj₁ ] (x₁≉y₁ ∘ proj₁) (inj₁ x₁>y₁)
 
186
    cmp′ (tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁) x₂ y₂ =
 
187
      cmp″ x₁≮y₁ x₁≈y₁ x₁≯y₁ (compare₂ x₂ y₂)
 
188
 
 
189
    cmp : Trichotomous (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_)
 
190
    cmp (x₁ , x₂) (y₁ , y₂) = cmp′ (compare₁ x₁ y₁) x₂ y₂
163
191
 
164
192
  -- Some collections of properties which are preserved by ×-Lex.
165
193
 
166
 
  _×-isPreorder_ : ∀ {≈₁ ∼₁} → IsPreorder ≈₁ ∼₁ →
167
 
                   ∀ {≈₂ ∼₂} → IsPreorder ≈₂ ∼₂ →
168
 
                   IsPreorder (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ ∼₁ ∼₂)
169
 
  _×-isPreorder_ {≈₁ = ≈₁} {∼₁ = ∼₁} pre₁ {∼₂ = ∼₂} pre₂ = record
170
 
    { isEquivalence = Pointwise._×-isEquivalence_
171
 
                        (isEquivalence pre₁) (isEquivalence pre₂)
172
 
    ; reflexive     = λ {x y} →
173
 
                      ×-reflexive ≈₁ ∼₁ ∼₂ (reflexive pre₂) {x} {y}
174
 
    ; trans         = λ {x y z} →
175
 
                      ×-transitive
176
 
                        (isEquivalence pre₁) (∼-resp-≈ pre₁) (trans pre₁)
177
 
                        {≤₂ = ∼₂} (trans pre₂) {x} {y} {z}
178
 
    ; ∼-resp-≈      = ×-≈-respects₂ (isEquivalence pre₁)
179
 
                                        (∼-resp-≈ pre₁)
180
 
                                        (∼-resp-≈ pre₂)
181
 
    }
 
194
  _×-isPreorder_ : ∀ {_≈₁_ _∼₁_} → IsPreorder _≈₁_ _∼₁_ →
 
195
                   ∀ {_≈₂_ _∼₂_} → IsPreorder _≈₂_ _∼₂_ →
 
196
                   IsPreorder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _∼₁_ _∼₂_)
 
197
  _×-isPreorder_ {_≈₁_ = _≈₁_} {_∼₁_ = _∼₁_} pre₁ {_∼₂_ = _∼₂_} pre₂ =
 
198
    record
 
199
      { isEquivalence = Pointwise._×-isEquivalence_
 
200
                          (isEquivalence pre₁) (isEquivalence pre₂)
 
201
      ; reflexive     = λ {x y} →
 
202
                        ×-reflexive _≈₁_ _∼₁_ _∼₂_ (reflexive pre₂)
 
203
                                    {x} {y}
 
204
      ; trans         = λ {x y z} →
 
205
                        ×-transitive
 
206
                          (isEquivalence pre₁) (∼-resp-≈ pre₁)
 
207
                          (trans pre₁) {_≤₂_ = _∼₂_} (trans pre₂)
 
208
                          {x} {y} {z}
 
209
      }
182
210
    where open IsPreorder
183
211
 
184
212
  _×-isStrictPartialOrder_ :
185
 
    ∀ {≈₁ <₁} → IsStrictPartialOrder ≈₁ <₁ →
186
 
    ∀ {≈₂ <₂} → IsStrictPartialOrder ≈₂ <₂ →
187
 
    IsStrictPartialOrder (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ <₁ <₂)
188
 
  _×-isStrictPartialOrder_ {<₁ = <₁} spo₁ {<₂ = <₂} spo₂ =
 
213
    ∀ {_≈₁_ _<₁_} → IsStrictPartialOrder _≈₁_ _<₁_ →
 
214
    ∀ {_≈₂_ _<₂_} → IsStrictPartialOrder _≈₂_ _<₂_ →
 
215
    IsStrictPartialOrder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_)
 
216
  _×-isStrictPartialOrder_ {_<₁_ = _<₁_} spo₁ {_<₂_ = _<₂_} spo₂ =
189
217
    record
190
218
      { isEquivalence = Pointwise._×-isEquivalence_
191
219
                          (isEquivalence spo₁) (isEquivalence spo₂)
192
220
      ; irrefl        = λ {x y} →
193
 
                        _×-irreflexive_ {<₁ = <₁} (irrefl spo₁)
194
 
                                        {<₂ = <₂} (irrefl spo₂) {x} {y}
 
221
                        _×-irreflexive_ {_<₁_ = _<₁_} (irrefl spo₁)
 
222
                                        {_<₂_ = _<₂_} (irrefl spo₂)
 
223
                                        {x} {y}
195
224
      ; trans         = λ {x y z} →
196
225
                        ×-transitive
197
 
                          {<₁ = <₁} (isEquivalence spo₁) (<-resp-≈ spo₁)
198
 
                                    (trans spo₁)
199
 
                          {≤₂ = <₂} (trans spo₂) {x} {y} {z}
 
226
                          {_<₁_ = _<₁_} (isEquivalence spo₁)
 
227
                                        (<-resp-≈ spo₁) (trans spo₁)
 
228
                          {_≤₂_ = _<₂_} (trans spo₂) {x} {y} {z}
200
229
      ; <-resp-≈      = ×-≈-respects₂ (isEquivalence spo₁)
201
 
                                          (<-resp-≈ spo₁)
202
 
                                          (<-resp-≈ spo₂)
 
230
                                      (<-resp-≈ spo₁)
 
231
                                      (<-resp-≈ spo₂)
203
232
      }
204
233
    where open IsStrictPartialOrder
205
234
 
206
235
  _×-isStrictTotalOrder_ :
207
 
    ∀ {≈₁ <₁} → IsStrictTotalOrder ≈₁ <₁ →
208
 
    ∀ {≈₂ <₂} → IsStrictTotalOrder ≈₂ <₂ →
209
 
    IsStrictTotalOrder (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ <₁ <₂)
210
 
  _×-isStrictTotalOrder_ {<₁ = <₁} spo₁ {<₂ = <₂} spo₂ =
 
236
    ∀ {_≈₁_ _<₁_} → IsStrictTotalOrder _≈₁_ _<₁_ →
 
237
    ∀ {_≈₂_ _<₂_} → IsStrictTotalOrder _≈₂_ _<₂_ →
 
238
    IsStrictTotalOrder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_)
 
239
  _×-isStrictTotalOrder_ {_<₁_ = _<₁_} spo₁ {_<₂_ = _<₂_} spo₂ =
211
240
    record
212
241
      { isEquivalence = Pointwise._×-isEquivalence_
213
242
                          (isEquivalence spo₁) (isEquivalence spo₂)
214
243
      ; trans         = λ {x y z} →
215
244
                        ×-transitive
216
 
                          {<₁ = <₁} (isEquivalence spo₁) (<-resp-≈ spo₁)
217
 
                                    (trans spo₁)
218
 
                          {≤₂ = <₂} (trans spo₂) {x} {y} {z}
 
245
                          {_<₁_ = _<₁_} (isEquivalence spo₁)
 
246
                                        (<-resp-≈ spo₁) (trans spo₁)
 
247
                          {_≤₂_ = _<₂_} (trans spo₂) {x} {y} {z}
219
248
      ; compare       = ×-compare (Eq.sym spo₁) (compare spo₁)
220
249
                                                (compare spo₂)
221
250
      ; <-resp-≈      = ×-≈-respects₂ (isEquivalence spo₁)
228
257
 
229
258
-- "Packages" (e.g. preorders) can also be combined.
230
259
 
231
 
_×-preorder_ : Preorder _ _ _ → Preorder _ _ _ → Preorder _ _ _
 
260
_×-preorder_ :
 
261
  ∀ {p₁ p₂ p₃ p₄} →
 
262
  Preorder p₁ p₂ _ → Preorder p₃ p₄ _ → Preorder _ _ _
232
263
p₁ ×-preorder p₂ = record
233
264
  { isPreorder = isPreorder p₁ ×-isPreorder isPreorder p₂
234
265
  } where open Preorder
235
266
 
236
267
_×-strictPartialOrder_ :
237
 
  StrictPartialOrder _ _ _ → StrictPartialOrder _ _ _ →
 
268
  ∀ {s₁ s₂ s₃ s₄} →
 
269
  StrictPartialOrder s₁ s₂ _ → StrictPartialOrder s₃ s₄ _ →
238
270
  StrictPartialOrder _ _ _
239
271
s₁ ×-strictPartialOrder s₂ = record
240
272
  { isStrictPartialOrder = isStrictPartialOrder s₁
243
275
  } where open StrictPartialOrder
244
276
 
245
277
_×-strictTotalOrder_ :
246
 
  StrictTotalOrder _ _ _ → StrictTotalOrder _ _ _ →
 
278
  ∀ {s₁ s₂ s₃ s₄} →
 
279
  StrictTotalOrder s₁ s₂ _ → StrictTotalOrder s₃ s₄ _ →
247
280
  StrictTotalOrder _ _ _
248
281
s₁ ×-strictTotalOrder s₂ = record
249
282
  { isStrictTotalOrder = isStrictTotalOrder s₁