Skip to content

Commit 2bda760

Browse files
jmougeotjamesmckinna
jmougeot
and
jamesmckinna
authored
[import] Relation.Construct.*...Relation.Index.Homogeneous (#2646)
* [import] ... * Update src/Relation/Binary/Construct/Composition.agda grouping * Update src/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.agda cognate grouping --------- Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
1 parent 225215f commit 2bda760

File tree

20 files changed

+73
-48
lines changed

20 files changed

+73
-48
lines changed

‎src/Relation/Binary/Construct/Composition.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,8 @@ open import Level using (Level; _⊔_)
1414
open import Relation.Binary.Core using (Rel; REL; _⇒_)
1515
open import Relation.Binary.Structures using (IsPreorder)
1616
open import Relation.Binary.Definitions
17-
using (_Respects_; _Respectsʳ_; _Respectsˡ_; _Respects₂_; Reflexive
18-
; Transitive)
17+
using (_Respects_; _Respectsʳ_; _Respectsˡ_; _Respects₂_
18+
; Reflexive; Transitive)
1919

2020
private
2121
variable

‎src/Relation/Binary/Construct/Constant.agda‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88

99
module Relation.Binary.Construct.Constant where
1010

11-
open import Level
11+
open import Level using (Level)
1212
open import Relation.Binary.Bundles using (Setoid)
1313
open import Relation.Binary.Structures using (IsEquivalence)
1414
open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)

‎src/Relation/Binary/Construct/Intersection.agda‎

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

99
module Relation.Binary.Construct.Intersection where
1010

11-
open import Data.Product.Base
11+
open import Data.Product.Base using (_,_; _×_; map; zip; <_,_>)
1212
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
1313
open import Function.Base using (_∘_)
1414
open import Level using (Level; _⊔_)
1515
open import Relation.Binary.Core using (Rel; REL; _⇒_)
1616
open import Relation.Binary.Structures
17-
using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder; IsStrictPartialOrder)
17+
using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder
18+
; IsStrictPartialOrder)
1819
open import Relation.Binary.Definitions
19-
using (Reflexive; Symmetric; Transitive; Antisymmetric; Decidable; _Respects_; _Respectsˡ_; _Respectsʳ_; _Respects₂_; Minimum; Maximum; Irreflexive)
20+
using (Reflexive; Symmetric; Transitive; Antisymmetric; Decidable; _Respects_
21+
; _Respectsˡ_; _Respectsʳ_; _Respects₂_; Minimum; Maximum; Irreflexive)
2022
open import Relation.Nullary.Decidable using (yes; no; _×-dec_)
2123

2224
private

‎src/Relation/Binary/Construct/Never.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@
88

99
module Relation.Binary.Construct.Never where
1010

11-
open import Relation.Binary.Core
12-
open import Relation.Binary.Construct.Constant
11+
open import Relation.Binary.Core using (Rel)
12+
open import Relation.Binary.Construct.Constant using (Const)
1313
open import Data.Empty.Polymorphic using (⊥)
1414

1515
------------------------------------------------------------------------

‎src/Relation/Binary/Construct/NonStrictToStrict.agda‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,10 +7,6 @@
77
{-# OPTIONS --cubical-compatible --safe #-}
88

99
open import Relation.Binary.Core using (Rel; _⇒_)
10-
open import Relation.Binary.Structures
11-
using (IsPartialOrder; IsEquivalence; IsStrictPartialOrder; IsDecPartialOrder; IsDecStrictPartialOrder; IsTotalOrder; IsStrictTotalOrder; IsDecTotalOrder)
12-
open import Relation.Binary.Definitions
13-
using (Trichotomous; Antisymmetric; Symmetric; Total; Decidable; Irreflexive; Transitive; _Respectsʳ_; _Respectsˡ_; _Respects₂_; Trans; Asymmetric; tri≈; tri<; tri>)
1410

1511
module Relation.Binary.Construct.NonStrictToStrict
1612
{a ℓ₁ ℓ₂} {A : Set a} (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) where
@@ -19,8 +15,16 @@ open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
1915
open import Data.Sum.Base using (inj₁; inj₂)
2016
open import Function.Base using (_∘_; flip)
2117
open import Relation.Nullary using (¬_; yes; no)
22-
open import Relation.Nullary.Negation using (contradiction)
2318
open import Relation.Nullary.Decidable using (¬?; _×-dec_)
19+
open import Relation.Nullary.Negation using (contradiction)
20+
open import Relation.Binary.Structures
21+
using (IsPartialOrder; IsEquivalence; IsStrictPartialOrder; IsDecPartialOrder
22+
; IsDecStrictPartialOrder; IsTotalOrder; IsStrictTotalOrder
23+
; IsDecTotalOrder)
24+
open import Relation.Binary.Definitions
25+
using (Trichotomous; Antisymmetric; Symmetric; Total; Decidable; Irreflexive
26+
; Transitive; _Respectsʳ_; _Respectsˡ_; _Respects₂_; Trans; Asymmetric
27+
; tri≈; tri<; tri>)
2428

2529
private
2630
_≉_ : Rel A ℓ₁

‎src/Relation/Binary/Construct/On.agda‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,11 +14,15 @@ open import Induction.WellFounded using (WellFounded; Acc; acc)
1414
open import Level using (Level)
1515
open import Relation.Binary.Core using (Rel; _⇒_)
1616
open import Relation.Binary.Bundles
17-
using (Preorder; Setoid; DecSetoid; Poset; DecPoset; StrictPartialOrder; TotalOrder; DecTotalOrder; StrictTotalOrder)
17+
using (Preorder; Setoid; DecSetoid; Poset; DecPoset; StrictPartialOrder
18+
; TotalOrder; DecTotalOrder; StrictTotalOrder)
1819
open import Relation.Binary.Structures
19-
using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsStrictPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictTotalOrder)
20+
using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder
21+
; IsDecPartialOrder; IsStrictPartialOrder; IsTotalOrder
22+
; IsDecTotalOrder; IsStrictTotalOrder)
2023
open import Relation.Binary.Definitions
21-
using (Reflexive; Irreflexive; Symmetric; Transitive; Antisymmetric; Asymmetric; Decidable; Total; Trichotomous; _Respects_; _Respects₂_)
24+
using (Reflexive; Irreflexive; Symmetric; Transitive; Antisymmetric
25+
; Asymmetric; Decidable; Total; Trichotomous; _Respects_; _Respects₂_)
2226

2327
private
2428
variable

‎src/Relation/Binary/Construct/StrictToNonStrict.agda‎

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -11,21 +11,23 @@
1111
{-# OPTIONS --cubical-compatible --safe #-}
1212

1313
open import Relation.Binary.Core using (Rel; _⇒_)
14-
open import Relation.Binary.Structures
15-
using (IsEquivalence; IsPreorder; IsStrictPartialOrder; IsPartialOrder; IsStrictTotalOrder; IsTotalOrder; IsDecTotalOrder)
16-
open import Relation.Binary.Definitions
17-
using (Transitive; Symmetric; Irreflexive; Antisymmetric; Trichotomous; Decidable; Trans; Total; _Respects₂_; _Respectsʳ_; _Respectsˡ_; tri<; tri≈; tri>)
1814

1915
module Relation.Binary.Construct.StrictToNonStrict
2016
{a ℓ₁ ℓ₂} {A : Set a}
2117
(_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂)
2218
where
2319

24-
open import Data.Product.Base
25-
open import Data.Sum.Base
26-
open import Data.Empty
27-
open import Function.Base
28-
open import Relation.Binary.Consequences
20+
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
21+
open import Data.Sum.Base using (inj₁; inj₂; _⊎_; [_,_]; [_,_]′)
22+
open import Data.Empty using (⊥; ⊥-elim)
23+
open import Function.Base using (_∘_; flip; _$_)
24+
open import Relation.Binary.Consequences using (trans∧irr⇒asym)
25+
open import Relation.Binary.Structures
26+
using (IsEquivalence; IsPreorder; IsStrictPartialOrder; IsPartialOrder
27+
; IsStrictTotalOrder; IsTotalOrder; IsDecTotalOrder)
28+
open import Relation.Binary.Definitions
29+
using (Transitive; Symmetric; Irreflexive; Antisymmetric; Trichotomous; Decidable
30+
; Trans; Total; _Respects₂_; _Respectsʳ_; _Respectsˡ_; tri<; tri≈; tri>)
2931
open import Relation.Nullary.Decidable using (_⊎-dec_; yes; no)
3032

3133
------------------------------------------------------------------------

‎src/Relation/Binary/Construct/Union.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@
88

99
module Relation.Binary.Construct.Union where
1010

11-
open import Data.Product.Base
12-
open import Data.Sum.Base as Sum
11+
open import Data.Product.Base using (_,_; _×_; map; zip; <_,_>)
12+
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
1313
open import Function.Base using (_∘_)
1414
open import Level using (Level; _⊔_)
1515
open import Relation.Binary.Core using (REL; Rel; _⇒_)

‎src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda‎

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,16 +8,19 @@
88

99
module Relation.Binary.HeterogeneousEquality.Quotients.Examples where
1010

11-
open import Relation.Binary.HeterogeneousEquality.Quotients
11+
open import Data.Nat.Base using (ℕ; zero; suc;_+_)
12+
open import Data.Nat.Properties
13+
using (+-assoc; +-comm; +-identityʳ; +-cancelˡ-≡)
14+
open import Data.Product.Base using (_×_; _,_)
15+
open import Function.Base
1216
open import Level using (0ℓ)
17+
open import Relation.Binary.HeterogeneousEquality.Quotients
1318
open import Relation.Binary.Bundles using (Setoid)
1419
open import Relation.Binary.Structures using (IsEquivalence)
1520
open import Relation.Binary.HeterogeneousEquality hiding (isEquivalence)
1621
import Relation.Binary.PropositionalEquality.Core as ≡
17-
open import Data.Nat.Base
18-
open import Data.Nat.Properties
19-
open import Data.Product.Base using (_×_; _,_)
20-
open import Function.Base
22+
using (_≡_; refl; sym; cong)
23+
2124

2225
open ≅-Reasoning
2326

‎src/Relation/Binary/Indexed/Heterogeneous/Bundles.agda‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,9 @@
1212
module Relation.Binary.Indexed.Heterogeneous.Bundles where
1313

1414
open import Level using (suc; _⊔_)
15-
open import Relation.Binary.Indexed.Heterogeneous.Core
15+
open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
1616
open import Relation.Binary.Indexed.Heterogeneous.Structures
17+
using (IsIndexedEquivalence; IsIndexedPreorder)
1718

1819
------------------------------------------------------------------------
1920
-- Definitions

0 commit comments

Comments
 (0)