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. apply transportf_comp_lemma_hset. - apply X. - apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.