\begin{code}
{-# OPTIONS --safe --cubical #-}

open import Container

module Container.Membership {s p} (𝒞 : Container s p) where

open import Prelude
open import HLevels

infixr  _∈_ _∈!_
_∈_ : A → ⟦ 𝒞 ⟧ A → Type _
\end{code}
%<*membership-def>
\begin{code}
x ∈ xs = fiber (snd xs) x
\end{code}
%</membership-def>
\begin{code}

_∈!_ : A → ⟦ 𝒞 ⟧ A → Type _
\end{code}
%<*uniq-memb-def>
\begin{code}
x ∈! xs = isContr (x ∈ xs)
\end{code}
%</uniq-memb-def>