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