Theorem homotrecomplnat {X Y : UU} (w : X ≃ Y) (x : X) (a : compl X x ⨿ unit) : recompl Y (w x) (coprodf (weqoncompl w x) (idfun unit) a) = w (recompl X x a). Proof. intros. induction a as [ ane | t ]. induction ane as [ a ne ]. simpl. apply idpath. induction t. simpl. apply idpath. Defined.