HoTT/HoTT — pull request #208 by JasonGross (2013-09-05 18:53:04+00:00)
Title: Make [sigT] an alias for [sig].

Now we only need to use [sig], [exist], and can choose either [proj1],
[proj1_sig], or [projT1] for its first projection (and similarly for its
second projection). Because [proj1] used to be for [and], which is now
a notation for [prod], I've added a coercion [prod >-> sig] which allows
us to use [proj1] in place of [fst] and [proj2] in place of [snd].
Additionally, I've made the parameters for [proj1] and [proj2] implicit
and maximally inserted, so that we can do things like [ap proj1] and
have it mean what we want it to (that is, [ap proj1] is [ap (@proj1 _
_)]). It would be nice to unify [Coq.Init.Specif] and
[Coq.Init.Datatypes], and make [fst] and [snd] just puns of [proj1] and
[proj2], maybe, but I think Coq will complain if I move identifiers
between files.