Zulip Chat Archive

Stream: new members

Topic: iff raises error


view this post on Zulip 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?

view this post on Zulip Kenny Lau (May 22 2020 at 18:53):

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

view this post on Zulip Jason KY. (May 22 2020 at 18:55):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Jason KY. (May 22 2020 at 18:56):

What's wrong with the notation?

view this post on Zulip Patrick Massot (May 22 2020 at 18:57):

It suggests a Prop

view this post on Zulip 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

view this post on Zulip 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