------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed binary relations
------------------------------------------------------------------------
-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Heterogeneous`.
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Indexed.Heterogeneous.Core
module Relation.Binary.Indexed.Heterogeneous.Structures
{i a ℓ} {I : Set i} (A : I → Set a) (_≈_ : IRel A ℓ)
where
open import Function.Base using (id; _⟨_⟩_)
open import Level using (suc; _⊔_)
open import Relation.Binary.Core using (_⇒_)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
open import Relation.Binary.Indexed.Heterogeneous.Definitions
using (Reflexive; Symmetric; Transitive)
------------------------------------------------------------------------
-- Equivalences
record IsIndexedEquivalence : Set (i ⊔ a ⊔ ℓ) where
field
refl : Reflexive A _≈_
sym : Symmetric A _≈_
trans : Transitive A _≈_
reflexive : ∀ {i} → _≡_ ⟨ _⇒_ ⟩ _≈_ {i}
reflexive ≡.refl = refl
record IsIndexedPreorder {ℓ₂} (_≲_ : IRel A ℓ₂) : Set (i ⊔ a ⊔ ℓ ⊔ ℓ₂) where
field
isEquivalence : IsIndexedEquivalence
reflexive : ∀ {i j} → (_≈_ {i} {j}) ⟨ _⇒_ ⟩ _≲_
trans : Transitive A _≲_
module Eq = IsIndexedEquivalence isEquivalence
refl : Reflexive A _≲_
refl = reflexive Eq.refl
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