proposition: 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: Proof. intros ex. apply @pathscomp0 with (transportf _ (idpath _) x). - apply (maponpaths (λ p, transportf _ p x)). apply hs. - exact ex. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics