------------------------------------------------------------------------
-- 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.Core where
open import Level using (Level; _⊔_)
open import Data.Product.Base using (_×_)
open import Relation.Binary.Core as B using (REL; Rel)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
import Relation.Binary.Indexed.Heterogeneous as I using (IREL)
open import Relation.Unary.Indexed using (IPred)
private
variable
a b c ℓ : Level
I : Set c
------------------------------------------------------------------------
-- Homegeneously indexed binary relations
-- Heterogeneous types
IREL : (I → Set a) → (I → Set b) → (ℓ : Level) → Set _
IREL A B ℓ = ∀ {i} → REL (A i) (B i) ℓ
-- Homogeneous types
IRel : (I → Set a) → (ℓ : Level) → Set _
IRel A = IREL A A
------------------------------------------------------------------------
-- Lifting to non-indexed binary relations
-- Ideally this should be in: `Construct.Lift` but we want this relation
-- to be exported by the various structures & bundles.
Lift : (A : I → Set a) → IRel A ℓ → Rel (∀ i → A i) _
Lift _ _∼_ x y = ∀ i → x i ∼ y i
------------------------------------------------------------------------
-- Conversion between homogeneous and heterogeneously indexed relations
module _ {i a b} {I : Set i} {A : I → Set a} {B : I → Set b} where
OverPath : ∀ {ℓ} → IREL A B ℓ → ∀ {i j} → i ≡ j → REL (A i) (B j) ℓ
OverPath _∼_ refl = _∼_
toHetIndexed : ∀ {ℓ} → IREL A B ℓ → I.IREL A B (i ⊔ ℓ)
toHetIndexed _∼_ {i} {j} x y = (p : i ≡ j) → OverPath _∼_ p x y
fromHetIndexed : ∀ {ℓ} → I.IREL A B ℓ → IREL A B ℓ
fromHetIndexed _∼_ = _∼_
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