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.