Definition transport_fun_path {X Y} {f g:X->Y} {x x':X} {p:x = x'} {e:f x = g x} {e':f x' = g x'} : e @ maponpaths g p = maponpaths f p @ e' -> transportf (λ x, f x = g x) p e = e'. Proof. intros k. induction p. rewrite maponpaths_idpath in k. rewrite maponpaths_idpath in k. rewrite pathscomp0rid in k. exact k. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.