Skip to content

Commit 5aeafad

Browse files
jmougeotjmougeot
authored
[Import] (#2645)
1 parent dfde0ac commit 5aeafad

File tree

21 files changed

+144
-96
lines changed

21 files changed

+144
-96
lines changed

‎src/Relation/Binary/Construct/Add/Extrema/Equality.agda‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -10,15 +10,15 @@
1010
-- Relation.Nullary.Construct.Add.Extrema
1111

1212
open import Relation.Binary.Core using (Rel)
13-
open import Relation.Binary.Structures
14-
using (IsEquivalence; IsDecEquivalence)
15-
open import Relation.Binary.Definitions
16-
using (Reflexive; Symmetric; Transitive; Decidable; Irrelevant; Substitutive)
1713

1814
module Relation.Binary.Construct.Add.Extrema.Equality
1915
{a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where
2016

2117
open import Function.Base using (_∘′_)
18+
open import Relation.Binary.Structures
19+
using (IsEquivalence; IsDecEquivalence)
20+
open import Relation.Binary.Definitions
21+
using (Reflexive; Symmetric; Transitive; Decidable; Irrelevant; Substitutive)
2222
import Relation.Binary.Construct.Add.Infimum.Equality as AddInfimum
2323
import Relation.Binary.Construct.Add.Supremum.Equality as AddSupremum
2424
open import Relation.Nullary.Construct.Add.Extrema

‎src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -10,17 +10,19 @@
1010
-- Relation.Nullary.Construct.Add.Extrema
1111

1212
open import Relation.Binary.Core using (Rel; _⇒_)
13-
open import Relation.Binary.Structures
14-
using (IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder; IsDecTotalOrder)
15-
open import Relation.Binary.Definitions
16-
using (Decidable; Transitive; Minimum; Maximum; Total; Irrelevant; Antisymmetric)
1713

1814
module Relation.Binary.Construct.Add.Extrema.NonStrict
1915
{a ℓ} {A : Set a} (_≤_ : Rel A ℓ) where
2016

2117
open import Function.Base
22-
open import Relation.Nullary.Construct.Add.Extrema
23-
import Relation.Nullary.Construct.Add.Infimum as I
18+
open import Relation.Binary.Structures
19+
using (IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder
20+
; IsDecTotalOrder)
21+
open import Relation.Binary.Definitions
22+
using (Decidable; Transitive; Minimum; Maximum; Total; Irrelevant
23+
; Antisymmetric)
24+
open import Relation.Nullary.Construct.Add.Extrema using (⊥±; ⊤±; [_])
25+
import Relation.Nullary.Construct.Add.Infimum as I using (⊥₋; [_])
2426
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
2527
import Relation.Binary.Construct.Add.Infimum.NonStrict as AddInfimum
2628
import Relation.Binary.Construct.Add.Supremum.NonStrict as AddSupremum

‎src/Relation/Binary/Construct/Add/Extrema/Strict.agda‎

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -16,17 +16,16 @@ module Relation.Binary.Construct.Add.Extrema.Strict
1616

1717
open import Level
1818
open import Function.Base using (_∘′_)
19-
20-
import Relation.Nullary.Construct.Add.Infimum as I
21-
open import Relation.Nullary.Construct.Add.Extrema
22-
open import Relation.Binary.PropositionalEquality.Core
23-
using (_≡_; refl)
19+
import Relation.Nullary.Construct.Add.Infimum as I using (⊥₋; [_])
20+
open import Relation.Nullary.Construct.Add.Extrema using (⊥±; ⊤±; [_])
21+
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
2422
import Relation.Binary.Construct.Add.Infimum.Strict as AddInfimum
2523
import Relation.Binary.Construct.Add.Supremum.Strict as AddSupremum
2624
import Relation.Binary.Construct.Add.Extrema.Equality as Equality
2725
import Relation.Binary.Construct.Add.Extrema.NonStrict as NonStrict
2826
open import Relation.Binary.Definitions
29-
using (Asymmetric; Transitive; Decidable; Irrelevant; Trichotomous; Irreflexive; Trans; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
27+
using (Asymmetric; Transitive; Decidable; Irrelevant; Trichotomous
28+
; Irreflexive; Trans; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
3029
open import Relation.Binary.Structures
3130
using (IsStrictPartialOrder; IsDecStrictPartialOrder; IsStrictTotalOrder)
3231

‎src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda‎

Lines changed: 12 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -10,22 +10,27 @@
1010
-- Relation.Nullary.Construct.Add.Infimum
1111

1212
open import Relation.Binary.Core using (Rel; _⇒_)
13-
open import Relation.Binary.Structures
14-
using (IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder; IsDecTotalOrder)
15-
open import Relation.Binary.Definitions
16-
using (Minimum; Transitive; Total; Decidable; Irrelevant; Antisymmetric)
13+
1714

1815
module Relation.Binary.Construct.Add.Infimum.NonStrict
1916
{a ℓ} {A : Set a} (_≤_ : Rel A ℓ) where
2017

2118
open import Level using (_⊔_)
22-
open import Data.Sum.Base as Sum
19+
open import Data.Sum.Base as Sum using (inj₁; inj₂)
2320
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
2421
import Relation.Binary.PropositionalEquality.Properties as ≡
22+
using (isEquivalence)
2523
import Relation.Binary.Construct.Add.Infimum.Equality as Equality
24+
using (_≈₋_; ⊥₋≈⊥₋; ≈₋-isEquivalence; ≈₋-isDecEquivalence; ≈₋-refl; ≈₋-dec
25+
; [_])
26+
open import Relation.Binary.Structures
27+
using (IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder
28+
; IsDecTotalOrder)
29+
open import Relation.Binary.Definitions
30+
using (Minimum; Transitive; Total; Decidable; Irrelevant; Antisymmetric)
2631
open import Relation.Nullary hiding (Irrelevant)
27-
open import Relation.Nullary.Construct.Add.Infimum
28-
import Relation.Nullary.Decidable as Dec
32+
open import Relation.Nullary.Construct.Add.Infimum using (⊥₋; [_]; _₋; ≡-dec)
33+
import Relation.Nullary.Decidable.Core as Dec using (map′)
2934

3035
------------------------------------------------------------------------
3136
-- Definition

‎src/Relation/Binary/Construct/Add/Infimum/Strict.agda‎

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -10,24 +10,30 @@
1010
-- Relation.Nullary.Construct.Add.Infimum
1111

1212
open import Relation.Binary.Core using (Rel)
13-
open import Relation.Binary.Structures
14-
using (IsStrictPartialOrder; IsDecStrictPartialOrder; IsStrictTotalOrder)
15-
open import Relation.Binary.Definitions
16-
using (Asymmetric; Transitive; Decidable; Irrelevant; Irreflexive; Trans; Trichotomous; tri≈; tri<; tri>; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
1713

1814
module Relation.Binary.Construct.Add.Infimum.Strict
1915
{a ℓ} {A : Set a} (_<_ : Rel A ℓ) where
2016

2117
open import Level using (_⊔_)
2218
open import Data.Product.Base using (_,_; map)
23-
open import Function.Base
24-
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; subst)
19+
open import Function.Base using (_∘_)
20+
open import Relation.Binary.PropositionalEquality.Core
21+
using (_≡_; refl; cong; subst)
2522
import Relation.Binary.PropositionalEquality.Properties as ≡
23+
using (isEquivalence)
2624
import Relation.Binary.Construct.Add.Infimum.Equality as Equality
25+
using (_≈₋_; ⊥₋≈⊥₋; ≈₋-isEquivalence; ≈₋-isDecEquivalence; ≈₋-refl; ≈₋-dec
26+
; [_]; [≈]-injective)
2727
import Relation.Binary.Construct.Add.Infimum.NonStrict as NonStrict
28+
open import Relation.Binary.Structures
29+
using (IsStrictPartialOrder; IsDecStrictPartialOrder; IsStrictTotalOrder)
30+
open import Relation.Binary.Definitions
31+
using (Asymmetric; Transitive; Decidable; Irrelevant; Irreflexive; Trans
32+
; Trichotomous; tri≈; tri<; tri>; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
2833
open import Relation.Nullary hiding (Irrelevant)
2934
open import Relation.Nullary.Construct.Add.Infimum
30-
import Relation.Nullary.Decidable as Dec
35+
using (⊥₋; [_]; _₋; ≡-dec; []-injective)
36+
import Relation.Nullary.Decidable.Core as Dec using (map′)
3137

3238
------------------------------------------------------------------------
3339
-- Definition

‎src/Relation/Binary/Construct/Add/Point/Equality.agda‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -10,20 +10,20 @@
1010
-- Relation.Nullary.Construct.Add.Point
1111

1212
open import Relation.Binary.Core using (Rel)
13-
open import Relation.Binary.Structures
14-
using (IsEquivalence; IsDecEquivalence)
15-
open import Relation.Binary.Definitions
16-
using (Reflexive; Symmetric; Transitive; Decidable; Irrelevant; Substitutive)
1713

1814
module Relation.Binary.Construct.Add.Point.Equality
1915
{a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where
2016

2117
open import Level using (_⊔_)
22-
open import Function.Base
18+
open import Function.Base using (id; _∘_; _∘′_)
2319
import Relation.Binary.PropositionalEquality.Core as ≡
24-
open import Relation.Nullary hiding (Irrelevant)
25-
open import Relation.Nullary.Construct.Add.Point
26-
import Relation.Nullary.Decidable as Dec
20+
open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence)
21+
open import Relation.Binary.Definitions
22+
using (Reflexive; Symmetric; Transitive; Decidable; Irrelevant; Substitutive)
23+
open import Relation.Nullary.Negation.Core using (¬_)
24+
open import Relation.Nullary.Decidable.Core using (yes; no)
25+
open import Relation.Nullary.Construct.Add.Point as Point using (Pointed; ∙ ;[_])
26+
import Relation.Nullary.Decidable.Core as Dec using (map′)
2727

2828
------------------------------------------------------------------------
2929
-- Definition

‎src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda‎

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -10,22 +10,23 @@
1010
-- Relation.Nullary.Construct.Add.Supremum
1111

1212
open import Relation.Binary.Core using (Rel; _⇒_)
13-
open import Relation.Binary.Structures
14-
using (IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder; IsDecTotalOrder)
15-
open import Relation.Binary.Definitions
16-
using (Maximum; Transitive; Total; Decidable; Irrelevant; Antisymmetric)
1713

1814
module Relation.Binary.Construct.Add.Supremum.NonStrict
1915
{a ℓ} {A : Set a} (_≤_ : Rel A ℓ) where
2016

2117
open import Level using (_⊔_)
2218
open import Data.Sum.Base as Sum
23-
open import Relation.Nullary hiding (Irrelevant)
24-
import Relation.Nullary.Decidable as Dec
19+
open import Relation.Binary.Structures
20+
using (IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder; IsDecTotalOrder)
21+
open import Relation.Binary.Definitions
22+
using (Maximum; Transitive; Total; Decidable; Irrelevant; Antisymmetric)
23+
import Relation.Nullary.Decidable.Core as Dec using (map′)
2524
open import Relation.Binary.PropositionalEquality.Core
2625
using (_≡_; refl; cong)
2726
import Relation.Binary.PropositionalEquality.Properties as ≡
28-
open import Relation.Nullary.Construct.Add.Supremum
27+
open import Relation.Nullary.Negation.Core using (¬_)
28+
open import Relation.Nullary.Decidable.Core using (yes; no)
29+
open import Relation.Nullary.Construct.Add.Supremum using (⊤⁺; _⁺; [_]; ≡-dec)
2930
import Relation.Binary.Construct.Add.Supremum.Equality as Equality
3031

3132
------------------------------------------------------------------------

‎src/Relation/Binary/Construct/Add/Supremum/Strict.agda‎

Lines changed: 15 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -10,24 +10,28 @@
1010
-- Relation.Nullary.Construct.Add.Supremum
1111

1212
open import Relation.Binary.Core using (Rel)
13-
open import Relation.Binary.Structures
14-
using (IsStrictPartialOrder; IsDecStrictPartialOrder; IsStrictTotalOrder)
15-
open import Relation.Binary.Definitions
16-
using (Asymmetric; Transitive; Decidable; Irrelevant; Irreflexive; Trans; Trichotomous; tri≈; tri>; tri<; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
1713

1814
module Relation.Binary.Construct.Add.Supremum.Strict
1915
{a r} {A : Set a} (_<_ : Rel A r) where
2016

21-
open import Level using (_⊔_)
2217
open import Data.Product.Base using (_,_; map)
23-
open import Function.Base
24-
open import Relation.Nullary hiding (Irrelevant)
25-
import Relation.Nullary.Decidable as Dec
26-
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; subst)
27-
import Relation.Binary.PropositionalEquality.Properties as ≡
18+
open import Function.Base using (_∘_)
19+
open import Level using (_⊔_)
20+
open import Relation.Binary.Definitions
21+
using (Asymmetric; Transitive; Decidable; Irrelevant; Irreflexive; Trans
22+
; Trichotomous; tri≈; tri>; tri<; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
2823
open import Relation.Nullary.Construct.Add.Supremum
24+
using (⊤⁺; _⁺; [_]; ≡-dec; []-injective)
2925
import Relation.Binary.Construct.Add.Supremum.Equality as Equality
26+
using (_≈⁺_; ⊤⁺≈⊤⁺; ≈⁺-isEquivalence; ≈⁺-dec; [≈]-injective; [_])
3027
import Relation.Binary.Construct.Add.Supremum.NonStrict as NonStrict
28+
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; subst)
29+
import Relation.Binary.PropositionalEquality.Properties as ≡
30+
open import Relation.Binary.Structures
31+
using (IsStrictPartialOrder; IsDecStrictPartialOrder; IsStrictTotalOrder)
32+
open import Relation.Nullary.Negation.Core using (¬_)
33+
open import Relation.Nullary.Decidable.Core using (yes; no)
34+
import Relation.Nullary.Decidable as Dec using (map′)
3135

3236
------------------------------------------------------------------------
3337
-- Definition
@@ -187,3 +191,4 @@ module _ {e} {_≈_ : Rel A e} where
187191
{ isStrictPartialOrder = <⁺-isStrictPartialOrder isStrictPartialOrder
188192
; compare = <⁺-cmp compare
189193
} where open IsStrictTotalOrder strictot
194+

‎src/Relation/Binary/Construct/Closure/Equivalence/Properties.agda‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,11 @@ module Relation.Binary.Construct.Closure.Equivalence.Properties where
1111
open import Function.Base using (_∘′_)
1212
open import Relation.Binary.Core using (Rel)
1313
open import Relation.Binary.Construct.Closure.Equivalence
14+
using (EqClosure; symmetric)
1415
open import Relation.Binary.Construct.Closure.ReflexiveTransitive as RTrans
16+
using (Star; _◅◅_)
1517
import Relation.Binary.Construct.Closure.Symmetric as SymClosure
18+
using (SymClosure; fwd)
1619

1720
module _ {a ℓ} {A : Set a} {_⟶_ : Rel A ℓ} where
1821

‎src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda‎

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,17 +8,22 @@
88

99
module Relation.Binary.Construct.Closure.Reflexive.Properties where
1010

11-
open import Data.Product.Base as Product
12-
open import Data.Sum.Base as Sum
11+
open import Data.Product.Base as Product using (_,_; map)
12+
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
1313
open import Function.Bundles using (_⇔_; mk⇔)
1414
open import Function.Base using (id)
15-
open import Level
15+
open import Level using (Level; _⊔_)
1616
open import Relation.Binary.Core using (Rel; REL; _=[_]⇒_)
1717
open import Relation.Binary.Structures
18-
using (IsPreorder; IsStrictPartialOrder; IsPartialOrder; IsDecStrictPartialOrder; IsDecPartialOrder; IsStrictTotalOrder; IsTotalOrder; IsDecTotalOrder)
18+
using (IsPreorder; IsStrictPartialOrder; IsPartialOrder
19+
; IsDecStrictPartialOrder; IsDecPartialOrder; IsStrictTotalOrder
20+
; IsTotalOrder; IsDecTotalOrder)
1921
open import Relation.Binary.Definitions
20-
using (Symmetric; Transitive; Reflexive; Asymmetric; Antisymmetric; Trichotomous; Total; Decidable; DecidableEquality; tri<; tri≈; tri>; _Respectsˡ_; _Respectsʳ_; _Respects_; _Respects₂_)
22+
using (Symmetric; Transitive; Reflexive; Asymmetric; Antisymmetric
23+
; Trichotomous; Total; Decidable; DecidableEquality; tri<; tri≈; tri>
24+
; _Respectsˡ_; _Respectsʳ_; _Respects_; _Respects₂_)
2125
open import Relation.Binary.Construct.Closure.Reflexive
26+
using (ReflClosure; [_]; refl)
2227
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
2328
import Relation.Binary.PropositionalEquality.Properties as ≡
2429
open import Relation.Nullary.Negation.Core using (contradiction)

0 commit comments

Comments
 (0)