diff options
Diffstat (limited to 'src/Relation/Binary/Indexed/Heterogeneous')
3 files changed, 170 insertions, 0 deletions
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) |