Zulip Chat Archive

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