Lemma test (X Y : UU) (phi : F X Y) (f : X -> Y) : paths (Fd1 phi (Fi (X -> Y) Y f)) (Fd2 phi (Fi (X -> Y) Y f)). Proof. intros. unfold Fd1. unfold Fd2. unfold Fi. unfold Ffunct. unfold funcomp. simpl. apply (maponpaths phi). apply etacorrection. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.