Re: [Agda] : vs. ∶

[Dominique Devriese]

Martin,

2012/5/4 Martin Escardo <m.escardo at cs.bham.ac.uk>:
> record Σ {X : Set} (Y : X → Set) : Set where
>  constructor _,_
>  field
>  π₀ : X
>  π₁ : Y π₀
>
> instead. So you have to write Σ {X} Y rather than Σ X Y. On the other hand,
> you can write Σ \(x : X) → Y x, or even Σ \x → Y x when X can be inferred.
> But this would break existing code that uses the libraries.

The standard library seems to call this "∃":

∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃ = Σ _

Dominique