HoTT/HoTT — pull request #639 by JasonGross (2014-12-12 08:18:38+00:00)
Title: Add LaxComma to categories.v

I had forgotten to export it when I originally ported it.