------------------------------------------------------------------------
-- 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.Definitions where
open import Data.Product.Base using (_×_)
open import Level using (Level)
open import Relation.Binary.Core using (_⇒_)
import Relation.Binary.Definitions as B
using (Reflexive; Symmetric; Transitive; Antisymmetric; Decidable)
open import Relation.Binary.Indexed.Homogeneous.Core using (IRel)
open import Relation.Unary.Indexed using (IPred)
private
variable
i a ℓ ℓ₁ ℓ₂ : Level
I : Set i
------------------------------------------------------------------------
-- Definitions
module _ (A : I → Set a) where
syntax Implies A _∼₁_ _∼₂_ = _∼₁_ ⇒[ A ] _∼₂_
Implies : IRel A ℓ₁ → IRel A ℓ₂ → Set _
Implies _∼₁_ _∼₂_ = ∀ {i} → _∼₁_ ⇒ (_∼₂_ {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 _∼_)
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