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.