Definition path_hfp_eta {X Y Z : UU} {f : X → Z} {g : Y → Z} {x y : hfp f g} (p : x = y) : p = path_hfp (maponpaths (hfpg f g) p) (maponpaths (hfpg' f g) p) (maponpaths (λ z, _ @ z) (maponpathscomp (hfpg f g) f p) @ !(homotsec_natural (commhfp f g) p) @ maponpaths (λ z, z @ _) (!(maponpathscomp (hfpg' f g) g p))).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.