strong_equivalence

A Coq formalisation in HoTT about strong equivalence, heterogeneous equality, and equivalent formulations of the univalence axiom.