proposition: Lemma isweqrcompwithweqUAH { Y Y':UU } (w: Y ≃ Y')(X:UU) : isweq (fun a:X->Y => (λ x, w (a x))).
proof: Proof. simple refine (isweq_iso _ _ _ _). exact (fun a':X->Y' => λ x, (invweq w (a' x))). exact (fun a :X->Y => funextfunPreliminaryUAH _ a (λ x, homotinvweqweq w (a x))). exact (fun a':X->Y' => funextfunPreliminaryUAH _ a' (λ x, homotweqinvweq w (a' x))). Defined.
imports: UniMath.Foundations.PartB