------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed unary relations
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Unary.Indexed where
open import Data.Product.Base using (∃; _×_)
open import Level using (Level)
open import Relation.Nullary.Negation.Core using (¬_)
IPred : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _
IPred A ℓ = ∀ {i} → A i → Set ℓ
module _ {i a} {I : Set i} {A : I → Set a} where
infix 4 _∈_ _∉_
_∈_ : ∀ {ℓ} → (∀ i → A i) → IPred A ℓ → Set _
x ∈ P = ∀ i → P (x i)
_∉_ : ∀ {ℓ} → (∀ i → A i) → IPred A ℓ → Set _
t ∉ P = ¬ (t ∈ 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