fact: Definition invrecompl (X : UU) (x : X) (is : isisolated X x) : X -> coprod (compl X x) unit := λ x' : X, match (is x') with | ii1 e => ii2 tt | ii2 phi => ii1 (make_compl _ _ x' phi) end.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom