small fixes to Sigma-types
Pi-types in basics
fixes to Pi