Coercion local homeomorph

Stream: new members

[Nicolò Cavalleri]

Is it a bad idea to define a coercion from from homeomorph to local_homeomorph so that one does not have to write .to_local_homeomorph each time?

[Reid Barton]

Based on https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/preferred.20alternatives.20to.20type.20ascriptions.20everywhere.3F/near/208213580, I don't think it would help as much as one would hope