[Agda] Re: Forall and product

[N. Raghavendra]

At 2015-02-18T12:03:28+01:00, Andreas Abel wrote:

> My verbalization is
>
>   Pi    : "dependent function type"
>   Sigma : "dependent pair type"
>
> which is non-ambiguous.  I also avoid "dependent product".

That seems good.  Also, does it make sense to think of Pi or dependent
function type when we look at something like (∀ x -> foo), and to think
of Sigma or dependent pair type when we look at (∃ λ y -> bar)?

Cheers,
Raghu.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/