------------------------------------------------------------------------
-- The Agda standard library
--
-- Membership for containers
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.Container.Membership where
 
open import Level using (_⊔_)
open import Relation.Unary using (Pred)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
open import Data.Container.Core using (Container; ⟦_⟧)
open import Data.Container.Relation.Unary.Any using (◇)
 
module _ {s p} {C : Container s p} {x} {X : Set x} where
 
  infix  _∈_
  _∈_ : X → Pred (⟦ C ⟧ X) (p ⊔ x)
  x ∈ xs = ◇ C (_≡_ x) xs