Remove Trunc_2 axiom and turn it into a WeakGroupoid component (avoids
inconsistency).
Adapt to latest polyproj branch of mattam82/coq.