`total-space`: pointfree notation for total space of dependent type

[TashiWalde]

1) add pointfree notation for total types of dependent families 2) move definitions of slice and coslice to earlier file

[emilyriehl]

This seems good to me. I think it's useful to have this optional notation without enforcing its use.

I imagine in cases where the family C has an explicit formula, the old Σ notation will be clearest, but in cases where A and C are abstract variables total-space A C is a useful alternative.

[jonweinb]

I'm in favor of this, but would suggest the name total-type rather than total-space since in general it won't be a space aka discrete.