Zulip Chat Archive

Stream: new members

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


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

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 12:27):

universe issues

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 01 2018 at 12:35):

Oh -- of course. Thanks.

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