Lemma pathscomp0_dep {X : UU} {P : X → UU} {x x' x'' : X} {e : x' = x} {e' : x'' = x'} {y} {y'} {y''} : (y = transportf P e y') -> (y' = transportf _ e' y'') -> y = transportf _ (e' @ e) y''. Proof. intros ee ee'. etrans. apply ee. apply transportf_bind, ee'. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.