fact: Definition homotrecomplfhomot {X Y : UU} (x : X) (y : Y) (isx : isisolated X x) (f f' : compl X x -> compl Y y) (h : homot f f') : homot (recomplf x y isx f) (recomplf x y isx f').
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom