diff options
Diffstat (limited to 'src/Relation/Binary/Indexed')
| -rw-r--r-- | src/Relation/Binary/Indexed/Core.agda | 69 | ||||
| -rw-r--r-- | src/Relation/Binary/Indexed/Heterogeneous.agda | 95 | ||||
| -rw-r--r-- | src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda | 66 | ||||
| -rw-r--r-- | src/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.agda | 56 | ||||
| -rw-r--r-- | src/Relation/Binary/Indexed/Heterogeneous/Core.agda | 48 | ||||
| -rw-r--r-- | src/Relation/Binary/Indexed/Homogeneous.agda | 253 | ||||
| -rw-r--r-- | src/Relation/Binary/Indexed/Homogeneous/Core.agda | 88 |
7 files changed, 606 insertions, 69 deletions
diff --git a/src/Relation/Binary/Indexed/Core.agda b/src/Relation/Binary/Indexed/Core.agda deleted file mode 100644 index c6f1332..0000000 --- a/src/Relation/Binary/Indexed/Core.agda +++ /dev/null @@ -1,69 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- Indexed binary relations ------------------------------------------------------------------------- - --- This file contains some core definitions which are reexported by --- Relation.Binary.Indexed. - -module Relation.Binary.Indexed.Core where - -open import Function -open import Level -import Relation.Binary.Core as B -import Relation.Binary.Core as P - ------------------------------------------------------------------------- --- Indexed binary relations - --- Heterogeneous. - -REL : ∀ {i₁ i₂ a₁ a₂} {I₁ : Set i₁} {I₂ : Set i₂} → - (I₁ → Set a₁) → (I₂ → Set a₂) → (ℓ : Level) → Set _ -REL A₁ A₂ ℓ = ∀ {i₁ i₂} → A₁ i₁ → A₂ i₂ → Set ℓ - --- Homogeneous. - -Rel : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _ -Rel A ℓ = REL A A ℓ - ------------------------------------------------------------------------- --- Simple properties of indexed binary relations - --- Reflexivity. - -Reflexive : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → Rel A ℓ → Set _ -Reflexive _ _∼_ = ∀ {i} → B.Reflexive (_∼_ {i}) - --- Symmetry. - -Symmetric : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → Rel A ℓ → Set _ -Symmetric _ _∼_ = ∀ {i j} → B.Sym (_∼_ {i} {j}) _∼_ - --- Transitivity. - -Transitive : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → Rel A ℓ → Set _ -Transitive _ _∼_ = ∀ {i j k} → B.Trans _∼_ (_∼_ {j}) (_∼_ {i} {k}) - ------------------------------------------------------------------------- --- Setoids - -record IsEquivalence {i a ℓ} {I : Set i} (A : I → Set a) - (_≈_ : Rel A ℓ) : Set (i ⊔ a ⊔ ℓ) where - field - refl : Reflexive A _≈_ - sym : Symmetric A _≈_ - trans : Transitive A _≈_ - - reflexive : ∀ {i} → P._≡_ ⟨ B._⇒_ ⟩ _≈_ {i} - reflexive P.refl = refl - -record Setoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where - infix 4 _≈_ - field - Carrier : I → Set c - _≈_ : Rel Carrier ℓ - isEquivalence : IsEquivalence Carrier _≈_ - - open IsEquivalence isEquivalence public diff --git a/src/Relation/Binary/Indexed/Heterogeneous.agda b/src/Relation/Binary/Indexed/Heterogeneous.agda new file mode 100644 index 0000000..4e8d0cc --- /dev/null +++ b/src/Relation/Binary/Indexed/Heterogeneous.agda @@ -0,0 +1,95 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Indexed binary relations +------------------------------------------------------------------------ + +module Relation.Binary.Indexed.Heterogeneous where + +open import Function +open import Level using (suc; _⊔_) +open import Relation.Binary using (_⇒_) +open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) + +------------------------------------------------------------------------ +-- Publically export core definitions + +open import Relation.Binary.Indexed.Heterogeneous.Core 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 +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 0.17 + +REL = IREL +{-# WARNING_ON_USAGE REL +"Warning: REL was deprecated in v0.17. +Please use IREL instead." +#-} +Rel = IRel +{-# WARNING_ON_USAGE Rel +"Warning: Rel was deprecated in v0.17. +Please use IRel instead." +#-} +Setoid = IndexedSetoid +{-# WARNING_ON_USAGE Setoid +"Warning: Setoid was deprecated in v0.17. +Please use IndexedSetoid instead." +#-} +IsEquivalence = IsIndexedEquivalence +{-# WARNING_ON_USAGE IsEquivalence +"Warning: IsEquivalence was deprecated in v0.17. +Please use IsIndexedEquivalence instead." +#-} diff --git a/src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda b/src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda new file mode 100644 index 0000000..dc71b48 --- /dev/null +++ b/src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda @@ -0,0 +1,66 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Instantiates indexed binary structures at an index to the equivalent +-- non-indexed structures. +------------------------------------------------------------------------ + +module Relation.Binary.Indexed.Heterogeneous.Construct.At where + +open import Relation.Binary +open import Relation.Binary.Indexed.Heterogeneous + hiding (IsEquivalence; Setoid) + +------------------------------------------------------------------------ +-- Structures + +module _ {a i} {I : Set i} {A : I → Set a} where + + isEquivalence : ∀ {ℓ} {_≈_ : IRel A ℓ} → IsIndexedEquivalence A _≈_ → + (index : I) → IsEquivalence (_≈_ {index}) + isEquivalence isEq index = record + { refl = refl + ; sym = sym + ; trans = trans + } + where open IsIndexedEquivalence isEq + + isPreorder : ∀ {ℓ₁ ℓ₂} {_≈_ : IRel A ℓ₁} {_∼_ : IRel A ℓ₂} → + IsIndexedPreorder A _≈_ _∼_ → + (index : I) → IsPreorder (_≈_ {index}) _∼_ + isPreorder isPreorder index = record + { isEquivalence = isEquivalence O.isEquivalence index + ; reflexive = O.reflexive + ; trans = O.trans + } + where module O = IsIndexedPreorder isPreorder + +------------------------------------------------------------------------ +-- Packages + +module _ {a i} {I : Set i} where + + setoid : ∀ {ℓ} → IndexedSetoid I a ℓ → I → Setoid a ℓ + setoid S index = record + { Carrier = S.Carrier index + ; _≈_ = S._≈_ + ; isEquivalence = isEquivalence S.isEquivalence index + } + where module S = IndexedSetoid S + + preorder : ∀ {ℓ₁ ℓ₂} → IndexedPreorder I a ℓ₁ ℓ₂ → I → Preorder a ℓ₁ ℓ₂ + preorder O index = record + { Carrier = O.Carrier index + ; _≈_ = O._≈_ + ; _∼_ = O._∼_ + ; isPreorder = isPreorder O.isPreorder index + } + where module O = IndexedPreorder O + +------------------------------------------------------------------------ +-- Some useful shorthand infix notation + +module _ {a i} {I : Set i} where + + _atₛ_ : ∀ {ℓ} → IndexedSetoid I a ℓ → I → Setoid a ℓ + _atₛ_ = setoid diff --git a/src/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.agda b/src/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.agda new file mode 100644 index 0000000..947f28e --- /dev/null +++ b/src/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.agda @@ -0,0 +1,56 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Creates trivially indexed records from their non-indexed counterpart. +------------------------------------------------------------------------ + +module Relation.Binary.Indexed.Heterogeneous.Construct.Trivial + {i} {I : Set i} where + +open import Relation.Binary +open import Relation.Binary.Indexed.Heterogeneous hiding (Rel) + hiding (IsEquivalence; Setoid) + +------------------------------------------------------------------------ +-- Structures + +module _ {a} {A : Set a} where + + private + Aᵢ : I → Set a + Aᵢ i = A + + isIndexedEquivalence : ∀ {ℓ} {_≈_ : Rel A ℓ} → IsEquivalence _≈_ → + IsIndexedEquivalence Aᵢ _≈_ + isIndexedEquivalence isEq = record + { refl = refl + ; sym = sym + ; trans = trans + } + where open IsEquivalence isEq + + isIndexedPreorder : ∀ {ℓ₁ ℓ₂} {_≈_ : Rel A ℓ₁} {_∼_ : Rel A ℓ₂} → + IsPreorder _≈_ _∼_ → + IsIndexedPreorder Aᵢ _≈_ _∼_ + isIndexedPreorder isPreorder = record + { isEquivalence = isIndexedEquivalence isEquivalence + ; reflexive = reflexive + ; trans = trans + } + where open IsPreorder isPreorder + +------------------------------------------------------------------------ +-- Packages + +indexedSetoid : ∀ {a ℓ} → Setoid a ℓ → IndexedSetoid I a ℓ +indexedSetoid S = record + { isEquivalence = isIndexedEquivalence isEquivalence + } + where open Setoid S + +indexedPreorder : ∀ {a ℓ₁ ℓ₂} → Preorder a ℓ₁ ℓ₂ → + IndexedPreorder I a ℓ₁ ℓ₂ +indexedPreorder O = record + { isPreorder = isIndexedPreorder isPreorder + } + where open Preorder O diff --git a/src/Relation/Binary/Indexed/Heterogeneous/Core.agda b/src/Relation/Binary/Indexed/Heterogeneous/Core.agda new file mode 100644 index 0000000..92c1d42 --- /dev/null +++ b/src/Relation/Binary/Indexed/Heterogeneous/Core.agda @@ -0,0 +1,48 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Indexed binary relations +------------------------------------------------------------------------ + +-- This file contains some core definitions which are re-exported by +-- Relation.Binary.Indexed.Heterogeneous. + +module Relation.Binary.Indexed.Heterogeneous.Core where + +open import Level +import Relation.Binary.Core as B +import Relation.Binary.PropositionalEquality.Core as P + +------------------------------------------------------------------------ +-- Indexed binary relations + +-- Heterogeneous types + +IREL : ∀ {i₁ i₂ a₁ a₂} {I₁ : Set i₁} {I₂ : Set i₂} → + (I₁ → Set a₁) → (I₂ → Set a₂) → (ℓ : Level) → Set _ +IREL A₁ A₂ ℓ = ∀ {i₁ i₂} → A₁ i₁ → A₂ i₂ → Set ℓ + +-- Homogeneous types + +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 _=[_]⇒_ + +_=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b} → + B.Rel A ℓ₁ → ((x : A) → B x) → IRel B ℓ₂ → Set _ +P =[ f ]⇒ Q = ∀ {i j} → P i j → Q (f i) (f j) diff --git a/src/Relation/Binary/Indexed/Homogeneous.agda b/src/Relation/Binary/Indexed/Homogeneous.agda new file mode 100644 index 0000000..fc1c545 --- /dev/null +++ b/src/Relation/Binary/Indexed/Homogeneous.agda @@ -0,0 +1,253 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Homogeneously-indexed binary relations +-- +-- Indexed structures are laid out in a similar manner as to those +-- in Relation.Binary. The main difference is each structure also +-- contains proofs for the lifted version of the relation. +------------------------------------------------------------------------ + +module Relation.Binary.Indexed.Homogeneous where + +open import Function using (_⟨_⟩_) +open import Level using (Level; _⊔_; suc) +open import Relation.Binary as B using (_⇒_) +open import Relation.Binary.PropositionalEquality as P using (_≡_) +open import Relation.Nullary using (¬_) +open import Data.Product using (_,_) + +------------------------------------------------------------------------ +-- Publically export core definitions + +open import Relation.Binary.Indexed.Homogeneous.Core 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ᵢ + + -- Lift properties + + reflexive : _≡_ ⇒ (Lift A _≈ᵢ_) + reflexive P.refl i = reflᵢ + + refl : B.Reflexive (Lift A _≈ᵢ_) + refl i = reflᵢ + + sym : B.Symmetric (Lift A _≈ᵢ_) + sym x≈y i = symᵢ (x≈y i) + + trans : B.Transitive (Lift A _≈ᵢ_) + trans x≈y y≈z i = transᵢ (x≈y i) (y≈z i) + + isEquivalence : B.IsEquivalence (Lift A _≈ᵢ_) + isEquivalence = record + { refl = refl + ; sym = sym + ; trans = trans + } + +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 + + Carrier : Set _ + Carrier = ∀ i → Carrierᵢ i + + _≈_ : B.Rel Carrier _ + _≈_ = Lift Carrierᵢ _≈ᵢ_ + + _≉_ : B.Rel Carrier _ + x ≉ y = ¬ (x ≈ y) + + setoid : B.Setoid _ _ + setoid = record + { isEquivalence = isEquivalence + } + +------------------------------------------------------------------------ +-- Decidable equivalences + +record IsIndexedDecEquivalence {i a ℓ} {I : Set i} (A : I → Set a) + (_≈ᵢ_ : IRel A ℓ) : Set (i ⊔ a ⊔ ℓ) where + infix 4 _≟ᵢ_ + field + _≟ᵢ_ : Decidable A _≈ᵢ_ + isEquivalenceᵢ : IsIndexedEquivalence A _≈ᵢ_ + + open IsIndexedEquivalence isEquivalenceᵢ public + +record IndexedDecSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where + infix 4 _≈ᵢ_ + field + Carrierᵢ : I → Set c + _≈ᵢ_ : IRel Carrierᵢ ℓ + isDecEquivalenceᵢ : IsIndexedDecEquivalence Carrierᵢ _≈ᵢ_ + + open IsIndexedDecEquivalence isDecEquivalenceᵢ public + + indexedSetoid : IndexedSetoid I c ℓ + indexedSetoid = record { isEquivalenceᵢ = isEquivalenceᵢ } + + open IndexedSetoid indexedSetoid public + using (Carrier; _≈_; _≉_; setoid) + +------------------------------------------------------------------------ +-- 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ᵢ : _≈ᵢ_ ⇒[ A ] _∼ᵢ_ + transᵢ : Transitive A _∼ᵢ_ + + module Eq = IsIndexedEquivalence isEquivalenceᵢ + + reflᵢ : Reflexive A _∼ᵢ_ + reflᵢ = reflexiveᵢ Eq.reflᵢ + + ∼ᵢ-respˡ-≈ᵢ : Respectsˡ A _∼ᵢ_ _≈ᵢ_ + ∼ᵢ-respˡ-≈ᵢ x≈y x∼z = transᵢ (reflexiveᵢ (Eq.symᵢ x≈y)) x∼z + + ∼ᵢ-respʳ-≈ᵢ : Respectsʳ A _∼ᵢ_ _≈ᵢ_ + ∼ᵢ-respʳ-≈ᵢ x≈y z∼x = transᵢ z∼x (reflexiveᵢ x≈y) + + ∼ᵢ-resp-≈ᵢ : Respects₂ A _∼ᵢ_ _≈ᵢ_ + ∼ᵢ-resp-≈ᵢ = ∼ᵢ-respʳ-≈ᵢ , ∼ᵢ-respˡ-≈ᵢ + + -- Lifted properties + + reflexive : Lift A _≈ᵢ_ B.⇒ Lift A _∼ᵢ_ + reflexive x≈y i = reflexiveᵢ (x≈y i) + + refl : B.Reflexive (Lift A _∼ᵢ_) + refl i = reflᵢ + + trans : B.Transitive (Lift A _∼ᵢ_) + trans x≈y y≈z i = transᵢ (x≈y i) (y≈z i) + + ∼-respˡ-≈ : (Lift A _∼ᵢ_) B.Respectsˡ (Lift A _≈ᵢ_) + ∼-respˡ-≈ x≈y x∼z i = ∼ᵢ-respˡ-≈ᵢ (x≈y i) (x∼z i) + + ∼-respʳ-≈ : (Lift A _∼ᵢ_) B.Respectsʳ (Lift A _≈ᵢ_) + ∼-respʳ-≈ x≈y z∼x i = ∼ᵢ-respʳ-≈ᵢ (x≈y i) (z∼x i) + + ∼-resp-≈ : (Lift A _∼ᵢ_) B.Respects₂ (Lift A _≈ᵢ_) + ∼-resp-≈ = ∼-respʳ-≈ , ∼-respˡ-≈ + + isPreorder : B.IsPreorder (Lift A _≈ᵢ_) (Lift A _∼ᵢ_) + isPreorder = record + { isEquivalence = Eq.isEquivalence + ; reflexive = reflexive + ; trans = trans + } + +record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ : + Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where + + infix 4 _≈ᵢ_ _∼ᵢ_ _≈_ _∼_ + + field + Carrierᵢ : I → Set c + _≈ᵢ_ : IRel Carrierᵢ ℓ₁ + _∼ᵢ_ : IRel Carrierᵢ ℓ₂ + isPreorderᵢ : IsIndexedPreorder Carrierᵢ _≈ᵢ_ _∼ᵢ_ + + open IsIndexedPreorder isPreorderᵢ public + + Carrier : Set _ + Carrier = ∀ i → Carrierᵢ i + + _≈_ : B.Rel Carrier _ + x ≈ y = ∀ i → x i ≈ᵢ y i + + _∼_ : B.Rel Carrier _ + x ∼ y = ∀ i → x i ∼ᵢ y i + + preorder : B.Preorder _ _ _ + preorder = record { isPreorder = isPreorder } + +------------------------------------------------------------------------ +-- Partial orders + +record IsIndexedPartialOrder {i a ℓ₁ ℓ₂} {I : Set i} (A : I → Set a) + (_≈ᵢ_ : IRel A ℓ₁) (_≤ᵢ_ : IRel A ℓ₂) : + Set (i ⊔ a ⊔ ℓ₁ ⊔ ℓ₂) where + field + isPreorderᵢ : IsIndexedPreorder A _≈ᵢ_ _≤ᵢ_ + antisymᵢ : Antisymmetric A _≈ᵢ_ _≤ᵢ_ + + open IsIndexedPreorder isPreorderᵢ public + renaming + ( ∼ᵢ-respˡ-≈ᵢ to ≤ᵢ-respˡ-≈ᵢ + ; ∼ᵢ-respʳ-≈ᵢ to ≤ᵢ-respʳ-≈ᵢ + ; ∼ᵢ-resp-≈ᵢ to ≤ᵢ-resp-≈ᵢ + ; ∼-respˡ-≈ to ≤-respˡ-≈ + ; ∼-respʳ-≈ to ≤-respʳ-≈ + ; ∼-resp-≈ to ≤-resp-≈ + ) + + antisym : B.Antisymmetric (Lift A _≈ᵢ_) (Lift A _≤ᵢ_) + antisym x≤y y≤x i = antisymᵢ (x≤y i) (y≤x i) + + isPartialOrder : B.IsPartialOrder (Lift A _≈ᵢ_) (Lift A _≤ᵢ_) + isPartialOrder = record + { isPreorder = isPreorder + ; antisym = antisym + } + +record IndexedPoset {i} (I : Set i) c ℓ₁ ℓ₂ : + Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where + field + Carrierᵢ : I → Set c + _≈ᵢ_ : IRel Carrierᵢ ℓ₁ + _≤ᵢ_ : IRel Carrierᵢ ℓ₂ + isPartialOrderᵢ : IsIndexedPartialOrder Carrierᵢ _≈ᵢ_ _≤ᵢ_ + + open IsIndexedPartialOrder isPartialOrderᵢ public + + preorderᵢ : IndexedPreorder I c ℓ₁ ℓ₂ + preorderᵢ = record { isPreorderᵢ = isPreorderᵢ } + + open IndexedPreorder preorderᵢ public + using (Carrier; _≈_; preorder) + renaming + (_∼_ to _≤_) + + poset : B.Poset _ _ _ + poset = record { isPartialOrder = isPartialOrder } + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 0.17 + +REL = IREL +{-# WARNING_ON_USAGE REL +"Warning: REL was deprecated in v0.17. +Please use IREL instead." +#-} +Rel = IRel +{-# WARNING_ON_USAGE Rel +"Warning: Rel was deprecated in v0.17. +Please use IRel instead." +#-} diff --git a/src/Relation/Binary/Indexed/Homogeneous/Core.agda b/src/Relation/Binary/Indexed/Homogeneous/Core.agda new file mode 100644 index 0000000..abb2609 --- /dev/null +++ b/src/Relation/Binary/Indexed/Homogeneous/Core.agda @@ -0,0 +1,88 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Homogeneously-indexed binary relations +------------------------------------------------------------------------ +-- This file contains some core definitions which are reexported by +-- Relation.Binary.Indexed.Homogeneous + +module Relation.Binary.Indexed.Homogeneous.Core where + +open import Level using (Level; _⊔_) +open import Data.Product using (_×_) +open import Relation.Binary as B using (REL; Rel) +open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) +import Relation.Binary.Indexed.Heterogeneous as I +open import Relation.Unary.Indexed using (IPred) + +------------------------------------------------------------------------ +-- Homegeneously indexed binary relations + +-- Heterogeneous types + +IREL : ∀ {i a b} {I : Set i} → (I → Set a) → (I → Set b) → (ℓ : Level) → Set _ +IREL A B ℓ = ∀ {i} → REL (A i) (B i) ℓ + +-- Homogeneous types + +IRel : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _ +IRel A = IREL A A + +------------------------------------------------------------------------ +-- Simple properties + +module _ {i a} {I : Set i} (A : I → Set a) where + + syntax Implies A _∼₁_ _∼₂_ = _∼₁_ ⇒[ A ] _∼₂_ + + Implies : ∀ {ℓ₁ ℓ₂} → IRel A ℓ₁ → IRel A ℓ₂ → Set _ + Implies _∼₁_ _∼₂_ = ∀ {i} → _∼₁_ B.⇒ (_∼₂_ {i}) + + Reflexive : ∀ {ℓ} → IRel A ℓ → Set _ + Reflexive _∼_ = ∀ {i} → B.Reflexive (_∼_ {i}) + + Symmetric : ∀ {ℓ} → IRel A ℓ → Set _ + Symmetric _∼_ = ∀ {i} → B.Symmetric (_∼_ {i}) + + Transitive : ∀ {ℓ} → IRel A ℓ → Set _ + Transitive _∼_ = ∀ {i} → B.Transitive (_∼_ {i}) + + Antisymmetric : ∀ {ℓ₁ ℓ₂} → IRel A ℓ₁ → IRel A ℓ₂ → Set _ + Antisymmetric _≈_ _∼_ = ∀ {i} → B.Antisymmetric _≈_ (_∼_ {i}) + + Decidable : ∀ {ℓ} → IRel A ℓ → Set _ + Decidable _∼_ = ∀ {i} → B.Decidable (_∼_ {i}) + + Respects : ∀ {ℓ₁ ℓ₂} → IPred A ℓ₁ → IRel A ℓ₂ → Set _ + Respects P _∼_ = ∀ {i} {x y : A i} → x ∼ y → P x → P y + + Respectsˡ : ∀ {ℓ₁ ℓ₂} → IRel A ℓ₁ → IRel A ℓ₂ → Set _ + Respectsˡ P _∼_ = ∀ {i} {x y z : A i} → x ∼ y → P x z → P y z + + Respectsʳ : ∀ {ℓ₁ ℓ₂} → IRel A ℓ₁ → IRel A ℓ₂ → Set _ + Respectsʳ P _∼_ = ∀ {i} {x y z : A i} → x ∼ y → P z x → P z y + + Respects₂ : ∀ {ℓ₁ ℓ₂} → IRel A ℓ₁ → IRel A ℓ₂ → Set _ + Respects₂ P _∼_ = (Respectsʳ P _∼_) × (Respectsˡ P _∼_) + +------------------------------------------------------------------------ +-- Conversion between homogeneous and heterogeneously indexed relations + +module _ {i a b} {I : Set i} {A : I → Set a} {B : I → Set b} where + + OverPath : ∀ {ℓ} → IREL A B ℓ → ∀ {i j} → i ≡ j → REL (A i) (B j) ℓ + OverPath _∼_ refl = _∼_ + + toHetIndexed : ∀ {ℓ} → IREL A B ℓ → I.IREL A B (i ⊔ ℓ) + toHetIndexed _∼_ {i} {j} x y = (p : i ≡ j) → OverPath _∼_ p x y + + fromHetIndexed : ∀ {ℓ} → I.IREL A B ℓ → IREL A B ℓ + fromHetIndexed _∼_ = _∼_ + +------------------------------------------------------------------------ +-- Lifting to non-indexed binary relations + +module _ {i a} {I : Set i} (A : I → Set a) where + + Lift : ∀ {ℓ} → IRel A ℓ → Rel (∀ i → A i) _ + Lift _∼_ x y = ∀ i → x i ∼ y i |