Definition homot_hfp {X Y Z : UU} {f : X → Z} {g : Y → Z} {x y : hfp f g} {h₁ h₁' : hfpg f g x = hfpg f g y} (e₁ : h₁ = h₁') {h₂ h₂' : hfpg' f g x = hfpg' f g y} (e₂ : h₂ = h₂') (h₃ : commhfp f g x @ maponpaths f h₁ = maponpaths g h₂ @ commhfp f g y) : path_hfp h₁ h₂ h₃ = path_hfp h₁' h₂' (maponpaths (λ z, _ @ maponpaths f z) (!e₁) @ h₃ @ maponpaths (λ z, maponpaths g z @ _) e₂).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.