extends coercion

Stream: new members

[Raphael Appenzeller]

In the following example I introduce a class my_pointed_space and then extend it to a class singular_space. Later on I would like to coerce a singular_space to a my_pointed_space. Should this not happen automatically due to the keyword extends? MWE:

class my_pointed_space (α : Type*) :=
(a : α )

class singular_space (α: Type*) extends my_pointed_space α :=
(extra_property : ∀ x : α , x = my_pointed_space.a )

class my_map {α β : Type*} (X : my_pointed_space α ) ( Y : my_pointed_space β):=
(to_fun : α → β)
(compatibility : to_fun(X.a) = Y.a)

class inj {α β : Type*} (X : singular_space α) (Y : my_pointed_space β) extends my_map X Y

[David Renshaw]

does it work if you do X.to_my_pointed_space?

[Kyle Miller]

I haven't tested it, but you want to declare it something like this:

class my_map (α β : Type*) [my_pointed_space α] [my_pointed_space β] :=
(to_fun : α → β)
(compatibility : to_fun (my_pointed_space.a α) = my_pointed_space.a β)

[Yaël Dillies]

"coerce" has a very specific meaning in Lean, and this is probably not what you want.

[Yaël Dillies]

Kyle, I suspect the problem is that there are many ways to point a given type!

[Kyle Miller]

The purpose of classes is that you're going to rely on typeclass inference to obtain structures in an implicit way.

[Yaël Dillies]

Btw,my_pointed_space is docs#Pointed

[Yaël Dillies]

And my_map is docs#Pointed.hom

[Kyle Miller]

Yaël Dillies said:

Kyle, I suspect the problem is that there are many ways to point a given type!

If you're #xy'ing it, sure, but I think the proximal problem is about using classes correctly

[Kyle Miller]

Once you've got that my_map, then I expect something like this should work:

class inj (α β : Type*) [singular_space α] [my_pointed_space β] extends my_map α β

[David Renshaw]

@Kyle Miller to get your version to work I needed to change it to this:

class my_map (α β : Type*) [my_pointed_space α] [my_pointed_space β] :=
(to_fun : α → β)
(compatibility : to_fun (@my_pointed_space.a α _) = @my_pointed_space.a β _)

[Kyle Miller]

@David Renshaw Ok, that means the types didn't come out the way I expected them to on my_pointed_space. The idiomatic way to write it then is this:

class my_map (α β : Type*) [my_pointed_space α] [my_pointed_space β] :=
(to_fun : α → β)
(compatibility : to_fun (my_pointed_space.a : α) = (my_pointed_space.a : β))

[Kyle Miller]

I think the way to get my original version to work is to do

class my_pointed_space (α : Type*) :=
(a [] : α)

which causes my_pointed_space.a to take an explicit argument.

[Kyle Miller]

I believe what's going on is that Lean sees that alpha is inferrable from the return type so it makes it implicit by default.

[Raphael Appenzeller]

Thanks a lot for your answers. Indeed my problem was that I was not using classes correctly.