Refactor diagonals

[fredrik-bakke]

• Renames diagonal to diagonal-product, and diagonal-maps-of-types to diagonal-maps-cartesian-products-of-types
• Defines diagonal-exponential A X : A -> X -> A in a file diagonal-maps-of-types

[fredrik-bakke]

I'm open to renaming suggestions for diagonal-product, diagonal-exponential and their files diagonal-maps-cartesian-products-of-types and diagonal-maps-of-types.

[EgbertRijke]

I'm experimenting with having

const' : {l1 l2 : Level} (A : UU l1) (B : UU l2) → B → A → B
const' A B b x = b

const : {l1 l2 : Level} {A : UU l1} {B : UU l2} → B → A → B
const = const' _ _

in the library.

In most cases Agda can infer both types. Typical places where Agda can't infer both types is when we assert something about a constant map in the type specification of an entry, but this doesn't have to rule our design choice.

The other reason why I think it is worth considering this option, is that I want to avoid creating inbalances in which arguments are made implicit and which aren't. In the case for many entries about commuting triangles it was a great pain to maintain the entries where the choice of implicit arguments was based on "what agda can infer", implying that the choice was varying a lot and it was extremely hard to keep track of what arguments Agda was expecting. This experience makes me wary about making one type explicit and one type implicit in const, even though I am aware that in the case at hand it won't be as painful to maintain const if only the codomain is implicit. I just think that from a maintainers perspective, it is not good to let Agda dictate what arguments should be implicit based but we should make that decisions as library designers based on what argument could be logically grouped together.

Moreover, it turns out that in fact Agda can infer both types in most cases, the same way that Agda can infer the element at which refl-htpy is taken in a proof. In this case we also have both refl-htpy and refl-htpy', where the latter is mostly used in type specifications of entries when the function cannot be inferred.

Sorry for the long story:P

[EgbertRijke]

I completed my experiment in #1097. I think it works well to have both type arguments of const implicit.

If you agree with that change, then I can close that pull request again and let you make that change here. I don't want that pull request to cause troubles with your work here by merging it, so I'd rather delete it.

[VojtechStep]

I just think that from a maintainers perspective, it is not good to let Agda dictate what arguments should be implicit based but we should make that decisions as library designers based on what argument could be logically grouped together.

The way I'm reading this is in contradiction with the coding style. Quoting https://unimath.github.io/agda-unimath/CODINGSTYLE.html#guidelines-for-definitions-in-the-agda-unimath-libraryhttps://unimath.github.io/agda-unimath/CODINGSTYLE.html#guidelines-for-definitions-in-the-agda-unimath-library:

Implicit arguments: If an argument can be inferred in most use cases, make it implicit.

Should the guideline be edited to not make this very direct blanket statement?

[fredrik-bakke]

That's interesting, because I changed which arguments are implicit for const based on how I would want people to use the constant function, and not based on what Agda can and cannot infer. If they wish to pass both types, it seems almost certain* to me that they should be using diagonal-exponential instead.

[fredrik-bakke]

Meaning I currently disagree with defining const' as you suggest

[EgbertRijke]

Meaning I currently disagree with defining const' as you suggest

We can omit const' from my suggestion, and use diagonal-exponent instead. Do you agree to make both type arguments in const implicit?

EDIT: I realized that my comment could be read in a confronting manner, but that was not intended.

[EgbertRijke]

I just think that from a maintainers perspective, it is not good to let Agda dictate what arguments should be implicit based but we should make that decisions as library designers based on what argument could be logically grouped together.

The way I'm reading this is in contradiction with the coding style. Quoting https://unimath.github.io/agda-unimath/CODINGSTYLE.html#guidelines-for-definitions-in-the-agda-unimath-libraryhttps://unimath.github.io/agda-unimath/CODINGSTYLE.html#guidelines-for-definitions-in-the-agda-unimath-library:

Implicit arguments: If an argument can be inferred in most use cases, make it implicit.

Should the guideline be edited to not make this very direct blanket statement?

Perhaps the guideline should be edited, but:

• It should be understood that if a guideline leads to bad experiences, as I described above, then we can adjust.
• In this particular case both arguments of const could typically be inferred.

[fredrik-bakke]

Meaning I currently disagree with defining const' as you suggest

We can omit const' from my suggestion, and use diagonal-exponent instead. Do you agree to make both type arguments in const implicit, or is that suggestion also problematic to you?

Well, I'm unsure. I find the suggestion for const unintuitive. It seems to me like users will have to specify the exponent in some cases, and I like having a uniform construction for it. I am guessing you want const to behave the same way as point? If one on the other hand wants it to be similar to precomp, then one does want the type to be explicit (although I realize the argument order should be opposite of the current one)

[fredrik-bakke]

Ah, but you are right. The use cases I have in mind where I want const to look like precomp are already covered by diagonal-exponential.

[fredrik-bakke]

Here's an instance where Agda is not able to infer the exponent:

[EgbertRijke]

Here's an instance where Agda is not able to infer the exponent:

Wouldn't this code be conceptually clearer if it was dependent postcomposition with a diagonal?

[fredrik-bakke]

Wouldn't this code be conceptually clearer if it was dependent postcomposition with a diagonal?

While I'm not sure in that particular scenario, here's another one where it seems appropriate to use const, but that doesn't work.

[fredrik-bakke]

To be honest, it still seems to me that the current implementation in this branch is the best one.

[EgbertRijke]

Ok, thank you for exploring the other option with me. We'll go with your solution.

[fredrik-bakke]

Ok, thank you for exploring the other option with me. We'll go with your solution.

No worries, thanks for looking into it and discussing it with me!

[fredrik-bakke]

Sorry for the delay. I implemented your suggestions now.