proposition: Theorem isweqtoforallpathsUAH : isweqtoforallpathsStatement.
proof: Proof. unfold isweqtoforallpathsStatement. intros. refine (isweqtotaltofib _ _ (λ (h:∏ t, P t), toforallpaths _ h g) _ f). refine (isweqcontrcontr (X := ∑ (h: ∏ t, P t), h = g) (λ ff, tpair _ (pr1 ff) (toforallpaths P (pr1 ff) g (pr2 ff))) _ _). { exact (iscontrcoconustot _ g). } { apply funextcontrUAH. } Qed.
imports: UniMath.Foundations.PartB