Definition maponpaths_hfpg'_path_hfp {X Y Z : UU} {f : X → Z} {g : Y → Z} {x y : hfp f g} (p₁ : hfpg f g x = hfpg f g y) (p₂ : hfpg' f g x = hfpg' f g y) (p₃ : commhfp f g x @ maponpaths f p₁ = maponpaths g p₂ @ commhfp f g y) : maponpaths (hfpg' f g) (path_hfp p₁ p₂ p₃) = p₂.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.