Definition path_to_fun {X Y} : X=Y -> X->Y. Proof. intros p. induction p. exact (idfun _). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.PartA.