Merge tag 'upstream/0.17'

Upstream version 0.17

# gpg: Signature made Fri 23 Nov 2018 05:29:18 PM MST
# gpg:                using RSA key 9B917007AE030E36E4FC248B695B7AE4BF066240
# gpg:                issuer "spwhitton@spwhitton.name"
# gpg: Good signature from "Sean Whitton <spwhitton@spwhitton.name>" [ultimate]
# Primary key fingerprint: 8DC2 487E 51AB DD90 B5C4  753F 0F56 D055 3B6D 411B
#      Subkey fingerprint: 9B91 7007 AE03 0E36 E4FC  248B 695B 7AE4 BF06 6240

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)