module existentialQuantification where


record ∃r  (A : Set) (B : A -> Set) : Set where
  field
     a : A
     b : B a

data ∃d  (A : Set) (B : A -> Set) : Set where
  exists : (a : A) -> B a -> ∃d A B