Structures vs Type classes: Projections

Stream: Is there code for X?

[Sina]

Say I have defined a structure named blah which has fields F1 ... Fn in its definition. When proving a certain theorem about blah, I have in my context some stuff X Y Z: blah which are going to be used in the statement and the proof of the theorem. In my tactic-style proof, Lean can display in context/goal X.F1, Y.F1 etc which is great. But, if I make blah into a type-class, which is desirable in some situations, then instead of X.F1 Lean displays blah.F1 for both X.F1, Y.F1, which is less useful when proving theorems with lots of instances. Is there a way to formalize my structure blah with a type-class but also have the useful projections X.F1, Y.F1?

[Yaël Dillies]

Yes, replace (the_field_I_want_a_projection_of : its_type) by (the_field_I_want_a_projection_of [] : its_type) in the structure declaration.

[Sina]

Not sure I am doing it right. Here's a MWE:

class functor (𝓒 : Type u₁) [category_str.{v₁} 𝓒] (𝓓 : Type u₂) [category_str.{v₂} 𝓓] : Type (max v₁ v₂ u₁ u₂) :=
(obj [] : 𝓒 → 𝓓)
(mor [] : Π {X Y : 𝓒}, (X ⟶ Y) → (obj X ⟶ obj Y))
(resp_id'   :
∀ (X : 𝓒), mor (𝟙 X) = 𝟙 (obj X) )
(resp_comp' :
∀ {X Y Z : 𝓒} (f : X ⟶ Y) (g : Y ⟶ Z), mor (f  ≫ g ) = (mor f) ≫  (mor g) )

Now, in defining composition of functors, Lean displays mor 𝓔 (mor 𝓓 (𝟙 X)) = 𝟙 (obj (obj X)) (when i put my cursor on the first simp in the definition below) whereas i would like it to display G.mor (F.mor (𝟙 X)) = 𝟙 (G.obj (F.obj X)).

def comp (F : functor 𝓒 𝓓) (G : functor 𝓓 𝓔) : functor 𝓒 𝓔 :=
{
  obj :=  λ X, G.obj (F.obj X), -- G.obj ∘ F.obj,
  mor := λ X, λ Y, λ f, G.mor (F.mor f),
  resp_id' := by {intro X, simp only [functor.resp_id ], },
  resp_comp' := by {intros X Y Z f g, simp only [functor.resp_comp],},
}

[Yaël Dillies]

That doesn't answer your question, but you most definitely don't want functor to be a class, as it means you will be able to use only one functor between any two categories!

[Sina]

Absolutely, I just used the functor example as MWE, since your trick with [ ] would work for other examples i had. Thanks for your answer though, i never quite understood the purpose of [ ] in type classes before.

[Reid Barton]

Have you tried defining your structure as a structure, but then adding attribute [class] to it afterwards?

[Yaël Dillies]

The [] trick answers why it shows up as blah.F1 rather than X.F1, but your second message makes it seem that you expected X.F1 rather than blah.F1 X. This is a different question, and relates to "pretty-printing" (aka pp).

[Sina]

@Yaël Dillies I see. I'd prefer X.F1, but would also be happy with blah.F1 X. With functor example, I do not even get the latter; I only get blah.F1. So, adding [] to obj and mor field of the functor type class , Lean would display

mor 𝓔 (mor 𝓓 (𝟙 X)) = 𝟙 (obj 𝓔 (obj 𝓓 X))

instead of

mor (mor (𝟙 X)) = 𝟙 (obj (obj X))

without adding [].

Does pp help with displaying either F.mor or mor F for a functor (F : functor 𝓒 𝓓) ? Again this is in the context of wrongly declaring functor as a type-class.