proposition: Lemma transportf_set {A : UU} (B : A → UU) {a : A} (e : a = a) (b : B a) (X : isaset A) : transportf B e b = b.
proof: Proof. apply transportf_comp_lemma_hset. - apply X. - apply idpath. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics