Structure homeomorphism

Stream: new members

[Nicolò Cavalleri]

Why is homeomorphism a structure and not a class? Supposed I defined a diffeomorphism, how do I build out of it an instance of homeomorphism or somehow transform it into a homeomorphism?

[Mario Carneiro]

you define a function from diffeo to homeo and make it a coe

[Yury G. Kudryashov]

It is not a class because we want to work with different homeomorphisms between the same pair of types.

[Nicolò Cavalleri]

Mario Carneiro said:

you define a function from diffeo to homeo and make it a coe

Suppose I did define a function def diffeomorph_to_homeomorph (d : M ≃ₘ[I|J] N) : M ≃ₜ N. What do you mean by making it a coe?

[Patrick Massot]

https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#coercions-using-type-classes