Lean unable to coerce from set to type (or something)

Stream: new members

[Abhimanyu Pallavi Sudhir]

(approximately M)WE:

import data.set.basic
import data.set.lattice
universe u

variable {X : Type u}
variable {Y : Type u}
variable {f : X → Y}

def G (f : X → Y) : set (X × Y) := { g | g.2 = f (g.1) }
def p1 (g : G f) : X := g.1.1
def injectivity' {X' Y' : Type} (g : X' → Y') := ∀ x1 x2 : X', g x1 = g x2 → x1 = x2
def surjectivity' {X' Y' : Type} (g : X' → Y') := ∀ y : Y', ∃ x : X', g x = y
def bijectivity' {X' Y' : Type} (g : X' → Y') := injectivity' g ∧ surjectivity' g

theorem bij_p1 : @bijectivity' (↥(set (X × Y))) (↥(G f)) (p1) :=
    begin
        sorry,
    end

#check p1
#check bijectivity'

But Lean doesn't seem to understand that ↥(set (X × Y) is a Type -- it gives me the error failed to synthesise type class instance for: has_coe_to_sort (Type u). What's going on?

[Kenny Lau]

import data.set.basic
import data.set.lattice
universe u

variable {X : Type u}
variable {Y : Type u}
variable {f : X → Y}

def G (f : X → Y) : set (X × Y) := { g | g.2 = f (g.1) }
def p1 (g : G f) : X := g.1.1
def injectivity' {X' Y' : Type u} (g : X' → Y') := ∀ x1 x2 : X', g x1 = g x2 → x1 = x2
def surjectivity' {X' Y' : Type u} (g : X' → Y') := ∀ y : Y', ∃ x : X', g x = y
def bijectivity' {X' Y' : Type u} (g : X' → Y') := injectivity' g ∧ surjectivity' g

theorem bij_p1 : @bijectivity' (↥(G f)) X (p1) :=
    begin
        sorry,
    end

#check p1
#check bijectivity'

[Kenny Lau]

universe issues

[Abhimanyu Pallavi Sudhir]

Oh -- of course. Thanks.

[Abhimanyu Pallavi Sudhir]

And I have no clue why I was putting in the domain and range of f instead of p1.