Stream: new members

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

Abhimanyu Pallavi Sudhir (Nov 01 2018 at 11:30):

(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 (Nov 01 2018 at 12:27):

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'


universe issues

Abhimanyu Pallavi Sudhir (Nov 01 2018 at 12:35):

Oh -- of course. Thanks.

Abhimanyu Pallavi Sudhir (Nov 01 2018 at 12:39):

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

Last updated: May 13 2021 at 06:15 UTC