[Agda] : vs. ∶

[Nils Anders Danielsson]

On 2012-11-29 02:30, Wolfram Kahl wrote:
> (As far as I know, ``syntax'' is only automatically imported with the
>   underlying identifier, and cannot be named in import lists?)

That's right.

> How can I rename or hide this syntax while still importing Σ ?

I guess you could do something awkward like in the following (untested)
code:

   module _ where

     open import Data.Product hiding (Σ)

     Σ : ...
     Σ = Data.Product.Σ

I almost never use this syntax, so if people don't like it I'm happy to
remove it. I guess I could also introduce a synonym for Σ, and attach
the syntax to this synonym.

-- 
/NAD