Stream: new members

Topic: iff raises error

Jason KY. (May 22 2020 at 18:52):

I have the following #mwe

import topology.basic

variables {X : Type*} [topological_space X]
variables {Y : Type*} [topological_space Y]

def is_continuous (f : X → Y) : Prop :=
∀ U : set Y, is_open U → is_open (f ⁻¹' U)

structure topological_space_equiv
(X Y) [topological_space X] [topological_space Y] extends X ≃ Y :=
(contin     : is_continuous to_fun)
(inv_contin : is_continuous inv_fun)
notation X  ≃*  Y := topological_space_equiv X Y

open function

noncomputable theory

example : (X ≃* Y) →
(∃ (f : X → Y) (h₀ : bijective f) (h₁ : is_continuous f),
∀ U : set X, is_open U → is_open (f '' U)) := sorry -- no errors

example : (∃ (f : X → Y) (h₀ : bijective f) (h₁ : is_continuous f),
∀ U : set X, is_open U → is_open (f '' U)) → (X ≃* Y) := sorry -- no errors

example : (X ≃* Y) ↔ -- breaks here
(∃ (f : X → Y) (h₀ : bijective f) (h₁ : is_continuous f),
∀ U : set X, is_open U → is_open (f '' U)) := sorry


As you can see, the first two examples work fine but the last one raises the error

type mismatch at application
iff (X ≃* Y)
term
X ≃* Y
has type
Type (max u_1 u_2) : Type (max (u_1+1) (u_2+1))
but is expected to have type
Prop : Type


Why might this be?

Kenny Lau (May 22 2020 at 18:53):

yeah, unlike in maths, "X and Y are homeomorphic" isn't a proposition

Jason KY. (May 22 2020 at 18:55):

Oh! I see! I should've thought about it a bit more

Kevin Buzzard (May 22 2020 at 18:55):

equiv X Y is data. That's why it's more than bijective f (which is a Prop)

Patrick Massot (May 22 2020 at 18:56):

Kenny Lau said:

yeah, unlike in maths, "X and Y are homeomorphic" isn't a proposition

That's not the issue. The issue is a somewhat confusing notation for the type of homeomorphisms from X to Y

Jason KY. (May 22 2020 at 18:56):

What's wrong with the notation?

Patrick Massot (May 22 2020 at 18:57):

It suggests a Prop

Patrick Massot (May 22 2020 at 18:57):

I found it very confusing in the beginning (the basic equiv case, this has nothing to do with topology) but I got used to it

Jason KY. (May 22 2020 at 18:58):

I think it's just confusing the first time it comes up. Hopefully I won't ever assume its a prop anymore :)

Last updated: May 13 2021 at 06:15 UTC