Lemma isaprop_isweqtoforallpathsStatement : isaprop isweqtoforallpathsStatement. Proof. unfold isweqtoforallpathsStatement. apply impred_isaprop; intro T; apply impred_isaprop; intro P; apply impred_isaprop; intro f; apply impred_isaprop; intro g. apply isapropisweq. Defined.
Require Import UniMath.Foundations.PartD.