search

mortberg / cubicaltt

Experimental implementation of Cubical Type Theory
https://arxiv.org/abs/1611.02108
MIT License
571 stars 76 forks source link

Please don't call it the "grad lemma". #72

Closed mikeshulman closed 7 years ago

mikeshulman commented 7 years ago

Generally there are two ways that theorems and lemmas are named in mathematics: descriptively (giving some information about what the theorem says, e.g. "the intermediate value theorem") and attributively (giving credit to whoever proved it, e.g. "Cauchy's theorem"). Whatever your feelings about the relative merits of the two, the name "grad lemma" achieves neither: it conveys no information about what the lemma says, nor does it give any credit to the people it refers to, instead depersonalizing them as "some nameless graduate students". Moreover it is even factually incorrect, since some of the people in question were actually postdocs at the time.

The HoTT/Coq library calls the analogous theorem adjointify, since it makes a non-adjoint equivalence into a (half-)adjoint one. That may not be so appropriate if your notion of "coherent equivalence" is not the half-adjoint one, but maybe coherentify would work. The HoTT/Agda library calls it is-eq, with a comment that this "is a very, very bad name." But even is-eq is better than "grad lemma".

mortberg commented 7 years ago

I think our use of this name dates back to Vladimir's Foundations code where it is called gradth. It is still called this in the Foundations part of UniMath:

https://github.com/UniMath/UniMath/blob/master/UniMath/Foundations/PartA.v#L1759

I agree that "grad lemma" is a bad name and I would be happy to change it to something more descriptive. Maybe isoToEquiv could be a lot better?

mikeshulman commented 7 years ago

Yes, I know it comes from UniMath. I haven't quite got up my courage to open an issue there yet, but after you change it here then maybe I will. I think isoToEquiv would be a great name!

coquand commented 7 years ago

Indeed it was from Vladimir's library and there's no reason to keep the same name given Mike's objections

Sent from my iPhone

On 11 Aug 2017, at 18:37, Anders Mörtberg notifications@github.com wrote:

I think our use of this name dates back to Vladimir's Foundations code where it is called gradth. It is still called this in the Foundations part of UniMath:

https://github.com/UniMath/UniMath/blob/master/UniMath/Foundations/PartA.v#L1759

I agree that "grad lemma" is a bad name and I would be happy to change it to something more descriptive. Maybe isoToEquiv could be a lot better?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

mortberg commented 7 years ago

@coquand : Do you also like the name isoToEquiv? If so I'll change it now.

mortberg commented 7 years ago

I have renamed this now and there should be no mention of grad lemma anywhere on the master branch (grepping for grad or Grad doesn't return anything at least). If I still managed to miss something or if some file doesn't load please let me know and I'll fix it. I didn't bother changing this on the many branches, but if we ever decide to merge for example the hcomptrans branch I'll make sure to change this there as well.

@mikeshulman : Thanks for getting us to change this to a more descriptive name. I'll close this issue now.

mikeshulman commented 7 years ago

Thank you!