Lemma transportf_comp_lemma_hset (X : UU) (B : X -> UU) (A : X) (e : A = A) {x x' : B A} (hs : isaset X) : x = x' -> transportf _ e x = x'. Proof. intros ex. apply @pathscomp0 with (transportf _ (idpath _) x). - apply (maponpaths (λ p, transportf _ p x)). apply hs. - exact ex. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.