HoTT/HoTT — pull request #382 by JasonGross (2014-04-24 03:20:49+00:00)
Title: Pseudonatural transformation

This is on top of #381.

This is based on an email from Mike Shulman.

Compared with the pain of pseduofunctors, this one is surprisingly fast and (comparatively) lacking in pain.

I'm not at all confident that I got it right, given that [nCatLab](http://ncatlab.org/nlab/show/pseudonatural+transformation#definition) mentions three laws rather than just one (respect for composition, respect for units, and naturality). But I guess if it gives me enough rope to define lax comma categories, and if I can show that every natural transformation between functors to Cat gives rise to a pseudonatural transformation between the corresponding pseudofunctors, I might not care?

Given that, I'd like @mikeshulman (or someone else with familiarity with pseudonatural transformations) to look at the definition and verify that I got it right (or, at least, that I'm not missing any coherence laws), before this is merged.