Definition transportf2 {X} {Y:X->Type} (Z:∏ x, Y x->Type) {x x'} (p:x = x') (y:Y x) (z:Z x y) : Z x' (p#y). Proof. intros. induction p. exact z. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.