Definition path_path_fun {X Y : UU} {f g : X → Y} {e₁ e₂ : f = g} (h : ∏ (x : X), eqtohomot e₁ x = eqtohomot e₂ x) : e₁ = e₂. Proof. refine (!(@funextsec_toforallpaths X (λ _, Y) f g e₁) @ _). refine (_ @ @funextsec_toforallpaths X (λ _, Y) f g e₂). apply maponpaths. use funextsec. intro x. apply h. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.PartA.