------------------------------------------------------------------------
-- The Agda standard library
--
-- Instantiating homogeneously indexed bundles at a particular index
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Binary.Indexed.Homogeneous.Construct.At where
open import Level using (Level)
open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder)
open import Relation.Binary.Indexed.Homogeneous
using (IRel; IsIndexedEquivalence; IsIndexedDecEquivalence; IsIndexedPreorder
; IndexedSetoid; IndexedDecSetoid; IndexedPreorder)
open import Relation.Binary.Structures
using (IsEquivalence; IsDecEquivalence; IsPreorder)
private
variable
a i ℓ ℓ₁ ℓ₂ : Level
I : Set i
Aᵢ : I → Set a
------------------------------------------------------------------------
-- Structures
isEquivalence : ∀ {_≈_ : IRel Aᵢ ℓ} → IsIndexedEquivalence Aᵢ _≈_ →
(index : I) → IsEquivalence (_≈_ {index})
isEquivalence isEq index = record
{ refl = reflᵢ
; sym = symᵢ
; trans = transᵢ
} where open IsIndexedEquivalence isEq
isDecEquivalence : ∀ {_≈_ : IRel Aᵢ ℓ} → IsIndexedDecEquivalence Aᵢ _≈_ →
(index : I) → IsDecEquivalence (_≈_ {index})
isDecEquivalence isEq index = record
{ isEquivalence = isEquivalence E.isEquivalenceᵢ index
; _≟_ = E._≟ᵢ_
} where module E = IsIndexedDecEquivalence 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
------------------------------------------------------------------------
-- Bundles
setoid : IndexedSetoid I a ℓ → I → Setoid a ℓ
setoid S index = record
{ isEquivalence = isEquivalence S.isEquivalenceᵢ index
} where module S = IndexedSetoid S
decSetoid : IndexedDecSetoid I a ℓ → I → DecSetoid a ℓ
decSetoid S index = record
{ isDecEquivalence = isDecEquivalence DS.isDecEquivalenceᵢ index
} where module DS = IndexedDecSetoid S
preorder : IndexedPreorder I a ℓ₁ ℓ₂ → I → Preorder a ℓ₁ ℓ₂
preorder O index = record
{ isPreorder = isPreorder O.isPreorderᵢ index
} where module O = IndexedPreorder O
------------------------------------------------------------------------
-- Some useful shorthand infix notation
infixr -1 _atₛ_
_atₛ_ : ∀ {ℓ} → IndexedSetoid I a ℓ → I → Setoid a ℓ
_atₛ_ = setoid
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4