Adapting to the new methodology with canonical structures
Added pentagonator, triangulator (bicat coherence structure); other minor changes.
Half done
More notation conventions, better concat2
use /\ for products only for parsing
commiting before pull
commit before pull
Merge branch 'master' of github.com:andrejbauer/HoTT
Fixed typo in prev commit.
renaming a few things
Make path concatenation destruct on both its arguments
Added plan for rewriting/reorganising Fibrations.v
Remove a spurious argument from whiskerL_1p
The Eckmann-Hilton argument
Merge branch 'master' of https://github.com/andrejbauer/HoTT
Changed some Lemmas/Qed to Definitions/Defined (for consistency with rest of file; plus, we expect to need their reduction later).
Defined [pmap_dep]; also, some reorganisation.:
Added coherence for transport on associativity.
Added path tactics.
Changed [pmap] from a notation to a definition (reasons documented inline), and similarly added [inverse].