Lemma testd2 {X Y : UU} (psi : F X Y -> Y) (phi : F X Y) : paths (Fv (funcomp (Fi X Y) psi) phi) (Fd2 phi psi). Proof. intros. apply idpath. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.