Implicit arguments in category theory

Stream: general

[Yaël Dillies]

docs#category_theory.adjunction.comp takes in two out of four functors explicitly. Why is it so? (I don't care much, I just want to know)

[Kevin Buzzard]

My guess: people want to apply it and lean isn't always smart enough to guess exactly how to fill in the metavariables without some hints

[Yaël Dillies]

Yeah, but why those two?

[Kevin Buzzard]

My guess: look at where it's used and you'll find that it's used very little and in the case where it was used, this was the convenient convention :-)

[Kevin Buzzard]

Either that or you'll find that it was just some mix-up with variables :-)

[Adam Topaz]

In practice, if you want to construct an adjunction which you know is the composition of two adjunctions, and you have the first one at hand, say adj_1, then it is useful to be able to write down what you're composing with if you want to construct something in term-mode.

[Adam Topaz]

e.g. adj_1.comp F G _ and you fill in the blank

[Yaël Dillies]

Okay, so somehow you always compose up rather than down?

[Adam Topaz]

more often than not, yes. Besides, dot notation won't work if you try to do the same thing but compose the other way

[Adam Topaz]

Note that this is in the adjunction namespace

[Yaël Dillies]

Yes, I noticed (and I'm fixing the lack of namespace in docs#adjunction.left_adjoint_uniq)