Defining structures as Sigma-types, close #231
Merge branch 'master' of github.com:HoTT/book