fact: Definition eqweqmapap_inv {T} (P:T->Type) {t u:T} (e:t = u) (p:P u) : (eqweqmap (maponpaths P e)) ((eqweqmap (maponpaths P (!e))) p) = p.
imports: UniMath.Foundations.All UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Equivalences