made the first argument of Sigma type implicit
fixed the pointed universe type
Merge made Sigma type simpler