proposition: 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: Proof. intros. induction a as [ ane | t ]. induction ane as [ a ne ]. simpl. apply idpath. induction t. simpl. apply idpath. Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom