§ Different types of arguments in Lean4:

• (x: T) regular argument
• [S: Functor f] typeclass argument / argument resolved by typeclass resolution
• {x: T}: Maximally implicit argument, to be inferred.
• ⦃x: T⦄: Non-maximally-inserted implicit argument. It is instantiated if it can be deduced from context, and remains uninstantiated (ie, no metavariable is introduced) otherwise.

In Coq people shun away from this binder. I'm not sure why, I guess there are issues with it at a larger scale. We could get rid of it. For the paper it's utterly irrelevant in my opinion