Re: [Agda] Why does Data.Product have � for the type constructor?

[Bengt Nordstrom]

Sorry, this discussion confuses me.

On my mac the symbol in question looks like a circle with a flying  
bird inside.

Either there is something wrong with my computer or there is a need  
for a lot of explanation why anyone would have bothered
to find such a strange symbol for something which we already have at  
least 4 other symbols for.

Bengt

On 10 maj 2008, at 10.21, Marcin Benke wrote:

> 2008/5/9 Samuel Bronson <naesten at gmail.com>:
>> Why does Data.Product have ㊥ for  
>> the type constructor? Wouldn't Π be
>> more appropriate? I guess that might have other connotations,
>> though... still, ㊥???
>
> Sigma x:A.B(x) is the set of proofs of the *existential* statement
> "exists x in A such that B(x)".
> As it happens, it is also a set of pairs <x,y> s.t. x in A, y in B(x),
> hence a generalisation of cartesian product
>
> Pi x:A.B(x) corresponds to the universal statement "for all x in A
> B(x) holds". It is a generalised product, i.e a set of functions.
>
> Hope this helps.
>
> -- 
> Marcin Benke
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda