-- Martin Escardo 2011.

module Subset where

open import Logic

-- We implement subsets as Σ-types as usual, but we use a special
-- syntax for them:

record subset (X : Set) (A : X → Prp) : Set where
  constructor _||_
  field
   element : X
   membership-proof : A element

syntax subset X (λ x → A) =  ⁅ x ∶ X ∣ A ⁆

-- Notice that "∶" is typed as "\:1" and ∣ is typed as "\mid" and the
-- braces as "\(" followed by an option offered in the emacs
-- mini-buffer.

-- The inclusion of a subset into the ambient set amounts to the first
-- projection:

incl : {X : Set} {A : X → Prp} → ⁅ x ∶ X ∣ A x ⁆ → X
incl(x || c) = x