HoTT/HoTT — pull request #556 by JasonGross (2014-10-06 22:14:14+00:00)
Title: Factor out tactic scripts for exponential laws

These can probably be put in a more general place, and be used more
widely in categories. In general, the parts of a proof done by tactics
in categories are, in no particular order:

- apply type-driven principles, such as destructing [sum]-types in
hypotheses and applying [path_prod] or [path_functor] to the goal

- eliminate composition with identities and inverses and normalize
morphisms (w.r.t., e.g., associativity)

- eliminate [transport]s

- miscellany, such as eliminating points in contractible types,
inducting on paths, using [simpl] and [reflexivity], or using
hypotheses

The first is very systematic and general, and the second is amenable to
systematic tactics or reflective proof scripts. The third is,
currently, rather ad-hoc, and the fourth is generally straightforward
but occasionally complicated.