fact: Definition recomplf {X Y : UU} (x : X) (y : Y) (isx : isisolated X x) (f : compl X x -> compl Y y) : X -> Y := funcomp (funcomp (invmap (weqrecompl X x isx)) (coprodf f (idfun unit))) (recompl Y y).
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom