Definition homot_hfp_one_type {X Y Z : UU} (HZ : isofhlevel 3 Z) {f : X → Z} {g : Y → Z} {x y : hfp f g} (p q : x = y) (r₁ : maponpaths (hfpg f g) p = maponpaths (hfpg f g) q) (r₂ : maponpaths (hfpg' f g) p = maponpaths (hfpg' f g) q) : p = q.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.