Progress on [isconn_wedge_incl].
Completed crude proof of wedge-elim, modulo lemma on connectedness of point-inclusion.
Merge branch 'master' into connectedness
Connectedness: abstracted/reorganised some auxiliary lemmas.
Added lemmas that [projT1_path] preserves groupoid structure.
Somewhat improved proof of [isconn_wedge_incl].
Completed wedge-inclusion connectivity lemma; reorganised Connectedness slightly.
Moved [unit_name] and [concatR] out of Connectedness to better homes.
Merge branch 'master' into connectedness
Added tactic [equiv_via].
Minor documentaion/alignment updating.
Fixed issue with prev definition of [equiv_via].
Added [contr_arrow], [trunc_arrow].
Initiated TruncType; proved that types of level n form an (n+1)-type, modulo one lemma.
ATruncType: added [contr_equiv_contr_contr], completing dependencies of [istrunc_trunctype].
Cleaned up auxiliary lemmas in TruncType.
Connectedness: minor cleanup.
Removing stale files
Moving around stale stuff
mistake