HoTT/HoTT — pull request #20 by benediktahrens (2012-10-11 01:37:20+00:00)
Title: Equiv as total space

Equiv as total space rather than record.
I suggest this change even though people might be even less convinced that this is necessary than they are for direct products...
Anyway, so far the mentioned reasons for preferring records over sigmas are not convincing, as show these patches. This might change when things grow, however.