same definition with different names

[fpvandoorn]

In the HoTT library we have many definitions which mean the same thing. This is done usually for shortening a name, or for making version where some arguments implicit. Examples:

• eq.refl rfl idp idpath
• idpo idpatho
• ids idsquare
• is_equiv.mk is_equiv.mk' adjointify
• pointed.mk' pointed.Mk pointed.MK
• ...

It is important that they mean the same, and that it doesn't matter much which of these we used in a definition. In Lean 2 this worked well enough when making all the variants [reducible]. However, hsimp doesn't seem to treat all these variants as the same (which I think is why you added these lines https://github.com/gebner/hott3/blob/master/init/path.lean#L567-L568). What is the best solution to this? Should we add hsimp rules saying that these things are the same, so that it will reduce to the "canonical" one?

[fpvandoorn]

Ah, I now also see what you've done in simp_attr. Should we try to minimize the amount of these duplicate definitions?

[gebner]

Ok, the idp_tr' and idp_tr'' are superfluous (at least now, maybe I forget the reducible attribute at first). I have removed them.

The story for equivalent names is two-fold:

• For lemmas such as transport _ idp u = u, where idp/refl/idpath occurs as an argument, it only needs to be marked as [reducible]. We don't do any indexing on constant names in the arguments at the moment, we only call the type_context unifier with reducible transparency. If it unifies reducibly, it's fine.
• If we hypothetically defined trsprt idp u, then it would be more difficult to use idp_tr.
  • The rwr tactic supports "key equivalences". You can tell it that transport and trsprt are equivalent using add_key_equivalence, and then idp_tr will also match trsprt refl _.
  • The hsimp tactic matches on the literal name. The best bet here is to add an idp-lemma that simplifies trsprt to transport. (We could also extend the simplifier to support key equivalences if that is necessary.)

[fpvandoorn]

Ok, let's try to make all these duplicates reducible, and we'll see whether we need add_key_equivalence. Thanks for the explanation.