Reorganise Relation.Binary.Indexed into the new hierarchy structure

src/Relation/Binary/Core.agda

@@ -4,8 +4,7 @@
 -- Properties of binary relations
 ------------------------------------------------------------------------
 
--- Note that all the definitions in this file are re-exported by
--- `Relation.Binary`.
+-- The contents of this module should be accessed via `Relation.Binary`.
 
 {-# OPTIONS --without-K --safe #-}
 

src/Relation/Binary/Definitions.agda

@@ -4,8 +4,7 @@
 -- Properties of binary relations
 ------------------------------------------------------------------------
 
--- Note that all the definitions in this file are re-exported by
--- `Relation.Binary`.
+-- The contents of this module should be accessed via `Relation.Binary`.
 
 {-# OPTIONS --without-K --safe #-}
 

src/Relation/Binary/Indexed/Heterogeneous.agda

@@ -1,71 +1,21 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Indexed binary relations
+-- Heterogeneously-indexed binary relations
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 module Relation.Binary.Indexed.Heterogeneous where
 
-open import Function.Core
-open import Level using (suc; _⊔_)
-open import Relation.Binary using (_⇒_)
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
-
 ------------------------------------------------------------------------
--- Publically export core definitions
+-- Publicly export core definitions
 
 open import Relation.Binary.Indexed.Heterogeneous.Core public
+open import Relation.Binary.Indexed.Heterogeneous.Definitions public
+open import Relation.Binary.Indexed.Heterogeneous.Structures public
+open import Relation.Binary.Indexed.Heterogeneous.Packages public
 
-------------------------------------------------------------------------
--- Equivalences
-
-record IsIndexedEquivalence {i a ℓ} {I : Set i} (A : I → Set a)
-                            (_≈_ : IRel A ℓ) : Set (i ⊔ a ⊔ ℓ) where
-  field
-    refl  : Reflexive  A _≈_
-    sym   : Symmetric  A _≈_
-    trans : Transitive A _≈_
-
-  reflexive : ∀ {i} → _≡_ ⟨ _⇒_ ⟩ _≈_ {i}
-  reflexive P.refl = refl
-
-record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
-  infix 4 _≈_
-  field
-    Carrier       : I → Set c
-    _≈_           : IRel Carrier ℓ
-    isEquivalence : IsIndexedEquivalence Carrier _≈_
-
-  open IsIndexedEquivalence isEquivalence public
-
-------------------------------------------------------------------------
--- Preorders
-
-record IsIndexedPreorder {i a ℓ₁ ℓ₂} {I : Set i} (A : I → Set a)
-                         (_≈_ : IRel A ℓ₁) (_∼_ : IRel A ℓ₂) :
-                         Set (i ⊔ a ⊔ ℓ₁ ⊔ ℓ₂) where
-  field
-    isEquivalence : IsIndexedEquivalence A _≈_
-    reflexive     : ∀ {i j} → (_≈_ {i} {j}) ⟨ _⇒_ ⟩ _∼_
-    trans         : Transitive A _∼_
-
-  module Eq = IsIndexedEquivalence isEquivalence
-
-  refl : Reflexive A _∼_
-  refl = reflexive Eq.refl
-
-record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ :
-                       Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where
-  infix 4 _≈_ _∼_
-  field
-    Carrier    : I → Set c
-    _≈_        : IRel Carrier ℓ₁  -- The underlying equality.
-    _∼_        : IRel Carrier ℓ₂  -- The relation.
-    isPreorder : IsIndexedPreorder Carrier _≈_ _∼_
-
-  open IsIndexedPreorder isPreorder public
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES

src/Relation/Binary/Indexed/Heterogeneous/Core.agda

@@ -4,8 +4,8 @@
 -- Indexed binary relations
 ------------------------------------------------------------------------
 
--- This file contains some core definitions which are re-exported by
--- Relation.Binary.Indexed.Heterogeneous.
+-- The contents of this module should be accessed via
+-- `Relation.Binary.Indexed.Heterogeneous`.
 
 {-# OPTIONS --without-K --safe #-}
 
@@ -31,17 +31,6 @@ IRel : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _
 IRel A ℓ = IREL A A ℓ
 
 ------------------------------------------------------------------------
--- Simple properties of indexed binary relations
-
-Reflexive : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → IRel A ℓ → Set _
-Reflexive _ _∼_ = ∀ {i} → B.Reflexive (_∼_ {i})
-
-Symmetric : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → IRel A ℓ → Set _
-Symmetric _ _∼_ = ∀ {i j} → B.Sym (_∼_ {i} {j}) _∼_
-
-Transitive : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → IRel A ℓ → Set _
-Transitive _ _∼_ = ∀ {i j k} → B.Trans _∼_ (_∼_ {j}) (_∼_ {i} {k})
-
 -- Generalised implication.
 
 infixr 4 _=[_]⇒_

src/Relation/Binary/Indexed/Heterogeneous/Definitions.agda

@@ -0,0 +1,35 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Indexed binary relations
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via
+-- `Relation.Binary.Indexed.Heterogeneous`.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.Indexed.Heterogeneous.Definitions where
+
+open import Level
+import Relation.Binary.Core as B
+import Relation.Binary.Definitions as B
+import Relation.Binary.PropositionalEquality.Core as P
+open import Relation.Binary.Indexed.Heterogeneous.Core
+
+private
+  variable
+    i a ℓ : Level
+    I : Set i
+
+------------------------------------------------------------------------
+-- Simple properties of indexed binary relations
+
+Reflexive : (A : I → Set a) → IRel A ℓ → Set _
+Reflexive _ _∼_ = ∀ {i} → B.Reflexive (_∼_ {i})
+
+Symmetric : (A : I → Set a) → IRel A ℓ → Set _
+Symmetric _ _∼_ = ∀ {i j} → B.Sym (_∼_ {i} {j}) _∼_
+
+Transitive : (A : I → Set a) → IRel A ℓ → Set _
+Transitive _ _∼_ = ∀ {i j k} → B.Trans _∼_ (_∼_ {j}) (_∼_ {i} {k})

src/Relation/Binary/Indexed/Heterogeneous/Packages.agda

@@ -0,0 +1,43 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Indexed binary relations
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via
+-- `Relation.Binary.Indexed.Heterogeneous`.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.Indexed.Heterogeneous.Packages where
+
+open import Function.Core
+open import Level using (suc; _⊔_)
+open import Relation.Binary using (_⇒_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.Indexed.Heterogeneous.Core
+open import Relation.Binary.Indexed.Heterogeneous.Structures
+
+------------------------------------------------------------------------
+-- Definitions
+
+record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
+  infix 4 _≈_
+  field
+    Carrier       : I → Set c
+    _≈_           : IRel Carrier ℓ
+    isEquivalence : IsIndexedEquivalence Carrier _≈_
+
+  open IsIndexedEquivalence isEquivalence public
+
+
+record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ :
+                       Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _∼_
+  field
+    Carrier    : I → Set c
+    _≈_        : IRel Carrier ℓ₁  -- The underlying equality.
+    _∼_        : IRel Carrier ℓ₂  -- The relation.
+    isPreorder : IsIndexedPreorder Carrier _≈_ _∼_
+
+  open IsIndexedPreorder isPreorder public

src/Relation/Binary/Indexed/Heterogeneous/Structures.agda

@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Indexed binary relations
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via
+-- `Relation.Binary.Indexed.Heterogeneous`.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Indexed.Heterogeneous.Core
+
+module Relation.Binary.Indexed.Heterogeneous.Structures
+  {i a ℓ} {I : Set i} (A : I → Set a) (_≈_ : IRel A ℓ)
+  where
+
+open import Function.Core
+open import Level using (suc; _⊔_)
+open import Relation.Binary using (_⇒_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.Indexed.Heterogeneous.Definitions
+
+------------------------------------------------------------------------
+-- Equivalences
+
+record IsIndexedEquivalence : Set (i ⊔ a ⊔ ℓ) where
+  field
+    refl  : Reflexive  A _≈_
+    sym   : Symmetric  A _≈_
+    trans : Transitive A _≈_
+
+  reflexive : ∀ {i} → _≡_ ⟨ _⇒_ ⟩ _≈_ {i}
+  reflexive P.refl = refl
+
+
+record IsIndexedPreorder {ℓ₂} (_∼_ : IRel A ℓ₂) : Set (i ⊔ a ⊔ ℓ ⊔ ℓ₂) where
+  field
+    isEquivalence : IsIndexedEquivalence
+    reflexive     : ∀ {i j} → (_≈_ {i} {j}) ⟨ _⇒_ ⟩ _∼_
+    trans         : Transitive A _∼_
+
+  module Eq = IsIndexedEquivalence isEquivalence
+
+  refl : Reflexive A _∼_
+  refl = reflexive Eq.refl