Thanks for your contribution! Is this ready for review? If so, please label it awaiting-review. (See here for a more detailed explanation of this and related labels.)

For context, there was already a little bit of discussion over this here on Zulip. One concern voiced there was that having an unbundled predicate in addition to the bundled Homeomorph structure would encourage a lot of API duplication. The way I've tried to avoid that is by only implementing API relating this to other unbundled properties of maps, such as with IsHomeomorph.isClosedMap - theorems involving properties of sets and spaces, like Homeomorph.compactSpace, are still available only for bundled homeomorphisms. My hope is that this provides enough API for most situations in which the IsHomeomorph predicate might be used, while also making it easy enough to convert between the IsHomeomorph and Homeomorph types when the additional API of Homeomorph is needed.

Hi @peabrainiac, this PR looks mostly fine, but there are still some places where it needs some work. Are you planning to continue working on this PR? Would you like some help from others, or do you want to hand over completely? (In the latter case, please label it with please-adopt.)

@peabrainiac, it looks like the PR hasn't moved since we last pinged you. We're going to close this for now, just for the sake of cleaning up our PR queue. But please do feel free to either re-open the PR if you'd like to continue working on it, or come across to the PR reviews zulip stream to ask for advice or request that we look at this again.

@j-loreaux asked that we reopen this.

PR summary 80789fee7f

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

build failing @YaelDillies

bors d+

✌️ peabrainiac can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

oops

bors d=yaeldillies

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors d-

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style