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. Proof. intros. destruct e. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Equivalences.