------------------------------------------------------------------------
-- The Agda standard library
--
-- Homogeneously-indexed binary relations
------------------------------------------------------------------------
-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Homogeneous`.
{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Binary.Indexed.Homogeneous.Bundles where
open import Level using (suc; _⊔_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles as B using (Setoid; Preorder; Poset)
open import Relation.Binary.Indexed.Homogeneous.Core using (IRel; Lift)
open import Relation.Binary.Indexed.Homogeneous.Structures
using (IsIndexedEquivalence; IsIndexedDecEquivalence; IsIndexedPreorder
; IsIndexedPartialOrder)
open import Relation.Nullary.Negation.Core using (¬_)
-- 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.
------------------------------------------------------------------------
-- Equivalences
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
infix 4 _≉_
_≈_ : Rel Carrier _
_≈_ = Lift Carrierᵢ _≈ᵢ_
_≉_ : Rel Carrier _
x ≉ y = ¬ (x ≈ y)
setoid : B.Setoid _ _
setoid = record
{ isEquivalence = isEquivalence
}
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 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
_≈_ : Rel Carrier _
x ≈ y = ∀ i → x i ≈ᵢ y i
_∼_ : Rel Carrier _
x ∼ y = ∀ i → x i ∼ᵢ y i
preorder : B.Preorder _ _ _
preorder = record
{ isPreorder = isPreorder
}
------------------------------------------------------------------------
-- Partial orders
record IndexedPoset {i} (I : Set i) c ℓ₁ ℓ₂ :
Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈ᵢ_ _≤ᵢ_
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
}
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