\begin{code} {-# OPTIONS --safe --cubical #-} open import Container module Container.Membership {s p} (𝒞 : Container s p) where open import Prelude open import HLevels infixr 5 _∈_ _∈!_ _∈_ : 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>