HoTT/HoTT — pull request #580 by mikeshulman (2014-10-18 22:14:40+00:00)
Title: Some lemmas about commutative squares.

I thought these would be used in more places, but I only found one.