proposition: Lemma eqcor0UAH { X X' : UU } ( w : X ≃ X' ) ( Y : UU ) ( f1 f2 : X' -> Y ) : (λ x : X, f1 ( w x )) = (λ x : X, f2 ( w x ) ) -> f1 = f2.
proof: Proof. apply ( invmaponpathsweq ( make_weq _ ( isweqcompwithweqUAH w Y ) ) f1 f2 ). Defined.
imports: UniMath.Foundations.PartB