UnivalentMathematics/Foundations — pull request #6 by DanGrayson (2014-03-16 12:00:26+00:00)
Title: simplify the proof of weqdirprodcomm in uu0

Definition weqdirprodcomm X Y : weq (dirprod X Y) (dirprod Y X).