Definition 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) : x = y. Proof. induction x as [ [ x₁ x₂ ] px ]. induction y as [ [ y₁ y₂ ] py ]. cbn in p₁, p₂. induction p₁, p₂. cbn in p₃. apply maponpaths. exact (!(pathscomp0rid _) @ p₃). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.