HoTT/HoTT — pull request #407 by JasonGross (2014-07-15 22:04:24+00:00)
Title: Port Matthieu's code formalizing pushouts

This code will (hopefully) allow the epi -> surj in set_cat proof to go
through without hacks and without universe inconsistencies in trunk.

The formalization is a bit slow (at 9s)...

I'm also not entirely happy with the proofs.

I think this needs at least one, maybe two pairs of eyes, other than my own and Matthieu's.