Infer typeclass from within structure

Stream: new members

[Jake Levinson]

Here is a #mwe of the issue I'm running into. I have a typeclass I want to use as an inferred argument [my_class X] and a structure that bundles the data of an X : Type and a corresponding my_class X instance. But then the instance doesn't seem to be visible for automatic typeclass inference later on.

Toy example:

class my_class (X : Type) := (elem [] : X)

open my_class

def cool_map {X Y : Type} [my_class X] [my_class Y] (f : X → Y) :=
  f (elem X) = elem Y

structure cool_structure (Y : Type) [my_class Y] :=
  (X : Type)
  (α : my_class X)
  (f : X → Y)
  (h : cool_map f)

lemma some_lemma {Y : Type} [my_class Y] (C : cool_structure Y)
  (g : Y → Y) (hg : g (elem Y) = elem Y) : cool_map (g ∘ C.f) := sorry

/-
failed to synthesize type class instance for
Y : Type,
_inst_1 : my_class Y,
C : cool_structure Y,
g : Y → Y,
hg : g (elem Y) = elem Y
⊢ my_class C.X
-/

Of course, there is a my_class C.X instance, namely C.α. If I write @cool_map _ _ C.α _ (g ∘ C.f) then it works, but this is sort of annoying (even in this toy example it takes a bunch of dashes; in my actual example I want to avoid the @ notation).

Is there a way to make this kind of structure work? Or, a better way to do this? It seems like a design question (what goes in the structure and what stays outside of it) that would come up a lot...

[Mario Carneiro]

Of course, there is a my_class C.X instance, namely C.α.

But that's not an instance: You never declared it as such. If you use instance : my_class C.X := C.α then it should work

[Eric Wieser]

Or just attribute [instance] C.α

[Jake Levinson]

Ah, I see. Looks like either of those lines can go right below the structure definition:

instance (Y : Type) [my_class Y] (C : cool_structure Y) : my_class C.X := C.α
or
attribute [instance] cool_structure.α

That's exactly what I needed. Thank you both!

[Adam Topaz]

The usual thing to do is to declare a has_coe_to_sort using your cool_structure.X and then declare a my_class C instance for C : cool_structure using C.\alpha.
Take a look e.g. at the code around src#Group

[Jake Levinson]

Followup question to all this (possibly related to Adam Topaz's suggestion re: coercions, I think this question is undoubtedly already answered by the choices made in defining group and ring maps, but the code in src#Group is quite abstract for me, I don't get what's going on in it).

In the toy setting above (I guess my toy example was maps of pointed sets, plus "pointed sets over a base pointed set" or something). Would it be better to have defined cool_map as a structure containing both the map and the property? So instead of

def cool_map {X Y : Type} [my_class X] [my_class Y] (map : X → Y) := map (elem X) = elem Y)

I would do

structure cool_map {X Y : Type} [my_class X] [my_class Y] :=
  (map : X → Y)
  (h : map (elem X) = elem Y)

instance {X Y : Type} [my_class X] [my_class Y] : has_coe_to_fun (cool_map X Y) :=
  { F := λ _, X → Y, coe := λ α, α.map }

Maybe I would rather use this approach since, for one thing, it makes cleaner theorem statements to have the information in a cool_map packaged together. Likewise for continuous functions or whatever other category.

But, then I am not sure the best way to declare other structures on top of it. For example, say I want to define a cool_equiv X Y that consists of an equiv X Y using cool_maps instead of arbitrary functions. In this situation I would want to be able to go either from a cool_equiv (or whatever) to a normal equiv, or to the associated cool_maps. I can say

structure cool_equiv (X Y : Type) [my_class X] [my_class Y] extends equiv X Y :=
  (cool : to_fun (elem X) = elem Y)
  (inv_cool : inv_fun (elem Y) = elem X)

variables {X Y : Type} [my_class X] [my_class Y] (φ : cool_equiv X Y)
def cool_equiv.to_cool_map : cool_map X Y := ⟨φ.to_fun, φ.cool⟩
def cool_equiv.inv_cool_map : cool_map Y X := ⟨φ.inv_fun, φ.inv_cool⟩

or I can instead package in the cool_maps and write the coercion to equiv X Y separately.

structure cool_equiv' (X Y : Type) [my_class X] [my_class Y] :=
  (to_cool_map : cool_map X Y)
  (inv_cool_map : cool_map Y X)
  (left_inv : function.left_inverse inv_cool_map to_cool_map)
  (right_inv : function.right_inverse inv_cool_map to_cool_map)

variables {X Y : Type} [my_class X] [my_class Y]
instance : has_coe (cool_equiv' X Y) (equiv X Y) :=
  ⟨λ φ, equiv.mk φ.to_cool_map φ.inv_cool_map φ.left_inv φ.right_inv⟩

I'm just wondering which of these approaches is better, and/or if either would cause me pain further down the road. Or, maybe there's some other way that's better?

[Adam Topaz]

@Jake Levinson is there some mathematical concept you're trying to model here? Pointed types?

[Yakov Pechersky]

The way ring_equivs are set up are independent of ring_hom. One does not need two ring_hom to make a ring_equiv. But I think there is a helper constructor that can take two ring_homs and make a ring_equiv, with the proper constraint that they are inverses

[Yakov Pechersky]

So I think that implies that the structure extends equiv is the better approach.

[Yakov Pechersky]

You can always bake in the forward direction proof of coolness by doing

my_cool_equiv := { ..my_cool_hom, other_field := _, }

[Adam Topaz]

It doesn't really matter if you make the right API e.g. you can just define a cool_equiv.to_equiv function and a cool_equiv.mk' constructor

[Jake Levinson]

Adam Topaz said:

Jake Levinson is there some mathematical concept you're trying to model here? Pointed types?

The actual example that prompted my post isn't so different from pointed types: continuous fiber bundle maps, and in particular the "continuous" part. I had already made some working API for "maps of fiber bundles" without any continuity conditions, so I was trying to extend my various fiber-bundle-related structures to add hypotheses about all the maps being continuous. I ran into the issue sketched about above when defining a cts_bundle_equiv since I had to decide how to relate it to bundle_equiv and cts_bundle_map which I had defined previously.

(I also ran into the simpler version of this question when defining continuous functions originally, and for whatever reason chose the other way -- defining cts as a property of functions rather than as part of a cts_map structure.)

[Adam Topaz]

I see. Presumably you need to add docs#continuous properties for the functions you use, or perhaps use bundled continuous maps instead of functions (we have such bundled continuous maps in mathlib)

[Adam Topaz]

docs#continuous_map