TopCat private mk

Stream: mathlib4

[Calle Sönne]

TopCat is defined in the following way in mathlib:

/-- The category of semirings. -/
structure TopCat where
  private mk ::
  /-- The underlying type. -/
  carrier : Type u
  [str : TopologicalSpace carrier]

My question is: why is the mk made private here? A bit below a constructor of is defined as follows:

/-- The object in `TopCat` associated to a type equipped with the appropriate
typeclasses. This is the preferred way to construct a term of `TopCat`. -/
abbrev of (X : Type u) [TopologicalSpace X] : TopCat :=
  ⟨X⟩

I do not see what the difference between of and mk is, so why is mk not just renamed to of (and not made private)?

[Calle Sönne]

I just made this #31622 to see what happens

[Anne Baanen]

TopCat.mk has different parameters as implicit and explicit IIRC.

[Calle Sönne]

It looks like both are explicit to me (I also thought this might be the case at first)

[Anne Baanen]

Ok, then I can't think of a reason either! :)

[Anne Baanen]

If we do make this change, then we should do the same for other categories.

[Calle Sönne]

For quite a few of these Cat structures there is a difference in implicit/explicit arguments. I think there is still a fix by writing specifying the explicit arguments via of (..) :: but this requires moving some variables into the structure declaration and there is a bunch of places where this could be done which seems very fiddly so I decided not to. Basically, I implemented this change only in files where it was trivial to do so, and mainly to prevent other people from becoming slightly confused like I did above.

[Christian Merten]

Calle Sönne said:

It looks like both are explicit to me (I also thought this might be the case at first)

Did this change? I am quite sure the difference in explicitness was the reason for the additional of constructor.

[Christian Merten]

This https://github.com/leanprover-community/mathlib4/pull/19065#discussion_r1847447502 is the corresponding discussion.

[Christian Merten]

I am confused:

structure FooCat (X : Type) where
  of ::
  carrier : Type

/--
info: FooCat.of {X : Type} (carrier : Type) : FooCat X
-/
#guard_msgs in
#check FooCat.of

seems to suggest the explicitness is still the same (X is implicit, but it should be explicit).

[Christian Merten]

Oh, sorry. I understand now. This of course only matters for relative categories, but not for TopCat which does not have a parameter.

[Calle Sönne]

Yeah exactly, I assume it's there because it was needed in a lot of other cases

[Calle Sönne]

Anyways the PR is ready to go now, it compiles and doesn't affect peformance.

[Andrew Yang]

I tried to do this once to another concrete category and the objection I got during the review was "we prefer global uniformity over local optimisations". Do we still care?

[Calle Sönne]

I vote for caring because this made me confused enough to post on zulip. The other alternative is to add a docstring explaining why we do it this way.

[Calle Sönne]

Also I do think basically all of these cases can nowadays be made with the single constructor of. For example in @Christian Mertens example above we can nowadays write:

structure FooCat (X : Type) where
  of (X) ::
  carrier : Type

[Calle Sönne]

So we could have global uniformity, but I was not motivated enough to also do it in these slightly trickier cases (especially as it involves moving such parameters into the definition of the structure itself, this would not work if X was a variable).

[Andrew Yang]

Oh that is valid syntax now? Then I would vote for switching everything to of ::. I think it would be very useful to have the ⟨X⟩ notation available.

[Calle Sönne]

Maybe I can try to fix this as well (but in another PR, as this one is getting merged)

[Kevin Buzzard]

oh wow this was my lean4#3574 and Eric's lean4#9072 , I also had not internalised that it actually existed now.

[Calle Sönne]

Andrew Yang said:

Oh that is valid syntax now? Then I would vote for switching everything to of ::. I think it would be very useful to have the ⟨X⟩ notation available.

Is this supposed to work when you have multiple explicit arguments? For example take AlgCat where an algebra X also requires a base ring R. It seems to me that if I change mk to make R explicit then ⟨X⟩ fails (as it is now expecting two arguments). So my question is: is there syntax for using ⟨ ⟩ with multiple arguments?

[Joël Riou]

Kevin Buzzard said:

oh wow this was my lean4#3574 and Eric's lean4#9072 , I also had not internalised that it actually existed now.

This means we have been able to remove many typeclasses fields like foo', see #26468 or #26252 for example.

[Junyan Xu]

So my question is: is there syntax for using ⟨ ⟩ with multiple arguments?

Did you try ⟨R, X⟩? It's also possible to write @⟨_, _⟩ but then you need to specify all implicit arguments. The (_ := _) syntax is probably not available for the anonymous constructor ⟨ ⟩.

[Calle Sönne]

Junyan Xu said:

So my question is: is there syntax for using ⟨ ⟩ with multiple arguments?

Did you try ⟨R, X⟩? It's also possible to write @⟨_, _⟩ but then you need to specify all implicit arguments. The (_ := _) syntax is probably not available for the anonymous constructor ⟨ ⟩.

Yes I did try ⟨R, X⟩, which gives an error saying that the expected type is not inductive. @⟨_, _⟩ also does not seem to work for similar reasons.

[Jovan Gerbscheid]

So do we need to make a new issue in Lean, since this notation doesn't work?

[Calle Sönne]

Possibly yeah, but is it expected that it should work with multiple arguments like this? Should the expected behaviour be that writing ⟨ ⟩ makes the extra argument implicit (so that you only need to provide one thing)? Presumably when using this notation you know the target type (e.g. AlgCat R) so you should be able to infer R.

[Jovan Gerbscheid]

Yes, I would expect that changing implicitness in the constructor does not change the syntax of the (nameless) constructor notation.