proposition: Theorem funextfunPreliminaryUAH : funextfunStatement.
proof: Proof. intros ? ? f1 f2 e. set ( f := λ x : X, pathsspacetriple Y ( e x ) ). set ( g1 := λ z : pathsspace Y, pr1 z ). set ( g2 := λ z : pathsspace Y, pr1 ( pr2 z ) ). change ( (funcomp f g1) = (funcomp f g2) ). apply maponpaths. apply apathpr1toprUAH. Defined.
imports: UniMath.Foundations.PartB